Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21438

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

Cross-posted to 4 groups.

Show all headers | View raw

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.

> 
> /**
>      The system of Simple_Arithmetic (SA) demonstrates that the
>      membership algorithm of recursive language L could be defined
>      to operate on finite strings of w some alphabet Σ such that the
>      Boolean function Theorem(w) decide would whether or not finite
>      string w is a theorem of the formal system of SA.
> 
>      The WFF of SA are defined by this regular expression:
>      [0-9]+[\+*][0-9]+[=<>][0-9]+
>      and specifies the entire language of the Simple_Arithmetic.
> 
>      A corresponding C++ program operates of finite strings of
>      the SA language as a quoted command line parameter and
>      decides whether the input finite string is a theorem of SA.
>      Only Theorems of SA are construed to be True in SA.

You have never given a definition of a formal system SA. You have given 
a computer program which adds numbers. That is not a formal system.

More importantly, though, all your program does is calculate sums. So it 
doesn't meet the requirements which Gödel lays out at the beginning of 
his proof, which is that it only applies to systems in which a certain 
minimal amount of arithmetic can be expressed. Your computer program 
doesn't come even remotely close to meeting this minimal threshold, so 
even if you were able to prove that this "system" is complete, it would 
have absolutely no bearing on Gödel.

> **/
> 
> Stanford Encyclopedia of Philosophy
> considers this as a reasonable approximation of the Gödel sentence:
> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
> (a) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉) // SEP original
> 
> (b) F ⊢ G_F ↔ ¬Prov_F(G_F) // Remove the arithmetization restriction

Which is a completely illegitimate operation. Those ceiling brackets 
MEAN something. You can't just delete them.

⌈G_F⌉ is an element of the set of natural numbers.
G_F is a proposition, i.e. an element of {true, false}

Raatikainen's function Prov_F() maps from integers to truth values. It 
does not map from truth values to truth values, so ¬Prov_F(G_F) isn't 
even a properly typed expression.

Since you like C so much, consider the following:

x = strcmp("2 + 3", "3 + 2");

what you're doing is no different from replacing the above with:

x = strcmp(2 + 3, 3 + 2);

Presumably these would give different results, if only the second one 
would actually compile which of course it won't. Take-home-point: You 
can't just randomly delete brackets, braces, quotes, ceiling brackets, 
etc. Things just don't work that way.

> Now the formal proof is free to use arithmetization or not, thus making 
> the provability of (b) logically equivalent to the provability of (a).
> 
> (c) ∃G ∈ WFF(F) (G ↔ F ⊬ G) // Change syntax and quantify.

Which is also not legitimate. Raatikainen's function Prov_F() is *not* 
the same as the ⊢ meta-operator. Yes, they both have to do with 
provability, but they are not the same thing and cannot simply be 
substituted for one another.

> Is there any sentence G of theory F such that G is logically equivalent 
> to its own unprovability?
> 
> // The formal system of Simple_Arithmetic has been defined above
> You can prove that a true statement is true:
> "2 + 3 = 5" ↔ (F ⊬ "2 + 3 = 5")
> LHS of ↔ is true. RHS of ⊬ is true. RHS of ↔ is false.
> 
> You can prove that a false statement is false:
> "2 + 3 = 9" ↔ (F ⊬ "2 + 3 = 9")
> LHS of ↔ is false. RHS of ⊬ is false. RHS of ↔ is true.
> 
> Thus there does not exist any sentence G of theory F that is logically 
> equivalent to its own unprovability because this is self-contradictory: 
> ∃G ∈ WFF(F) (G ↔ F ⊬ G) is false.

Umm. Now you've gone completely off the deep end. How exactly does 
considering TWO cases prove that there does not exist ANY case?

Consider the following statement: People are under five years of age if 
and only if they have red hair.

I present you with Mary, who is four years old and has red hair.
I present you with Harold, who is sixteen years old and has black hair.

Quod erat demonstrandum.

Do you seriously believe that anyone would accept that logic?

You can prove an existential claim with a single example.
You can disprove a universal claim with a single counterexample.

To disprove an existential claim or to prove a universal claim requires 
more than just considering a few specific cases.

> Now we evaluate the negation of: ∃G ∈ WFF(F) (G ↔ F ⊬ G)
> https://sites.math.washington.edu/~aloveles/Math300Winter2011/m300Quantifiers.pdf 
> 
> 
> Applying negation rule (2): ¬[∃x ∈ A, P(x)] ⇔ ∀x ∈ A, ¬P(x).
> ¬[∃G ∈ WFF(F) (G ↔ F ⊬ G)] ⇔∀G ∈ WFF(F) (G ↔ F ⊢ G)

That isn't even the correct negation of ∃G ∈ WFF(F) (G ↔ F ⊬ G).

That would be

∀G ∈ WFF(F) ¬(G ↔ F ⊬ G)

You really should try learning logic before you actually attempt to use it.

> All WFF G of formal system F are logically equivalent to their own 
> provability. This is self-evident.

It's not even evident, let alone self-evident.

Let's return to the example from Q which you keep avoiding. In Q, x + y 
= y + x is not provable.

Is it "self-evident" to you that (x + y = y + x) is logically equivalent 
it its own provability in Q?

André

> ∃G ∈ WFF(F) (G ↔ F ⊬ G) is false.
> Its negation ∀G ∈ WFF(F) (G ↔ F ⊢G) true thus failing to meet the 
> standard definition of incompleteness: A theory T is incomplete if and 
> only if there is some sentence φ such that (T ⊬ φ) and (T ⊬ ¬φ).
> 


-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.

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