LEM and the curry-howard correspondence

Question

The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus which is guaranteed to halt.

Constructive logic only differs from classical logic in that it omits LEM.

There seems to be a deep connection here between LEM and the non-halting behavior of Turing machines.

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.

I am not a mathematician, but everything I know about the Curry-Howard correspondence, mathematical proof checkers, Homotopy Type Theory, etc is based on constructive logic which in turn only differs from classical logic in that it explicitly omits LEM.

I'm having trouble squaring my own understanding and this mathematicians statement without falling back to that I must be missing something.

So my questions:

• 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:

• They key distinguishing characteristic of the simply typed lambda calculus and untyped lambda calculus is that the former halts, 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.

What am I missing?

Thanks.

Answer 1

I'm in a hurry but will try to answer a couple of your questions:

Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical?

Yes!

Is it correct that the Curry-Howard correspondence is conditioned on the omission of LEM?

In a basic version of the Curry–Howard correspondence, you are quite right: There is no program of the type corresponding to LEM. That would be a kind of oracle which is able, for any type $A$, to either produce a value of $A$ or else produce a procedure $A \to \bot$. In particular, with such an oracle there would be an algorithm deciding the halting problem.

Astoundingly, there are more refined versions of the Curry–Howard correspondence which interpret LEM just fine. Every constructive proof gives rise to a pure program while every classical proof gives rise to a program with side effects. Which side effects exactly, depends on the amount of classical axioms used. For interpreting LEM, to have continuations as side effects is enough. For interpreting countable or dependent choice, other side effects are required. You find some references in these slides.

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?

Literally speaking: No. Coq and Lean support LEM just fine as an unproven assumption and still their proof checking terminates.

Is it correct that therefore to conclude that it is LEM that is at the heart of the halting problem?

Yes in some sense and no in some other.

Yes: Without LEM, it becomes possible for all functions $\mathbb{N} \to \mathbb{N}$ to be computable (by a Turing machine or equivalently by an untyped lambda term). The halting function, which maps a number $n$ to $0$ or $1$ depending on whether the $n$-th Turing machine terminates, is no longer a total function $\mathbb{N} \to \mathbb{N}$ in such a world. (Instead, its domain of definition is the subset consisting of those numbers $n$ such that the $n$-th Turing machine terminates or does not terminate.) Accordingly, the question whether there is a Turing machine computing this no-longer-existing gadget loses a bit of its relevance. There are lots of worlds like this, for instance the "effective topos", I tried to give an introduction here.

No: There is a metatheorem stating that every PA-proof of termination of a Turing machine can be mechanically transformed into a HA-proof, and similarly with ZFC and IZF. (PA is Peano Arithmetic, HA is its constructive cousin without LEM; ZFC is Zermelo–Fraenkel set theory with the axiom of choice, IZF is its constructive cousin without LEM and without choice.) So LEM will never be crucial in proving termination of a Turing machine. LEM might be crucial for abstract tools helping with termination proofs, but in the end LEM can always be eliminated from concrete termination results. Keywords to lookup are "Friedman's trick", "continuation trick" or "Barr's theorem".

Answer 2

The main significance of the fact that proof assistants use constructive, rather than classical, logic is that terms normalize. For example, if you have a closed term of type $\mathbb{N}$ in a constructive proof assistant, the term is guaranteed to simplify down to an actual natural number. This doesn't require any proofs on the part of the user; the program can simply do it. Similarly, if you have a closed term of a sum type, the term is guaranteed to simplify to one of the variants.

In general, it is not possible to get this normalizing behavior when using classical logic because of the incompleteness theorems. In particular, let $\phi$ be a proposition such that there is no closed term of type $\phi$, and there is no closed term of type $\neg \phi$ (such a type exists by Godel's first incompleteness theorem). If LEM is a part of our axiom system, we must have a closed term of type $\phi + \neg \phi$. But this term cannot normalize, since then we would have either a term of type $\phi$, or a term of type $\neg \phi$, neither of which is possible.

We can relate this to the halting problem as follows. Given a Turing machine $T$ and input $i$, we can define a type $\phi(T, i) :\equiv \sum n : \mathbb{N}, \ulcorner T$ halts in exactly $n$ steps when run on input $i \urcorner$. If we had a normalizing, consistent proof assistant with LEM, we could produce a term $W : \prod i : I, \phi(T, i) + \neg \phi(T, i)$ (where $I$ is the input type, perhaps the type of binary strings). To determine whether $T$ halts on $i$, we would simply normalize the term $W(i)$. By the normalization properties, this would either give us some particular $n$ and a term of type $\ulcorner T$ halts in exactly $n$ steps when run on input $i \urcorner$, or it would give us a term of type $\neg \phi(T, i)$.

In the former case, check whether $T$ actually halts in exactly $n$ steps. If it doesn't, then our proof assistant is inconsistent; contradiction. Thus, $T$ does halt in exactly $n$ steps on input $i$.

In the latter case, suppose $T$ halted in exactly $n$ steps on input $i$. Then we could construct a term of type $\ulcorner T$ halts in exactly $n$ steps when run on input $i \urcorner$, and thus a term of type $\phi(T, i)$. But we already have a term of type $\neg \phi(T, i)$, which means our proof assistant is inconsistent; contradiction. Thus, the Turing machine does not halt on input $i$.

Therefore, such a proof assistant would enable us to solve the Halting problem. Since the proof assistant is itself a computable process, this is a contradiction. Note that the proof that the halting problem is unsolvable is (or can easily be made) purely constructive.

However, you don't necessarily need terms to normalize to get a halting proof-checker. Whether you write your formal proofs in set theory, arithmetic, type theory, or any other commonly used system, and whether you use classical logic or not, there should be a computer program which can check, in finite time, whether your proof is valid. The only rub is that you don't get this extremely convenient normalizing behavior unless you use a nice, constructive system.

Finally, a classical proof in Coq of $\phi$ is simply a constructive proof that $LEM \to \phi$. There is nothing magic about $LEM$ or any other axioms here.