0
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ This is complete nonsense. $\endgroup$
    – user21820
    Feb 1 at 5:27

3 Answers 3

0
$\begingroup$
  • 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.

$\endgroup$
4
  • $\begingroup$ I think I should back up. I have a distinct memory of a developer of CoQ telling me that the kernel of CoQ was written in a strongly renormalizing rewrite system EXACTLY BECAUSE it was proven to halt. That this kernel is at the base of all other systems and that the developers took pains to make sure that it is walled off so that nothing but this strongly normalizing rewrite system was allowed. The upshot was that, "On the basis that we haven't made any bugs in the kernel, therefore CoQ can be shown to halt." or something to that effect. $\endgroup$
    – user3074
    Dec 6, 2023 at 13:50
  • $\begingroup$ This is I believe where I understood this from: lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf $\endgroup$
    – user3074
    Dec 6, 2023 at 18:50
  • $\begingroup$ Yes, Coq does pin some aspects of its soundness proof on normalization, but Coq is also a complex theory and proofs in the literature don't necessarily apply to everything Coq can do in practice. This is not the case for all systems, and in particular Lean does not depend on strong normalization for its soundness argument. Also note: "strongly normalizing rewrite system EXACTLY BECAUSE it was proven to halt." - this is tautological, if it is strongly normalizing then reduction halts by definition. But maybe you should consider why you think halting is important? $\endgroup$ Dec 7, 2023 at 1:29
  • $\begingroup$ Yes, I think I may have placed too much import on the fact that constructive logical systems - when embodied by computational systems always halt because they are type checked. For me it has always seemed a hugely important fact that you can't build a non-halting program in a constructive system. If I tried to explicitly program a non-halting program in the simple typed lambda calculus or any of the systems in the lambda cube I couldn't do it because they are all strongly normalizing. $\endgroup$
    – user3074
    Dec 7, 2023 at 3:11
0
$\begingroup$

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.

$\endgroup$
17
  • $\begingroup$ Would you agree with this alternative formulation, “ Is it correct that the omission of indirect proof is the distinguishing characteristic of constructive logic as opposed to classical?” $\endgroup$
    – user3074
    Dec 6, 2023 at 13:13
  • $\begingroup$ "There is a common misunderstanding that constructive mathematics is just mathematics without proofs by contradiction (reductio-ad-absurdum arguments). This is not the case." I'd suggest you do read that SEP article (the first link in my answer). $\endgroup$ Dec 6, 2023 at 13:21
  • $\begingroup$ That article is in-artfully worded. "Proof by contradiction" can mean two things in the common literature: indirect proof, or refutation by contradiction. Constructive logic is exactly that logic you get by disallowing the former, but allowing the latter. If this is incorrect, then I've royally misunderstood something, but I'm like 99.9999% confident that at least this is true so please check carefully and see if I'm wrong. $\endgroup$
    – user3074
    Dec 6, 2023 at 13:44
  • $\begingroup$ IMO, you just keep missing the point, but I have already said it in my answer: what "constructive" actually means, etc. Indeed, if not even SEP is good enough for you, I just wouldn't know what to add. $\endgroup$ Dec 6, 2023 at 13:56
  • 1
    $\begingroup$ The nuance in this answer is, I imagine, motivated by the fact that there are several other propositions that are considered non-constructive, but are weaker than LEM. A comment by Andrej Bauer gave one, the limited principle of omniscience. There are several ways to weaken that further that are still considered non-constructive. LEM is the easiest to state, and makes sense in propositional logic. But in richer systems, it isn't the only non-constructive principle. $\endgroup$
    – Dan Doel
    Dec 6, 2023 at 20:45
0
$\begingroup$

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.

$\endgroup$
12
  • $\begingroup$ I know my complexity theorist is very deeply interested in the halting problem and Turing machines. Are you saying he can safely ignore the omission of LEM in consideration of the halting problem? That constructive logic/mathematics/etc has nothing to say about the halting problem? Thank you very much for answering btw. I deeply appreciate you taking the time as an expert in such questions. $\endgroup$
    – user3074
    Dec 6, 2023 at 14:52
  • $\begingroup$ There is no LEM in the usual consideration of the halting problem! Show me a proof that uses LEM or one of its equivalent forms in the proof that the halting oracle does not exist, please. $\endgroup$ Dec 6, 2023 at 14:56
  • 1
    $\begingroup$ Correct. For example this Wikipedia proof is constructively valid, even though it uses the phrase "proof by contradiction" (it links to the page where it is explained that "proof by contradiction" has several meanings, and the one used in the proof of non-existence of the halting oracle is just "proof of negation".) $\endgroup$ Dec 6, 2023 at 15:00
  • 1
    $\begingroup$ By the way, there is another sense in which the halting oracle is related to excluded middle. Namely, the principle LPO (an instance of excluded middle) is invalid in certain realizability toposes because the halting oracle does not exist. I belive this is closer to what you had in mind, namely a Curry-Howard interpretation of LEM (or some instance of it) whose computational meaning essentially yields a halting oracle. $\endgroup$ Dec 6, 2023 at 15:08
  • 2
    $\begingroup$ Here is an Agda formalization of the proof that the halting problem is undecidable. Here is a formalization of the Scott-Curry theorem for untyped lambda calculus, and a corollary that normalization is undecidable. Neither use excluded middle. $\endgroup$
    – Dan Doel
    Dec 6, 2023 at 16:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.