Hehner and Stoddart agree that the halting problem has an inconsistent, unsatisfiable specification. Hehner and Macias agree that a key issue with the halting problem is that it requires a: subjective specification(Hehner) / context dependent function(Macias). When a problem has an unsatisfiable specification because this specification is inconsistent then the unsatisfiability of the specification is anchored in its error thus does not actually limit computation.

A pair of C functions are defined such that D has the halting problem proof's pathological relationship to simulating termination analyzer H. When D correctly simulated by H must be aborted to prevent its own infinite execution then H is necessarily correct to reject D as specifying non-halting behavior. This exact same reasoning is applied to the Peter Linz Turing machine based halting problem proof.

A simulating halt decider correctly predicts what the behavior of its input would be if this simulated input never had its simulation aborted. It does this by correctly recognizing several non-halting behavior patterns in a finite number of steps of correct simulation. -/- When simulating halt decider H correctly predicts that directly executed D(D) would remain stuck in recursive simulation (run forever) unless H aborts its simulation of D this directly applies to the halting theorem.

The novel concept of a simulating halt decider enables halt decider H to to correctly determine the halt status of the conventional “impossible” input D that does the opposite of whatever H decides. This works equally well for Turing machines and “C” functions. The algorithm is demonstrated using “C” functions because all of the details can be shown at this high level of abstraction.

MIT Professor Michael Sipser has agreed that the following verbatim paragraph is correct (he has not agreed to anything else in this paper) -------> -/- If simulating halt decider H correctly simulates its input D until H correctly determines that its simulated D would never stop running unless aborted then H can abort its simulation of D and correctly report that D specifies a non-halting sequence of configurations.

The halting theorem counter-examples present infinitely nested simulation (non-halting) behavior to every simulating halt decider. The pathological self-reference of the conventional halting problem proof counter-examples is overcome. The halt status of these examples is correctly determined. A simulating halt decider remains in pure simulation mode until after it determines that its input will never reach its final state. This eliminates the conventional feedback loop where the behavior of the halt decider effects the behavior of its input.

The novel concept of a simulating halt decider enables halt decider H to to correctly determine the halt status of the conventional “impossible” input D that does the opposite of whatever H decides. This works equally well for Turing machines and “C” functions. The algorithm is demonstrated using “C” functions because all of the details can be shown at this high level of abstraction. ---------------------------------------------------------------------------------------------------- ---- Simulating halt decider H correctly determines that D correctly simulated by H would remain stuck in (...) recursive simulation never reaching its own final state. D cannot do the opposite of the return value from H because this return value is unreachable by every correctly simulated D. This same result is shown to be derived in the Peter Linz Turing machine based proof. (shrink)

This is an explanation of a possible new insight into the halting problem provided in the language of software engineering. Technical computer science terms are explained using software engineering terms. No knowledge of the halting problem is required. -/- It is based on fully operational software executed in the x86utm operating system. The x86utm operating system (based on an excellent open source x86 emulator) was created to study the details of the halting problem proof counter-examples at the much higher level (...) of abstraction of C/x86. (shrink)

The halting theorem counter-examples present infinitely nested simulation (non-halting) behavior to every simulating halt decider. Whenever the pure simulation of the input to simulating halt decider H(x,y) never stops running unless H aborts its simulation H correctly aborts this simulation and returns 0 for not halting.

By making a slight refinement to the halt status criterion measure that remains consistent with the original a halt decider may be defined that correctly determines the halt status of the conventional halting problem proof counter-examples. This refinement overcomes the pathological self-reference issue that previously prevented halting decidability.

The conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic property of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide valid the deductive inference. Conclusions of sound arguments are derived from truth preserving finite string transformations applied to true premises.

Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to true conclusions without any need for other representations such as model theory.

Minimal Type Theory (MTT) is based on type theory in that it is agnostic about Predicate Logic level and expressly disallows the evaluation of incompatible types. It is called Minimal because it has the fewest possible number of fundamental types, and has all of its syntax expressed entirely as the connections in a directed acyclic graph.

This sentence G ↔ ¬(F ⊢ G) and its negation G ↔ ~(F ⊢ ¬G) are shown to meet the conventional definition of incompleteness: Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). They meet conventional definition of incompleteness because neither the sentence nor its negation is provable in F (or any other formal system). -- .

Could the intersection of [formal proofs of mathematical logic] and [sound deductive inference] specify formal systems having [deductively sound formal proofs of mathematical logic]? All that we have to do to provide [deductively sound formal proofs of mathematical logic] is select the subset of conventional [formal proofs of mathematical logic] having true premises and now we have [deductively sound formal proofs of mathematical logic].

If the conclusion of the Tarski Undefinability Theorem was that some artificially constrained limited notions of a formal system necessarily have undecidable sentences, then Tarski made no mistake within his assumptions. When we expand the scope of his investigation to other notions of formal systems we reach an entirely different conclusion showing that Tarski's assumptions were wrong.

If there truly is a proof that shows that no universal halt decider exists on the basis that certain tuples: (H, Wm, W) are undecidable, then this very same proof (implemented as a Turing machine) could be used by H to reject some of its inputs. When-so-ever the hypothetical halt decider cannot derive a formal proof from its input strings and initial state to final states corresponding the mathematical logic functions of Halts(Wm, W) or Loops(Wm, W), halting undecidability has been (...) decided. (shrink)

This is an explanation of a key new insight into the halting problem provided in the language of software engineering. Technical computer science terms are explained using software engineering terms. -/- To fully understand this paper a software engineer must be an expert in the C programming language, the x86 programming language, exactly how C translates into x86 and what an x86 process emulator is. No knowledge of the halting problem is required.

To eliminate incompleteness, undecidability and inconsistency from formal systems we only need to convert the formal proofs to theorem consequences of symbolic logic to conform to the sound deductive inference model. -/- Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) thus unlike the formal proofs of symbolic logic provability cannot diverge from truth.

This paper decomposes the Liar Paradox into its semantic atoms using Meaning Postulates (1952) provided by Rudolf Carnap. Formalizing truth values of propositions as Boolean properties of these propositions is a key new insight. This new insight divides the translation of a declarative sentence into its equivalent mathematical proposition into three separate steps. When each of these steps are separately examined the logical error of the Liar Paradox is unequivocally shown.

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. -/- By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that evaluate to neither True nor False.

We can simply define Gödel 1931 Incompleteness away by redefining the meaning of the standard definition of Incompleteness: A theory T is incomplete if and only if there is some sentence φ such that (T ⊬ φ) and (T ⊬ ¬φ). This definition construes the existence of self-contradictory expressions in a formal system as proof that this formal system is incomplete because self-contradictory expressions are neither provable nor disprovable in this formal system. Since self-contradictory expressions are neither provable nor disprovable (...) only because they are self-contradictory we could define them as unsound instead of defining the formal system as incomplete. (shrink)

Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language. -/- The only thing required to eliminate incompleteness, undecidability and inconsistency from formal systems is transforming the formal proofs of symbolic logic to use the sound deductive inference model.

The conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic value of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide the valid deductive inference. Sound deductive conclusions are the result of these finite string transformation rules.

A Simulating Halt Decider (SHD) computes the mapping from its input to its own accept or reject state based on whether or not the input simulated by a UTM would reach its final state in a finite number of simulated steps. -/- A halt decider (because it is a decider) must report on the behavior specified by its finite string input. This is its actual behavior when it is simulated by the UTM contained within its simulating halt decider while this (...) SHD remains in UTM mode. (shrink)

Within the (Haskell Curry) notion of a formal system we complete Tarski's formal correctness: ∀x True(x) ↔ ⊢ x and use this finally formalized notion of Truth to refute his own Undefinability Theorem (based on the Liar Paradox), the Liar Paradox, and the (Panu Raatikainen) essence of the conclusion of the 1931 Incompleteness Theorem.

Both Tarski and Gödel “prove” that provability can diverge from Truth. When we boil their claim down to its simplest possible essence it is really claiming that valid inference from true premises might not always derive a true consequence. This is obviously impossible.

Hypothesis: WFF(x) can be applied syntactically to the semantics of formalized declarative sentences such that: WFF(x) ↔ (x ↦ True) ∨ (x ↦ False) (see proof sketch below) For clarity we focus on simple propositions without binary logical connectives.

When we understand that every potential halt decider must derive a formal mathematical proof from its inputs to its final states previously undiscovered semantic details emerge. -/- When-so-ever the potential halt decider cannot derive a formal proof from its input strings to its final states of Halts or Loops, undecidability has been decided. -/- The formal proof involves tracing the sequence of state transitions of the input TMD as syntactic logical consequence inference steps in the formal language of Turing Machine (...) Descriptions. (shrink)

This is the formal YACC BNF specification for Minimal Type Theory (MTT). MTT was created by augmenting the syntax of First Order Logic (FOL) to specify Higher Order Logic (HOL) expressions using FOL syntax. Syntax is provided to enable quantifiers to specify type. FOL is a subset of MTT. The ASSIGN_ALIAS operator := enables FOL expressions to be chained together to form HOL expressions.

An abstract machine having a tape head that can be advanced in 0 to 0x7FFFFFFF increments an unlimited number of times specifies a model of computation that has access to unlimited memory. The technical name for memory addressing based on displacement from the current memory address is relative addressing.

Minimal Type Theory (MTT) shows exactly how all of the constituent parts of an expression relate to each other (in 2D space) when this expression is formalized using a directed acyclic graph (DAG). This provides substantially greater expressiveness than the 1D space of FOPL syntax. -/- The increase in expressiveness over other formal systems of logic shows the Pathological Self-Reference Error of expressions previously considered to be sentences of formal systems. MTT shows that these expressions were never truth bearers, thus (...) never sentences of any formal logic system. (shrink)

When we look at 800,000 year ice core data CO2 levels since 1950 have risen at a rate of 123-fold faster than the fastest rate in 800,000 years. When we see that this rise is precisely correlated with global carbon emissions the human link to climate change seems certain and any rebuttal becomes ridiculously implausible. The 800,000 year correlation between CO2 and global temperatures seems to be predicting at least 9 degrees C of more warming based on current CO2 levels.

Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to deductive conclusions without any need for other representations.

The fail-safe makes sure the fee is high enough to meet carbon emission reduction targets. The safeguard keeps the fee from getting any higher than needed. -/- One of the ways that we could account for the unpredictability of the price elasticity of demand for carbon would be to provide a fail-safe mechanism to ensure that we definitely stay on the carbon reduction schedule. If we keep Energy Innovation Act (HR 763) essentially as it is and scale up the annual (...) carbon fee increase by Number-of-Years-Behind-Schedule * 0.15. (shrink)

The generalized conclusion of the Tarski and Gödel proofs: All formal systems of greater expressive power than arithmetic necessarily have undecidable sentences. Is not the immutable truth that Tarski made it out to be it is only based on his starting assumptions. -/- When we reexamine these starting assumptions from the perspective of the philosophy of logic we find that there are alternative ways that formal systems can be defined that make undecidability inexpressible in all of these formal systems.

By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that have the semantic error of Pathological self-reference(Olcott 2004). The foundation of this system requires the notion of a BaseFact that anchors the semantic notions of True and False. When-so-ever a formal proof from BaseFacts of language L to a closed WFF X or ~X of language L does not exist X is decided to be semantically (...) incorrect. (shrink)

We begin with the hypothetical assumption that Tarski’s 1933 formula ∀ True(x) φ(x) has been defined such that ∀x Tarski:True(x) ↔ Boolean-True. On the basis of this logical premise we formalize the Truth Teller Paradox: "This sentence is true." showing syntactically how self-reference paradox is semantically ungrounded.

One of the ways that we could account for the unpredictability of the price elasticity of demand for carbon would be to provide a fail-safe mechanism to ensure that we definitely stay on the carbon reduction schedule. If we kept Energy Innovation Act (HR 763) essentially as it is and scale up the annual carbon fee increase by Number-of-Years-Behind-Schedule * 0.15.