I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum:
It was recently said to me by a prominent mathematician, who I deeply deeply respect, to the effect that they have never seen any benefit to denying LEM for any question which they care about. This person is at the very forefront of their field in computational complexity theory. I couldn't understand this given the following:
Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical?
Is it correct that the Curry-Howard correspondence is conditioned on the omission of LEM?
Is it correct that were LEM used in the heart of CoQ and LEAN that in turn these proof checkers would not be proven to halt?
Is it correct that therefore to conclude that it is LEM that is at the heart of the halting problem?
Is it correct that what distinguishes the untyped lambda calculus (which can model turing machines) from the simply typed lambda calculus (which is guaranteed to always halt) must at the heart be LEM?
It is my understanding that LEM is at the heart of the halting problem precisely because it allows double negation elimination aka indirect proof. It allows to assign a positive truth value to something indirectly by showing its opposite leads to contradiction. Modern proof assistants always halt precisely because they do not allow this indirect proof.
I've always conjectured that the only programs that do not halt are ones that try and make use of indirect proof. Ascribing an affirmative truth value only through showing its opposite leads to contradiction. That while the simply typed lambda calculus is strictly weaker than the untyped lambda calculus (and thus not turing complete) it is only those programs that use indirect proof that are omitted.
The conjecture is based on the following:
- A key distinguishing characteristic of the simply typed lambda calculus and untyped lambda calculus is that the former halts (it is strongly normalizing), but the latter is not guaranteed to.
- The key thing that makes the simply typed lambda calculus guaranteed to always halt is the type checker.
- The type checker is based on the Curry-Howard correspondence where types have to be built constructively aka proven.
- The type checker is therefore programmed using the rules of constructive logic.
- The key distinguishing characteristic of constructive logic is the omission of double negation elimination (aka indirect proof).
- Therefore it is the omission/inclusion of double negation elimination that distinguishes systems that always halt versus ones that are not guaranteed to halt.
Thus double negation elimination aka indirect proof is at the heart of the halting problem.
Have I got the above right? Maybe it is a bit hand wavy, but is there any obvious big error(s) here?