Let me stress that for all these systems the Curry - Howard isomorphism still holds. We may call it also the propositions-as-types property. For any of the logics we mentioned - the propositional, the propositional second or higher-order, the predicate logic - we have that a formula A is provable in the logic iff there is a l-term M -extracted from the proof of A - for which we prove that has type A. And this is a very strong correspondence that embodies the Curry - Howard correspondence.

---