Halting decidability decider defined

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