Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21437

Simply defining Gödel Incompleteness and Tarski Undefinability away V21

Cross-posted to 4 groups.

Show all headers | View raw

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:
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.


/**
     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.
**/

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
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.
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.

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)

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

∃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 ⊬ ¬φ).

-- 
Copyright 2020 Pete Olcott

Back to comp.theory | Previous | Next — 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