Halting Problem Proof from Finite Strings to Final States

**The following relatates to the above paper and shows how a
decidability decider would be defined. **

A wf C is said to be a consequence in S of a set Γ of wfs if and only if

there is a sequence B1, …, Bk of wfs such that C is Bk and, for each i,

either Bi is an axiom or Bi is in Γ, or Bi is a direct consequence by some

rule of inference of some of the preceding wfs in the sequence. Such a

sequence is called a proof (or deduction) of C from Γ. The members of Γ

are called the hypotheses or premisses of the proof. We use Γ ⊢ C as an

abbreviation for “C is a consequence of Γ”

…

If Γ is the empty set ∅, then ∅ ⊢ C if and only if C is a theorem. It

is customary to omit the sign “∅” and simply write ⊢ C. Thus, ⊢ C is

another way of asserting that C is a theorem. (Mendelson 2015: 28)

Formalism (philosophy of mathematics)

In foundations of mathematics, philosophy of mathematics, and philosophy of logic, formalism is a theory that holds that statements of mathematics and logic can be considered to be statements about the consequences of certain string manipulation rules.

Thus a formalist proof can be considered as finite string transformation rules (in the language of predicate logic) applied to finite strings representing:

(1) A possibly empty set of premises,

(2) A set of axioms,

(3) A set of rules of inference.

deriving a finite string consequence.

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 above provides the conventional basis for the following analysis:**

The key conventional understanding that I have overcome with the following new insights is that some WFF expressions of formal language F may be erroneous in ways that were never previously understood to be erroneous.

The key brand new insight that I bring to the Halting Problem and other undecidable self-referential expressions of formal language is this:

(∀x ∈ Language(F) ( Satisfiable(x) ∨ Falsifiable(x) ∨ ~Sentence(x) ))

If any expression of language does not evaluate to {True, False} then this expression of language is not a sentence of that formal language even if it is a closed WFF of the language.

**Then we apply this key new insight to the Halting Problem where: **

A halt decider H is construed as deriving a formal proof in the language of Turing machine descriptions. The inference steps of this formal proof would be construed as a hypothetical execution trace of the input Turing machine description on its input finite string.

**Defining a Halting Decidability Decider**

No finite sequence of steps satisfies Halts(Ĥ, Ĥ) or satisfies Loops(Ĥ, Ĥ) where the term {satisfies} and the predicates Halts() and Loops() are mathematical. The predicates Halts() and Loops() correspond predicate logic True and False, thus the unsatisfiability of Halts() and Loops() indicates that Ĥ does not specify a logic sentence.

**Copyright 2018 Pete Olcott**

Mendelson, Elliott 2015.

Introduction to Mathematical logic Sixth edition.

1.4 An Axiom System for the Propositional Calculus: 28 CRC Press