G ↔ ~∃Γ ⊆ F Provable(Γ, G) // Simplified 1931 GIT in Predicate Logic

[Pete Olcott]

https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence
A formula A is a syntactic consequence within some formal system 𝓕𝓢 of a set Γ of formulas if there is a formal proof in 𝓕𝓢 of A from the set Γ.    Γ ⊢_𝓕𝓢 A      ≡     ∃Γ ⊆ FS Provable(Γ, A)

I just noticed that I have been saying this incorrectly all along.
I did not notice the error until I translated it into English.
The mistake was that I had the negation on the Provable predicate
instead of on the existential quantifier.

This may be third order logic because it quantifies over sets of WFF
G ↔ ~∃Γ ⊆ F Provable(Γ, G) // Predicate Logic
G is logically equivalent to the expression:
[ There does not exist a set Γ of WFF in language F such that G is proven from Γ ]

Assuming that the above (3rd order logic?) expression can be translated into Prolog:
The above predicate logic expression would be rejected by the Prolog by the following Prolog predicate:

acyclic_term(@Term)
True if Term does not contain cycles, i.e. can be processed recursively in finite time.

because it attempts to match a term against an uninstantiated subterm of itself.

http://liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf
http://www.swi-prolog.org/pldoc/man?predicate=acyclic_term/1

Copyright 2017 Pete Olcott

http://liarparadox.org/index.php/2017/11/03/refuting-the-conclusion-of-godels-1931-incompleteness-theorem/

-- 
Defining Tarski’s ∀x True(x) ↔ φ(x) 
∀x True(x)  ↔ ∃y Provable(y, x)  // True entirely defined by Provability
∀x False(x) ↔ ∃y Provable(y, ~x) // False entirely defined by Refutability

[burs...@gmail.com]

But from the gist from what you post, this looks
rather like crank stuff. Sorry, I am only honest.

Am Samstag, 2. Dezember 2017 22:31:26 UTC+1 schrieb Pete Olcott:

[Pete Olcott]

On 12/2/2017 3:31 PM, Pete Olcott wrote:

https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence
A formula A is a syntactic consequence within some formal system 𝓕𝓢 of a set Γ of formulas if there is a formal proof in 𝓕𝓢 of A from the set Γ.    Γ ⊢_𝓕𝓢 A      ≡     ∃Γ ⊆ FS Provable(Γ, A)

I just noticed that I have been saying this incorrectly all along.
I did not notice the error until I translated it into English.
The mistake was that I had the negation on the Provable predicate
instead of on the existential quantifier.

This may be third order logic because it quantifies over sets of WFF
G ↔ ~∃Γ ⊆ F Provable(Γ, G) // Predicate Logic
G is logically equivalent to the expression:
[ There does not exist a set Γ of WFF in language F such that G is proven from Γ ]

Assuming that the above (3rd order logic?) expression can be translated into Prolog:
The above predicate logic expression would be rejected by the Prolog by the following Prolog predicate:

acyclic_term(@Term)
True if Term does not contain cycles, i.e. can be processed recursively in finite time.

because it attempts to match a term against an uninstantiated subterm of itself.

http://liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf
http://www.swi-prolog.org/pldoc/man?predicate=acyclic_term/1

Copyright 2017 Pete Olcott

I replaced the title and name of this link
http://liarparadox.org/index.php/2017/12/08/1931-incompleteness-theorem-is-only-undecidable-because-it-is-not-a-sentence-expressing-boolean/

--
      Γ ⊢_FS A   ↔   ∃Γ ⊆ FS Provable(Γ, A)     // MTT notational conventions
∀X True(X)   ≡   ∃Γ ⊆ MTT Provable(Γ, X)   // MTT Truth Predicate

[Pete Olcott]

On 12/8/2017 9:45 PM, Rupert wrote:

So what?

http://liarparadox.org/index.php/2017/12/08/1931-incompleteness-theorem-is-only-undecidable-because-it-is-not-a-sentence-expressing-boolean/
(G) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉).

http://liarparadox.org/index.php/2017/11/03/refuting-the-conclusion-of-godels-1931-incompleteness-theorem/
G @ ∃X ~Provable(X, G) // Minimal Type Theory

I have shown that the above two correct simplifications of the 1931 Incompleteness Theorem
are both incorrect, thus the conclusion of the original 1931 proof is also incorrect.

[Pete Olcott]

On 12/8/2017 5:44 PM, Jim Burns wrote:

On 12/8/2017 4:27 PM, peteolcott wrote:

<http://liarparadox.org/index.php/2017/12/08/1931-incompleteness-theorem-is-only-undecidable-because-it-is-not-a-sentence-expressing-boolean/>

The sentence G to which you are referring has Boolean values.
As it happens for this particular sentence G, it has different
Boolean values for different models.

This difference in value between models is not paradoxical.
The sentence G is not a theorem of the formal system.
It is theorems of a formal system which are true in all
models of that formal system.

http://liarparadox.org/index.php/2017/12/08/1931-incompleteness-theorem-is-only-undecidable-because-it-is-not-a-sentence-expressing-boolean/
(G) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉).

http://liarparadox.org/index.php/2017/11/03/refuting-the-conclusion-of-godels-1931-incompleteness-theorem/
G @ ∃X ~Provable(X, G) // Minimal Type Theory

Evaluating the satisfaction of the above two formulas never completes.

<https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)>
<wiki>
   In mathematical logic, a sentence of a predicate logic
   is a boolean-valued well-formed formula with no free
   variables. A sentence can be viewed as expressing a
   proposition, something that must be true or false.
</wiki>

If you read just a little bit further on that page:
<wiki>
   To properly evaluate the truth (or falsehood) of a
   sentence, one must make reference to an interpretation
   [that is: a *model* ] of the theory. For first-order
   theories, interpretations are commonly called structures.
   Given a structure or interpretation, a sentence will
   have a fixed truth value.
</wiki>

So maybe in some models this program would halt?
HERE:
    goto HERE;

That the truth value of a particular sentence depends upon
how that sentence is interpreted is a fact of first-order
logic, quite possibly of all logic, too. Most importantly,
that is a fact about everyday, non-logic-based, non-math-based
speech.

You are still not getting me. Infinite loops are infinite loops in any language and in any interpretation.

Consider, as an example, the archetypal argument:
   Socrates is a man.
   All men are mortal
   Therefore, Socrates is mortal.
If "Socrates" refers to an important Greek philosopher,

You forgot the "if" so you made an axiom rather than a conditional.

[Dhu on Gate]

On Sat, 02 Dec 2017 15:31:19 -0600, Pete Olcott wrote:

> I did not notice the error until I translated it into English. <br>

> The mistake was that I had the negation on the Provable predicate

That's an interesting observation all of it's own.

Dhu



--
Je suis Canadien. Ce n'est pas Francais ou Anglaise.
C'est une esp`ece de sauvage: ne obliviscaris, vix ea nostra voco;-)

http://babayaga.neotext.ca/PublicKeys/Duncan_Patton_a_Campbell_pubkey.txt