16
$\begingroup$

I was wiki-wandering on the articles of Curry-Howard correspondence (link here) and found some statements that get me thinking.

It says that:

Howard made explicit in 1969 a syntactic analogy between the programs of simply typed lambda calculus and the proofs of natural deduction.

Then, when I turn to wiki page of simply typed lambda calculus (link here ), it says:

it is decidable whether or not a simply typed lambda calculus program halts.

Then, it makes me conclude that natural deduction is decidable.

This is very strange, since there is the famous result that says first order logic is undecidable (and also intuitionistic logic).

It seems to me that the correspondence must be restricted to some parts of natural deduction.

Does Curry-Howard correspondce implies decidibility of natural deduction? If no, what is happening?

$\endgroup$
1
  • 4
    $\begingroup$ What makes you think that halting of a program corresponds to existence of a proof? $\endgroup$
    – Alex Kruckman
    Apr 22, 2022 at 0:58

1 Answer 1

Reset to default
15
$\begingroup$

First, the simply typed lambda calculus is actually equivalent to propositional logic, which is decidable. In order to add quantifiers, which boost the power of the calculus to predicate logic (which is undecidable), we have to add dependent types, which are not usually considered part of the "simply typed" lambda calculus.

That said, Martin-Löf Type Theory, which does have these extra features, and can model full first order logic, still has decidable halting problem! Why is this? Surprisingly, it's true for the stupidest possible reason:

Every program halts!

Indeed, Martin-Löf type theory is not turing complete, and can't implement full recursion. There are no looping programs at all!

But why does this not say anything about decidability of predicate logic? This is best cleared up with the mantra

Types are Propositions and Programs are Proofs

Searching for whether a proposition is true is asking whether there exists a program of a certain type! It has nothing to do with whether such a program loops or halts. The PL-theoretic analogue of proof search is called the Type Inhabitation Problem, and this is well known to be undecidable in general, and extremely hard in the cases where it's not undecdiable.

For instance, the problem is decidable in the case of the simply typed lambda calculus (which makes sense, since propositional logic is decidable using truth tables). But the inhabitation problem for this calculus is PSPACE-complete.

I hope this helps ^_^

$\endgroup$
2
  • $\begingroup$ About the last paragraph and "propositional logic is decidable using truth tables": is it really possible to decide intuitionistic propositional logic using truth tables? Can't we only decide classical propositional logic using tables? The only proof I've even seen to decide IPL searches cut-free derivations in Gentzen's sequents -- other algorithms likely exist, but I wonder if tables can be used somehow. $\endgroup$
    – chi
    Apr 22, 2022 at 17:13
  • 2
    $\begingroup$ @chi -- good point! Truth tables per se don't work for IPL, but IPL has the finite model property with respect to kripke frames. Then we get decidability by searching for a proof of $\varphi$ and searching for a (finite!) countermodel in parallel. This is spiritually similar to truth tables, in the sense that we're leveraging semantics to get a proof theoretic result. For modal logic we can actually bound the size of a hypothetical countermodel, which lets us avoid the proof search half of the above algorithm. I suspect by embedding IPL into S4 this will work for IPL too. $\endgroup$
    – HallaSurvivor
    Apr 23, 2022 at 1:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .