LEM, the halting problem, the curry-howard correspondence -> deep connection?

Question

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?

Answer 1

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

Not exactly, there do exist ways to transport LEM (or more naturally, Peirce's law) across the Curry-Howard correspondence using undelimited continuations and call/cc. But this is mostly true.

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

(This question presupposes that Coq and Lean have been proven to halt, which I think is not the case. Large subsystems of both systems have been proven to halt but AFAIK termination of the type system for the full theory is still an open question, although it looks more likely to be true for Coq than for Lean.)

There are two issues with this line of questioning:

• It is possible to introduce LEM as an axiom without impacting termination of the type checker. In fact this is done in both Coq and Lean, and classical mathematics can be done in both systems.

• Just because the type checker is non-terminating does not mean it is inconsistent. Normally you would call it "proof search" in that case, but SMT solvers generally have exactly this behavior - they may not (and generally will not) terminate without an explicit timeout, but when they do find a proof the theorem is true. (This is being rather optimistic about the non-existence of bugs in the solver.)

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

I suppose you could say this, although it is amusing to run this example with the call/cc-based proof of LEM. A halting oracle using LEM will, given any program, return "no, program P does not halt" (that is, a function of the form A -> False where A is "P halts". You may, however, become suspicious of this quick response, and try to catch it in a lie, by saying "Are you sure? Because I have a proof of P halting right here: p : A". At this point the halting oracle will take your proof and time-travel to the point of the original question, and now return "Yes, P halts, here is a proof: p : A".

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

I don't think this correspondence exactly holds, there exist more levels of complexity between STLC and Turing-complete, and Coq and Lean both lie in that middle ground. And as mentioned you can have LEM and still have a halting typechecker.

I've always conjectured that the only programs that do not halt are ones that try and make use of indirect proof.

I don't think this is true in the most literal interpretation of Curry-Howard. Most programs that loop are making use of inconsistent axioms like fix : (A -> A) -> A. If you are going to make a comparison between programs and proofs it would be closer to this - the Turing-complete languages have inconsistent (in the logical sense) type systems. (I'm not sure this statement is true in general either, although it does seem to be true in most cases in practice.)

---

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.

Let's come back to this statement. This person is speaking as a mathematican, which is to say they are evaluating the usefulness of denying LEM with regards to conducting proofs, and in this case there is no direct benefit to denying a principle that is true even if it is not something you could normalize in the style of lambda calculus, because this is not an activity that mathematicians do in the vast majority of cases.

If statements are given meaning by directly embedding them in a model rather than by normalizing them and interpreting the normal forms, then it is possible to ascribe meaning even to expressions that you would consider non-terminating. In ZFC, we generally do not even have a built-in notion of reduction of expressions, expressions simply are and have some interpretation. The expressions may have equalities to other expressions but there is no particular directionality to this, and you can rewrite an expression to an infinite sequence of larger expressions but this poses no problem for modeling. In this context, having a theory with a strongly normalizing rewrite system on top is a nice-to-have but by no means a requirement. ZFC is trivially strongly normalizing because everything halts immediately.

The whole concept of applying Curry-Howard isomorphism to the logical system is foreign to most traditional mathematics (yes, even computer science and complexity theory). It is popular in proof assistants primarily because type systems are useful in programming languages for other reasons and so this is a nice way to get a proof system "for free" from your type system. But there also exist proof systems not based on dependent type theory, and these generally do not use reduction-in-the-kernel in any load-bearing way.

Answer 2

Complexity theory in general has very low logical complexity. Almost all of it can be expressed in Peano arithmetic, and often in much weaker fragments of arithmetic. Furthermore, the most interesting questions in complexity theory themselves have low logical complexity. There are meta-theorems in logic which explain that under these circumstances excluded middle is simply not an important consideration.

For example $\mathrm{P} \neq \mathrm{NP}$ is equivalent to a $\Pi^0_2$-sentence ("For all machines $M$ and polynomials $p$, there is an instance $\phi$ of SAT such that $M$ does not correctly solve $\phi$ within $p(|\phi|)$ steps".) By a theorem of Friedmann's, Peano arithmetic is conservative over Heyting arithmetic (which is Peano arithmetic without excluded middle) for $\Pi^0_2$ sentences, so Peano arithmetic and Heyting arithmetic agree on the answer to $\mathrm{P} \neq \mathrm{NP}$.

It is therefore possible to give a well-reasoned argument in favor of excluded middle in complexity theory, although of course we cannot speculate on what grounds your secret prominent mathematician holds their opinion. In Slovenian we have a saying: “An old habit is an iron shirt.”

P.S. Please note that the usual proof of the non-existence of the halting oracle is constructively valid, contrary to how one might understand your writing "LEM is at the heart of the halting oracle". Consequently, if you write down the stament "there is no Turing machine which decides the halting of Turing machines" and interpret it a la Curry-Howard, you can prove it by giving a suitable constructive proof term. However, the related but more abstract statement ”every infinite binary sequence contains a $1$ or it does not” (known as the Limited principle of omniscience) is neither provable nor refutable in type theory.

Answer 3

I'll just try and address some of the more basic points, I'll let others deal with the more technical details related to proof assistants (see Mario Carneiro's answer for example):

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

No, that's at best a simplification: "Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “we can construct”. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions." https://plato.stanford.edu/entries/mathematics-constructive/

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

No, the Curry-Howard correspondence was born for intuitionistic logic, but is not in fact limited to it: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Classical_logic_and_control_operators

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

No, besides that LEM is not really at the heart of anything, as the above should make clear, the halting problem is not that some programs do not terminate on some inputs, it's about the impossibility of a general halt decider, i.e. a program that, for any pair program-input, can tell whether or not that program will halt on that input.

• It is my understanding that LEM is at the heart of the halting problem precisely because it allows double negation elimination aka indirect proof.

LEM is fine when all propositions are indeed decidable, so, literally, for all P, P or not P: but that is very rarely the case. It also allows the non-expert very easy mistakes: imagine teaching logic to a kid and saying "if you don't see that it is raining, then you can safely conclude that it is not raining." Except, can you? And that is LEM in a nutshell: handle with care.

Answer 4

You forgot to say, for the benefit of others, what LEM is, because "LEM" sounds like something NASA might use for moon missions to those who aren't clued in on the insider-language. You're talking about the classical assertion $$⊢ a ∧ ¬a$$

I won't answer the full question, but will address a key element of it.

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

Not at all, for one very simple reason: neither "false" ($⊥$) nor "not" ($a ↦ ¬a$) are involved in the distinction between classical versus non-classical logic, and are not even needed to make the distinction between the two!

In particular, you can already make the distinction between classical versus intuitionist logic even with minimal logic, where there is nothing but the conditional operator ($a, b ↦ a ⊃ b$) ... which I'll adopt the convention of associating to the right for the sake of discussion ($a ⊃ b ⊃ c = a ⊃ (b ⊃ c)$).

Add in the following axiom $$μ: ((a ⊃ b) ⊃ b) ⊃ (b ⊃ a) ⊃ a$$ and you have a classical version of this logic.

If you allow in the $a, b ↦ a ∨ b$ operator, you can still express the classical versus non-classical distinction without the $a ↦ ¬a$ operator, using an axiom such as $$γ: (((a ⊃ b) ⊃ c) ⊃ a ⊃ c) ⊃ a ⊃ b ∨ c.$$

How do we know they're classical? Truth tables show they're classically valid. Embedding them in intuitionistic logic; i.e. expanding the minimal logic by adding in all the other connectives and constants, shows they're not intuitionistically valid. Taking $b = ⊥$, and using the equivalences $⊥ ⊃ x = ⊤$, $⊤ ⊃ x = x$ and $x ⊃ ⊥ = ¬x$, the $μ$ axiom instantiates to: $$ μ: ((a ⊃ ⊥) ⊃ ⊥) ⊃ (⊥ ⊃ a) ⊃ a = (¬a ⊃ ⊥) ⊃ ⊤ ⊃ a = ¬¬a ⊃ a. $$ Taking $a = ⊤$ and $c = ⊥$, and using the same equivalences along with the equivalence $x ∨ ⊥ = x$, the $γ$ axiom instantiates to: $$ γ: (((⊤ ⊃ b) ⊃ ⊥) ⊃ ⊤ ⊃ ⊥) ⊃ ⊤ ⊃ b ∨ ⊥ = ((b ⊃ ⊥) ⊃ ⊥) ⊃ ⊤ ⊃ b = ¬¬b ⊃ b. $$ Yet, there is no $⊢ a ∨ ¬a$ in either version of logic, because there is no $¬(\_)$ in either logic here, nor any $(\_)∨(\_)$ in minimal logic.

The fact that you can express "classicality" without any use of $¬$ (or even $∨$) is a key element of the ability to expand the coverage of the Curry-Howard correspondence to classical logic ... which invariably brings the concept of "continuations" onto the scene.

Another way the classical versus non-classical distinction shows up is in the expansion of "modus ponens" to "modus ponens with continuation". Just as you already have the following extension of modus ponens with "left continuation": $$(c ∧ a) ⊃ b = c ⊃ (a ⊃ b),$$ available intuitionistically, you can also consider modus ponens with "right continuation" $$a ⊃ (b ∨ d) = (a ⊃ b) ∨ d,$$ which is classical, but not intuitionistic, nor is the version with two-sided continuation $$(c ∧ a) ⊃ (b ∨ d) = c ⊃ ((a ⊃ b) ∨ d).$$ Neither involves the $¬$ operator or the $⊥$ constant, so they can be formulated in a logic that has no $¬$ or $⊥$, but we can tell it's classical, because if we add these to the logic and use the same equivalences as before (particularly, $⊤ ⊃ x = x$), along with the equivalences $⊤ ∧ x = x$, $⊥ ∨ x = x$ and $x ⊃ x = ⊤$, then setting $c = ⊤$, $b = ⊥$ and $d = a$, we get: $$ (⊤ ∧ a) ⊃ (⊥ ∨ a) = ⊤ ⊃ ((a ⊃ ⊥) ∨ a),\\ a ⊃ a = ⊤ ⊃ (¬a ∨ a),\\ ⊤ = ¬a ∨ a. $$

This makes it clear that LEM, as you call it, is directly connected with the right-continuation $d$, and that this is the actual root of the classical versus non-classical distinction. In sequent form, the modus ponens rule with two-sided continuation takes on a form as the following equivalence between sequents: $$ 𝔛, a ⊢ b, 𝔜 ⇔ 𝔛 ⊢ a ⊃ b, 𝔜 $$ with left continuation (a.k.a. "context") $𝔛$ and right continuation $𝔜$.

Answer 5

Let me answer this question tangentially: while in our world the LEM may seem an unobjectionable and harmless principle, there are "worlds" where the LEM is false.

In the normal mathematical world, we just assume that some things exist. For example, piecewise functions exist: I can define a function $f : \mathbb{R} \rightarrow \mathbb{R}$ by $f(x) = 0$ if $x \leq 0$, $f(x) = x$ if $x > 0$. Given any two real numbers $a$ and $b$, precisely one of $a < b$, $a = b$ or $a > b$ is true. Some functions are provably discontinuous. Noncomputable functions from $\mathbb{N}$ to $\mathbb{N}$ exist and cam be defined. Everything seems perfectly normal, right?

But this is not the only "mathematical world" that exists. There are other mathematical worlds out there. There is a world where all functions from $\mathbb{R}$ to $\mathbb{R}$ are not only continuous but smooth; however, of course this necessitates that piecewise functions could not exist. There is a world where all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable, and this necessitates that the Busy Beaver and other non-computable functions are undefinable. Of course, all of these nice properties necessitate that the LEM fails to hold.

More formally speaking, the mathematical worlds I've been talking about are the concept of (elemantary) toposes. Each topos has an internal language, where mathematics can be conducted; depending on your topos, however, the internal language may validate or fail to validate statements that may seem bonkers.

Now, by the Curry-Howard correspondence, each of the internal languages could be used as a programming language. This is the beginnings of type theory. In some of them, there exist oracles for things that are not explicitly computable, and the law of excluded middle is just one of them. Recall that the LEM has the type: $\forall P : \mathtt{Prop}, P \vee \neg P$; by Curry-Howard, it is a function that, when given a proposition $P$, returns either a proof that either $P$ is true or that $\neg P$ is true. Of course, it is impossible to write down the definition of this function via recursion, which can be done in any topos with enough structure (if it were possible, then all toposes admit the LEM, which is not the case!). But still we can allow this principle as a function that defines itself.

So, LEM and Curry-Howard are not really directly related. It's not right to think of Curry-Howard as a specific statement, but rather as a broad principle. In some toposes, the internal language actually does allow you to write functions to decide whether a Turing machine halts - they just aren't computable in the usual sense. Meanwhile there are a plethora of reasons why internal functions in toposes can fail to be computable, again in the usual sense, and the LEM is just one of them; it is nothing special.

If you want to learn more about this subject, I suggest reading Mac Lane & Moerdijk's Sheaves in Geometry and Logic, which is a fantastic introduction to topos theory. Also, you may be interested in the effective topos.