The ultimate foundation of
[a priori] Truth

Simple English:
For any natural (human) or formal (mathematical) language L we know that an expression X of language L is true if and only if there are expressions Γ of language L that connect X to known facts.

The only way that you know that a {dog} is not a type of {cat} is that the terms: {dog} and {cat} are defined to have a set of {BaseFact} properties, and some of these properties are defined to be mutually exclusive. A BaseFact is the ultimate ground of the notion of True.

BaseFact is an expression X of (natural or formal) language L that has been assigned the semantic property of True by making it a member of the collection named: BaseFacts.   (Similar to a math Axiom).
(1) BaseFacts that contradict other BaseFacts are prohibited.
(2) BaseFacts must specify Relations between Things.
The above is the complete specification for a BaseFact.

To verify that an expression X of language L is True or False only requires a syntactic logical consequence inference chain (formal proof) from one or more BaseFacts to X or ~X.    (Backward chaining reverses this order).

True(L, X) ↔ ∃Γ ⊆ BaseFacts(L) (Γ  ⊢ X)
False(L, X) ↔ ∃Γ ⊆ BaseFacts(L) (Γ  ⊢ ~X)

Sentence (mathematical logic)
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. The restriction of having no free variables is needed to make sure that sentences can have concrete, fixed truth values: As the free variables of a (general) formula can range over several values, the truth value of such a formula may vary.

Defining a Generic Decidability Decider:
∀L ∈ Formal_Systems
∀X ∈ Closed-WFF(L)
~True(L, X) ∧ ~False(L, X) → Incorrect(L, X)

A language L is a set of finite strings of characters from a
defined alphabet specifying relations to other finite strings.
These finite strings could be tokenized as single integer values.

A Relation is identical to the common notion of a Predicate
from Predicate Logic, essentially a Boolean valued function.

Finite string Expression X expresses relation R of language L.

True(L, X) ↔ ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X)
01 There_Exists (2)(6)
02 Subset_Of      (3)(4)
03 Γ
04 BaseFacts        (5)
05 L
06 Provable          (3)(7)
07 X

Copyright 2018 (and many other years since 1997) Pete Olcott

Removing all extraneous complexity from the 1931 GIT

So far everyone in the whole world is not up to the challenge of removing the extraneous complexity from the 1931 Incompleteness Theorem.

This complexity comes from the fact that the GIT must construct the equivalent of a HOL provability predicate within the language of arithmetic.

Doing this apparently requires 46 definitions, Gödel numbers and the Diagonal lemma. If we were dealing with HOL that has its own provability predicate none of this extraneous complexity would be required.

Stanford Encyclopedia of Philosophy Gödel’s Incompleteness Theorems 
2.5 The First Incompleteness Theorem—Proof Completed
(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉).

My adaptation:
G ↔ ~∃Γ ⊆ WFF(F) Provable(Γ, G) // No Gödel numbers required

Simple refutation of the 1931 Incompleteness Theorem

a Collection is defined one or more things that have one or more properties in common. These operations from set theory are available:  {⊆, ∈}

An BaseFact is an expression X of (natural or formal) language  L that has been assigned the semantic property of True. (Similar to a math Axiom).

A Collection T of BaseFacts of language L forms the ultimate foundation of the notion of Truth in language L.

To verify that an expression X of language L is True or False only requires a syntactic logical consequence inference chain (formal proof) from one or more elements of T to X or ~X.

True(L, X) ↔ ∃Γ ⊆ BaseFact(L) Provable(Γ, X)
False(L, X) ↔ ∃Γ ⊆ BaseFact(L) Provable(Γ, ~X)

Since an expression X of language L is not a statement of language L unless and until it is proven to be True or False in L, every statement of language L can be proved or disproved in L.

∀L ∈ Formal_Systems
∀X ∈ L
Statement(L, X) → ( Provable(L, X) ∨ Refutable(L, X) )

Stanford Encyclopedia of Philosophy Gödel’s Incompleteness Theorems
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.

Formalized as: Statement(F, G) ∧ ~Provable(F, G) ∧ ~Refutable(F, G)

“This sentence is not true”.    // is not true
// HOL with self-reference semantics
LP ≡ ~∃Γ ⊆ BaseFact(L) Provable(Γ, LP)

LP is rejected as semantically incorrect on the basis that no formal proof exists from one or more elements of T to LP or ~LP.
Because LP is neither True nor False LP is semantically incorrect.

“This sentence is not provable”.    // is not provable
// HOL with self-reference semantics
G ≡ ~∃Γ Provable(Γ, G)

G is rejected as semantically incorrect on the basis that no formal proof exists from one or more elements of T to G or ~G.

Copyright 2017, 2018 Pete Olcott 

The Nature of Truth in Plain English

A Statement in English is only known to be True when it is established to be a Verified Fact. An Analytical ** Fact is completely verified as True entirely based on the meaning of its words.

A BaseFact is an expression of language defined to be True.

To prove that an expression of language is an Analytical Fact we confirm that there is a correct line-of-reasoning from one or more BaseFacts that make this expression necessarily True.

Since every Statement of language must be True or False and this is verified by proving that the statement is a Analytical Fact or contradicts an Analytical Fact all Statements of language can always be proved or disproved.

** Analytical means: a priori

Copyright Pete Olcott 2018

 

Simple English Refutation of Gödel’s 1931 Incompleteness Theorem

A Statement in English is only known to be True when it is established to be a verified fact. An Analytical Fact is completely verified as True entirely based on the meaning of their words.

To prove that an expression of language is an Analytical Fact we  confirm that there is a correct line-of-reasoning from other Analytical Facts that make this expression necessarily True.

False simply means contradicting an Analytic Fact. An Statement of language must be True or False or it is not a correct Statement.

Since every Analytic Statement of language must be True or False and this is verified by proving that the statement is an Analytic Fact or contradicts an Analytic Fact all Statements of language can always be proved or disproved.

Here is the plain English version of the proof that I am refuting: **
“The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.”

**Stanford Encyclopedia of Philosophy Gödel’s Incompleteness Theorems.

All material besides the SEP quote is Copyright 2017, 2018 Pete Olcott

True(X) and ~Provable(X) is Impossible

A Fact(English) is Only known to be True(Math) when it is verified(English).
Analytic Facts(English) are Only Verified(English) by their Proof(Math).

An analytic Fact is an expression of language that is completely verified as True entirely based on the meaning of its words (or symbols).

Some expressions of language are defined to be necessarily True.  This forms the foundation of all Truth. To keep things simple we will call these expressions VERIFIED_FACTS.

To provide mathematical rigor to the definition of VERIFIED_FACTS we apply the David Hilbert formalist approach and specify a set of finite strings that are defined to have the semantic property of: True.

True(L, Y, X) means that there is an inference chain from a set Y of one or more VERIFIED_FACTS of L that derive X.

False(L, Y, X) means that there is an inference chain from a set Y of one or more VERIFIED_FACTS of L that derive ~X.

Provable(L, Y, X means that there is an inference chain from a set Y of one or more expressions of L that derive X.

Refutable(L, Y, X) means that there is an inference chain from a set Y of one or more expressions of L that derive ~X.

Statement(L, Y, X) ↔ ( True(L, Y, X) ∨ False(L, Y, X) ) ∴
~◇( Statement(L, Y, X) ∧ ~Provable(L, Y, X) ∧ ~Refutable(L, Y, X) )

This is a refinement to the 1997 Mathematical Mapping Theory of Truth

Copyright 1997 2004, 2015, 2016, 2017, 2018 Pete Olcott

1931 Incompleteness Theorem Refutation

https://plato.stanford.edu/entries/goedel-incompleteness/
“The first incompleteness theorem states that in any consistent
formal system F within which a certain amount of arithmetic can
be carried out, there are statements of the language of F which can
neither be proved nor disproved in F.”

Formalized as: SentenceF(G) ∧ ~ProvableF(G) ∧ ~RefutableF(G)

Any expression G of language F is not a sentence of language F 
if this expression G of language F is not provable or refutable in F.
(see definitions below)

∀FS ∈ Formal_Systems:
… Provable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ X)
… Refutable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ ~X)
… True(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ X)
… False(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ ~X)
… Sentence(FS, X) ↔ ( True(FS, X) ∨ False(FS, X) )
Axioms ⊆ Rules ⊆ WFF  ∴
True(FS, X) ⊢ Provable(FS, X)
False(FS, X) ⊢ Refutable(FS, X)

∴ ( ~Provable(F, G)  ∧  ~Refutable(F, G) )  → ~Sentence(F, G)

 

copyright 2017, 2018 Pete Olcott

Refutation of Halting Problem Proof

Decidability of the Halting Problem as a David Hilbert formalism
∃a ∈ Turing_Machines_Descriptions
∀b ∈ Finite_Strings  // some of these specify Turing Machine Descriptions
∀c ∈ Finite_Strings
Halts(a, b, c) ∨ ~Halts(a, b, c)

Halt Decider definition
A Halt Decider (HD) determines whether or not a finite string represents a correct Turing Machine Description that would halt on its input. It does this by performing a mathematical proof on a pair of finite strings as a David Hilbert formalism in the language of Turing Machine Descriptions.

The syntactic logical consequence of this proof is two finite strings:
(1) “Y”  input pair (b,c) is a correct TMD that would halt on its input.
(2) “N” indicating the else branch of (1).

If the first element of the input finite string pair is a correct TMD then this proof must necessarily proceed from the specified TMD start state through all of the state transitions of this TMD to the halting or non halting behavior of this TMD.

The proof would essentially be a hypothetical execution trace** of the state transition sequences of the input TMD. It cannot be an actual execution trace or the halt decider could have non-halting behavior.
** Like step-by-step mode in a debugger.

http://liarparadox.org/HP_Infinite_Recursion.pdf
The following has been adapted from material from the above link:
We begin our analysis by constructing a hypothetical halt decider: H.

Figure 12.1 Turing Machine H
Figure 12.1

The dashed lines proceeding from state (q0) are represented in the text definition as the asterisk ⊢* wildcard character. These conventions are used to encode unspecified state transition sequences.

Definition of Turing Machine H (state transition sequence)
H.q0 Wm W ⊢* H.qy  // Wm W corresponds to (b,c) shown above
H.q0 Wm W ⊢* H.qn  // Wm W corresponds to (b,c) shown above

The diagram and the state transition sequence indicate that H begins at its own start state H.q0 and is applied to finite string pair (Wm, W).

H.qy is the final state of H indicating that Wm is a correct TM that would halt on input W.  Syntactic logical consequence : “Y” (shown above).

H.qn is the final state of H indicating that Wm is not a correct TM that would halt on input W.  Syntactic logical consequence: “N” (shown above).

We create Turing Machine Ĥx by making the following changes to H:
(1) Ĥx copies its input Wm a its Ĥx.q0 state and transitions to its Ĥx.qx state.

(2) Ĥx would begin to evaluate Wm Wm at its Ĥx.qx state in exactly the same way that H would begin to evaluate its Wm W input at its H.q0 state.

Since Turing Machine Ĥx is created by adapting H, it would have exactly the same behavior at its Ĥx.qx state as H would have at its H.q0 state.

Figure 12.4 Turing Machine Ĥx
Figure 12.4

Definition of Turing Machine Ĥx (state transition sequence)
Ĥx.q0 Wm ⊢* Ĥx.qx Wm Wm ⊢* Ĥx.qy   // NO LOOP
Ĥx.q0 Wm ⊢* Ĥx.qx Wm Wm ⊢* Ĥx.qn   // NO LOOP HERE EITHER

If Turing Machine H is applied to Turing Machine description [Ĥx] [Ĥx]
 would it transition to H.y or H.n ? 

We append a “2” to the input to [Ĥx] for clarity [Ĥx2] is a copy of [Ĥx].

To answer this question we perform an execution trace on H
(1) H begins at its start state H.q0.
(2) H begins to evaluate what [Ĥx] would do on its input [Ĥx2].

Hypothetical Execution trace of what [Ĥ] would do if it was executed
(3) [Ĥx] would begin at its start state [Ĥx].q0
(4) [Ĥx] would make a copy of its input [Ĥx2], we will call this [Ĥx3].
(5) [Ĥx] would transition to its state [Ĥx].qx.
(6) [Ĥx] would begin to evaluate what [Ĥx2] would do on its input [Ĥx3].
Can you see the infinite recursion?

H [Ĥx] [Ĥx] specifies an infinitely recursive evaluation sequence.
Every HP proof by contradiction depends this same infinite recursion.

Because of this every TMD in the infinitely recursive sequence is defined in terms of H each would reject the whole sequence as semantically incorrect before even beginning any halting evaluation.

Therefore H would correctly transition to its H.qn state rejecting the infinitely recursive evaluation sequence specified by [Ĥx] [Ĥx] as the semantic error of Pathological self-reference(Olcott 2004).

Figure 12.3 Turing Machine Ĥ
Figure 12.3

Definition of Turing Machine Ĥ (state transition sequence)
Ĥ.q0 Wm ⊢* Ĥ.q Wm Wm ⊢* Ĥ.qy ∞
Ĥ.q0 Wm ⊢* Ĥ.q Wm Wm ⊢* Ĥ.qn

Copyright 2004, 2015, 2016, 2017, 2018 Pete Olcott

Reformulating the notions of Truth and formal provability

I am reformulating the generic notions of {Truth} and {formal provability} from scratch. I cannot use the conventional terms of the art with their conventional meanings because these terms of the art have fundamental misconceptions built in to their definitions.

These conventional terms of the art are defined in terms of other conventional terms of the art and these terms also have fundamental misconceptions built in to their definitions, on and on.

My system analyzes specific instances the generic notion of finite strings of characters to determine if these finite strings correspond to the generic notion of {Truth}.

The generic notion of {formal provability} simply examines whether or not a specific preexisting set of finite string transformation rules allow one finite string to be derived from another. In the case where the first finite string has the Boolean property of True, then the derived finite string is also known to have this same Boolean property.

The set of finite string transformation rules includes a set of finite strings that have been defined to have the Boolean property of True. This corresponds to notion of Prolog Facts. From the Fact that “a can is made of tin” we can derive the fact that “a can is made of metal”.

The above systematic reconstruction of the notions of {Truth} and {formal provability} are applied to the following of specific concrete examples. The essence of these examples are reformalized and analyzed for logical coherence within a new formal system.

The Liar Paradox from antiquity
David Hilbert’s 1928 Entscheidungsproblem
Kurt Gödel’s 1931 incompleteness Theorem
Alfred Tarski’s 1936 Undefinability Theorem
Alan Turing’s 1937 Halting Problem

1931 Incompleteness Theorem Refutation Strategy

https://plato.stanford.edu/entries/goedel-incompleteness/
“The first incompleteness theorem states that in any consistent
formal system F within which a certain amount of arithmetic can
be carried out, there are statements of the language of F which can
neither be proved nor disproved in F.”

Formalized as: SentenceF(G) ∧ ~ProvableF(G) ∧ ~RefutableF(G)

Any expression G of language F is not a sentence of language F 
if this expression G of language F is not provable or refutable in F.
(see definitions below)

∀FS ∈ Formal_Systems:
… Provable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ X)
… Refutable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ ~X)
… True(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ X)
… False(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ ~X)
… Sentence(FS, X) ↔ ( True(FS, X) ∨ False(FS, X) )
Axioms ⊆ Rules ⊆ WFF  ∴
True(FS, X) ⊢ Provable(FS, X)
False(FS, X) ⊢ Refutable(FS, X)

∴ ( ~Provable(F, G)  ∧  ~Refutable(F, G) )  → ~Sentence(F, G)

copyright 2017, 2018 Pete Olcott

Simple tutorial on Propositional Logic

A very simple tutorial explaining Propositional Logic short-hand to everyone that knows Aristotle’s Syllogisms. I am pretty sure that this is all there is to Propositional Logic. If I missed anything please let me know.

Aristotle Syllogism (slightly enhanced):
…..Premise (a) “It is raining outside.”
…..Premise (b) “You go outside unprotected from the rain.”
Conclusion (c) “You get wet.”

Partial translation to Propositional Logic:
if (a) and (b) then (c)

Full translation to Propositional Logic:
(a ∧ b) → c

Propositional Logic Symbols and their English meanings
P …………. P is true
~P ……….. P is not true
P ∧ P ……. P and Q are both true
P ∨ Q ……. either P or Q (or both) are true
P → Q ….. if P is true then Q is true
…………….. if Q is false then P is false
…………….. if P is false then (Q  ∨ ~Q)

If you understand the above then you know your P’s and Q’s

Forming a Bridge between Proof Theory and Model Theory

Formalizing the internal semantic meaning of propositional (sentential) variables using Rudolf Carnap (1952) Meaning Postulates bridges the gap between syntactic consequence (formal proof) and semantic consequence (logical entailment).

Syntactic versus Semantic Logical Consequence
Meaning postulates specify semantic logical entailment syntactically.
The best two examples from his paper: Bachelor(x) and Warmer(x,y):

Bachelor(x) → ~Married(x)

For example, let ‘W’ be a primitive predicate designating the relation Warmer. Then ‘W’ is transitive, irreflexive, and hence asymmetric in virtue of its meaning.

In the previous example of the predicate ‘W’, we could lay down the following postulates (a) for transitivity and (b) for irreflexivity; then the statement (c) of asymmetry:

(a)  ∀(x,y,z) Warmer(x,y) ∧ Warmer(y,z) → Warmer(x,z)
(b)  ∀(x)      ~Warmer(x,x)
(c)  ∀(x,y)    Warmer(x,y) → ~( Warmer(y,x) )

Meaning Postulates Rudolf Carnap (1952)

Copyright 2017 Pete Olcott

Fulfilling Tarski’s ∀x True(x) ↔ φ(x)

x True(x) ↔ φ(x) is fulfilled by the satisfaction of the Provability predicate on the basis of axioms: 
x True(x) ↔ ∃Γ ⊆ FS ∧ Axioms(Γ) Provable(Γ, x)

Syntactic Consequence (Provability)
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)

1931 Incompleteness Theorem is only undecidable because it is not a sentence expressing Boolean

https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
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.

G @ ∃X ~Provable(X, G) // Minimal Type Theory
(1) The above expression says that it is not provable.
(2) The above expression is indeed not provable.
(3) However the above expression is not a sentence (see graph below).

Expression translated into a Directed Acyclic Graph by the MTT compiler
[01] G                                (02)(04)
[02] THERE_EXISTS (03)
[03] X
[04] NOT                          (05)
[05] Provable                 (03)(01)   // cycle indicate infinite evaluation loop

Cycles in directed graphs of logical expressions are erroneous:
https://en.wikipedia.org/wiki/Occurs_check
A naive omission of the occurs check leads to the creation of cyclic structures and may cause unification to loop forever.

Programming in Prolog (2003) by Clocksin and Mellish page 254
equal(X, X).
?- equal(foo(Y), Y).
match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y, which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind of infinite structure.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉)

Match a term against an uninstantiated subterm of itself:
Equivalent( GF, ¬ProvF( Godel_Number(GF) )
Equivalent( GF, ¬ProvF(GF) )
Equivalent( ¬ProvF(GF), GF )

Equivalent( ProvF(GF), GF )
?- equal(foo(Y), Y).
Can you see how the above two are the same?

Concise Formalization of the Liar Paradox

The Liar Paradox refers to itself when it says: {This sentence is not true}
In order to mathematically formalize every aspect of the Liar Paradox as predicate logic, I had to enhance the way that predicate logic works.

Defining Self-Reference Semantics <assign alias name> operator
LHS is assigned as an alias name for the RHS
LHS ≡ RHS
The LHS is logically equivalent to the RHS only Because the LHS is merely an alias name for the RHS

LiarParadox ≡ ~True(LiarParadox).
The name and alias name operator are merely notational conventions for translating the meaning: {This sentence is not true} into predicate logic.

Translation into directed acyclic graph
01 LiarParadox (02)
02 Not         (03)
03 True        (01) 
// infinite evaluation loop

Here is how {alias name} works in computer science:
In computer science variable names to refer to memory addresses. Variable names are considered one and the same thing as the memory address. When a computer program is compiled the names are translated into these memory addresses and discarded.

// The Liar Paradox in C++
Test the value of a variable before this variable has a value
then assign this non-existent value to this variable.
bool Liar_Paradox = (Liar_Paradox == false);

This statement is semantically analogous to the one above
in that the quotient of division by zero does not exist.
double BadNumber = 1.0 / 0.0;

 

Copyright 2016, 2017 2018 Pete Olcott

Quick recap of the Liar Paradox Error

https://plato.stanford.edu/entries/logic-provability/#FixePoinTheo
2.2 The fixed point theorem
GL ⊢ B ↔ A(B)
GL ⊢ LiarParadox ↔ ~True(LiarParadox)

Do you see the similarity? Prolog rejects both of these as erroneous.
http://liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

Here is the error that Prolog detects:    (see above link)
match a term against an uninstantiated subterm of itself.

The exact same thing as this C++
bool LiarParadox = LiarParadox == false;
Copyright 2017 Pete Olcott

Copyright 2016, 2017 Pete Olcott

Refuting the conclusion of Gödel’s 1931 Incompleteness Theorem

Syntactic Consequence (Provability)
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)

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
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.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved nor disproved in F:       SentenceF(G) ∧ ~ProvableF(G) ∧ ~RefutableF(G)

G @ ~∃Γ ⊆ F Provable(Γ, G) // Minimal Type Theory
(1) The above expression says that it is not provable.
(2) The above expression is indeed not provable.
(3) However the above expression is not a sentence (see graph below).

Sentence translated into a Directed Acyclic Graph by the MTT compiler:
[01] G                                (02)(07)
[02] NOT                          (03)
[03] THERE_EXISTS (04)
[04] SUBSET_OF         (05)(06)
[05] Γ
[06] F
[07] Provable                 (05)(01) // cycle indicates infinite evaluation loop

G_Not_Provable.png


Defining Tarski’s 1933 ∀x True(x) ↔ φ(x)

Provable explained in using conventional notation:
Logical_consequence#Syntactic_consequence

Direct quote from above Wikipedia link:
A formula A is a syntactic consequence within some formal system FS of a set Γ of formulas if there is a formal proof in FS of A from the set Γ.
ProvableFS (Γ, A)  // Paraphrase of Γ ⊢FS A

In other words: Formula A is Provable within Formal System FS if there exists an inference chain (connected sequence of WFF) from a set of Formula Γ to Formula A.

Furthermore if Γ are axioms of FS, then Provable(Γ, A) ≡ True(A) in FS:
TrueFS(A) ≡ ProvableFS (Γ, A)    
FalseFS(A) ≡ ProvableFS (Γ, ~A) 

Last paragraph copyright 2017 Pete Olcott

Gödel’s 1931 Incompleteness Theorem summed as a single line of Minimal Type Theory

https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.

When Godel said that he found a sentence G of language F such that:
~(ProvableF(G) ∨ RefutableF(G) ) he was wrong.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉) 

1931 GIT entirely summed up as a single line of Minimal Type Theory:
G @ ∃X ~Provable(X, G)

(1) The above expression says that it is not provable.
(2) The above expression is indeed not provable.
(3) However the above expression is not a sentence (see graph below).

Sentence translated into a Directed Acyclic Graph by the MTT compiler:
[01] G                                (02)(04)
[02] THERE_EXISTS (03)
[03] X
[04] NOT                         (05)
[05] Provable                (03)(01)   // cycle indicate infinite evaluation loop

G_Not_Provable.png

1931 Incompleteness Theorem simplified

∃X (X ⊢ Y) asserts that there is a set of connected WFF from X to Y.

If G is an alias (sentential variable) for ∃X (X ⊢ Y), then G is either True or False, even if both X and Y are gibberish.

If G is an alias (sentential variable) for ~∃X (X ⊢ G) we have pathological self-reference creating infinite recursion.  This prevents G from ever evaluating to either True or False, thus making G semantically ill-formed.

copyright 2017 Pete Olcott  (Created Friday October 13, 2017)

Originally posted material is shown below

If the 1931 Incompleteness Theorem is correct then the much simpler expression at the end of this post equally proves that there are some sentences of predicate logic that are neither provable nor refutable.
Syntactic_Logical_Consequence (Γ proves A)

A formula A is a syntactic consequence within some formal system FS of a set Γ of formulas if there is a formal proof in FS of A from the set Γ:
Γ ⊢ FS A

Translation to Minimal Type Theory notational conventions
Γ ⊢ FS A  ≡ ( Γ ⊂ FS (Γ ⊢ A) )

Named predicate (of predicate logic PL) impossible to prove and impossible to refute: G( ~∃Γ ⊂ PL (Γ ⊢ G) )

Simple English refutation of the Incompleteness Theorem

https://plato.stanford.edu/entries/goedel-incompleteness/
The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.

As long as the above sentence accurately sums up the GIT no greater understanding of the GIT is required to totally refute it:

(1) Every WFF of all formal systems must be a truth bearer.

(2) If no formal proof exists within a formal system to show that an expression evaluates to exactly one of the set: {true, false}, then this expression is not a truth bearer, and not a WFF in this formal system.

(3) Therefore there are no WFF in any formal system which can be neither proved nor disproved within this formal system.