Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21442

Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21

Cross-posted to 4 groups.

Show all headers | View raw

On 7/4/2020 1:21 PM, André G. Isaak wrote:
> On 2020-07-04 10:36, olcott wrote:
>> OVERVIEW:
>> The sentence used in the SEP article to show the essential gist of the 
>> 1931 Gödel incompleteness sentence
>>
>> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
>> (G) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)
>>
>> has been shown to not meet the standard definition of incompleteness:
> 
> Umm. Of course this doesn't meet the definition of incompleteness. 
> Incompleteness is a property of *systems*. What you've given above is a 
> *statement*, not a formal system.
> 
>> A theory T is incomplete if and only if there is some sentence φ such 
>> that (T ⊬ φ) and (T ⊬ ¬φ). Because its negation is provable in F.
>>
>> This is not understood to be any failing of the simplified essence to 
>> sufficiently correspond to the gist of the orginal Gödel sentence. It 
>> is understood to mean that the Gödel incompleteness sentence does not 
>> actually prove incompleteness at all.
> 
> nor has it been claimed to prove incompleteness.
> 
> The significance of
> 
> F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)
> 
> Is that this statement can only be true if EITHER F is inconsistent OR 
> if F is incomplete. And since Gödel provides a mechanical procedure for 
> generating a proposition G_F which satisfies the above, ONE of these two 
> things must be true.
> 
> This only proves that F is incomplete once we add the stipulation that F 
> is consistent. Thus, this only proves that F is incomplete once we 
> recall Gödel claims his proof only holds true for CONSISTENT formal 
> systems in which some minimal amount of arithmetic can be performed.

We are doing way too many steps at once we will never get resolution at 
the current rate because we always slip-slid into extraneous side issues.

Discussing this one step at a time until that step is 100% resolved.

Can you see how this can be existentially quantified:
F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉) such as this: ∃G_F ∈ WFF(F) ¬Prov_F(⌈G_F⌉)

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 11:36 -0500
  Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-04 12:21 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 16:28 -0500
      Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 07:17 -0600
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 10:31 -0500
          Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:28 -0600
            Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 11:42 -0500
              Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:53 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:38 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 12:44 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:56 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 13:16 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 15:25 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 14:46 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 16:08 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 David Kleinecke <dkleinecke@gmail.com> - 2020-07-05 15:28 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 17:50 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2020-07-05 17:13 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 20:37 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) André G. Isaak <agisaak@gm.invalid> - 2020-07-05 20:46 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 17:39 -0500
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:15 -0500

csiph-web