Does the Curry-Howard correspondence imply decidibility of natural deduction? 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?
 A: 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 ^_^
