Refutation of Halting Problem Proof

http://liarparadox.org/HP_Infinite_Recursion.pdf
The following is based on the material from the above link:

It combines everything into a single Turing Machine definition
and corrects, clarifies and simplifies the original text.
The second start state of Ĥ has been renamed to qx.

Figure 12.3

Definition of Turing Machine Ĥ (state transition sequence)
q0 ŵ ⊢* Ĥ qx ŵ ŵ ⊢* Ĥ qy ∞
q0 ŵ ⊢* Ĥ qx ŵ ŵ ⊢* Ĥ qn

Turing Machine Ĥ is applied to a Turing Machine description of itself ŵ.
Would Ĥ transition to its state (qy) or ((qn)) on ŵ ?

To answer this question we perform an execution trace on Ĥ
(1) At q0 Ĥ makes a copy of its input, for clarity we will call this copy ŵ2.
(2) At qx Ĥ begins to evaluate what ŵ would do on its input ŵ2.

Execution trace of Ĥ analysis of finite string ŵ
(3) At q0 ŵ would make a copy of its input, we will call this copy ŵ3.
(4) At qx ŵ would begin to evaluate what ŵ2 would do on its input ŵ3.
Can you see the infinite recursion?

The end result of all of this is that The Halting Problem proof suffers from the exact same Pathological Self-Reference (PSR) error as the Liar Paradox.

We must first formalize expressions using Higher Order Logic (HOL) with Self-Reference Semantics (SRS). Then we translate these expressions intro their corresponding Directed Acyclic Graph (DAG).

PSR is detected when the translation of a HOL expression into a DAG requires the insertion of infinite cycles into this otherwise acyclic graph.
(New insight: cycles may be OK infinite cycles must be rejected.)

Pathological-Self-Reference(X) means that expression X specifies an infinite evaluation sequence that never resolves to True or False.

LP  ≡  ~True(LP)           // Liar Paradox
  Ĥ  ≡     Halts(⌈Ĥ⌉)         // ⌈Ĥ⌉ is TMD of Ĥ
  G  ≡  ~Provable(⌈G⌉)   // ⌈G⌉ is Gödel Number of G

Copyright 2004, 2016, 2017, 2018 Pete Olcott

Terminology of Minimal Type Theory

Wolfram Mathworld: Axiom
An axiom is a proposition regarded as self-evidently true without proof.

Wikipedia: Axiom
An axiom or postulate is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments.

Wolfram Mathworld: Theorem
A theorem is a statement that can be demonstrated to be true by accepted mathematical operations and arguments.

Wikipedia: Theorem
In mathematics, a theorem is a statement that has been proved on the basis of previously established statements, such as other theorems, and generally accepted statements, such as axioms.

Axiom(MTT)
This differs from the conventional meaning of Axiom(Math) in that it a formal expression of language that has been tautologically defined to be necessarily True.

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)

If the above formalism succinctly states the accurate conclusion
of the 1931 GIT and this conclusion can be proven self-contradictory
then all of the details of the 1931 GIT can be ignored as extraneous
and the 1931 GIT can be refuted entirely on the basis that its conclusion
is self-contradictory.

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)

https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence 
A formula A is a syntactic consequence within some formal system FS
of a set Γ of formulas if there is a formal proof in of A from the set Γ.
Γ ⊢FS A  (translated to Minimal Type Theory becomes) ∃Γ ⊆ 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.