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?