2018-11-05 02:11:10 UTC
A world class expert provided some coaching. They have published very much
in the field of Incompleteness and many related fields.
They changed this:
∀F ∈ Formal_Systems (∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G)))
L(F) means the language of formal system F.
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)
I realized that Q is not needed if the following expression evaluates to False:
∃F ∈ Formal_Systems ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
The following analysis seems to refute Gödel 1931 Incompleteness as long as
the term "satisfiable" is interpreted using the conventional meanings of the
symbols within symbolic logic.
If G was Provable in F this contradicts its assertion: G is not Provable in F
If ~G was Provable in F this contradicts its assertion: G is Provable in F.
Since G is neither Provable nor Refutable in F it forms a Gödel sentence in F.
Because G is not satisfiable in any Formal System F, the Gödel sentence does not exist.
Copyright 2018 Pete Olcott