# A confusion about Church's simple theory of types and the Curry-Howard isomorphism

I am confused about Church's simply typed lambda calculus and the Curry-Howard isomorphism.

Church's simply typed lambda calculus in the paper cited above is given a classical proof theory, in that on p. 4 of the PDF above (p. 58 of the original article) we have the classical definitions of disjunction, conjunction and existential quantification.

Later authors (Henkin in Completeness in the Theory of Types and A Theory of Propositional Types) follow suit; section §4 of the latter article building up the connectives via $\top$ and $\bot$ with a classical disjunction (see 4.5 of section §4). Henkin's type theory is classical in its proof rules and its semantics.

However, the simply typed lambda calculus is usually taken to correspond syntactically via the Curry Howard isomorphism to intuitionistic propositional logic.

Given the classical behaviour, proof-theoretically, of Church's original simply typed lambda calculus in the above article, how is this correspondence achieved with intuitionistic logic? Do the simply typed lambda calculi of Henkin and Church correspond to the Intuitionistic propositional calculus? Can we have the simply typed lambda calculus with classical proof rules and a classical semantics corresponding to intuitionistic propositional logic.

What would the law of the excluded middle in the simply typed lambda calculus of the Church or Henkin variety described correspond to on the logic side of the Curry Howard isomorphism?

If someone could clarify where I am going wrong I would be very happy.

• Church's simple type theory, and the Type Theory that arises from the Curry Howard isomorphism are 2 completely different things. It is unfortunate that they share the same name. In Church's simple type theory, all theorems are typed lambda expressions. In C.H. type theory, all proofs are typed lambda expressions. – DanielV Mar 31 '18 at 16:52
• Can you give me a reference where this is discussed? As far as I was aware, Church's version of the simply typed lambda calculus does correspond to Intuitionistic propositional logic. What distinction are you drawing between the simply typed lambda calculus and Church's simple type theory? Where can I read about this? – user65526 Mar 31 '18 at 17:14
• @user65526 I don't know if I'd say they're 'completely different things' but certainly agree there's an important distinction Daniel is making. The 'intuitionistic propositions' on one end of the CH correspondence correspond to the types in the lambda calculus. The propositions of the embedded classical logic here, on the other hand, are terms of a particular type. What CH says here is that an inhabited type corresponds to a valid proposition. A classic example is the existence of the term Church calls $K_{\alpha\beta\alpha}$ means $A\to (B\to A)$ is an intuitionistically valid prop. – spaceisdarkgreen Mar 31 '18 at 18:14
• @user65526 In other words the intuisitionistic implicational logic and the classical logic are "completely different things" in that they play completely different roles here (and of course they also are completely different logics). But the CH correspondence does apply to Church's types here. But to add to what I said above, a proof of one of the valid intuititionistic propositions corresponds to a type inference on a term, not to one of the proofs done in the proof theory described – spaceisdarkgreen Mar 31 '18 at 18:23
• I'm not 100% crystal clear I understand. Could you please either give a full answer, or cite some relevant literature where this distinction is made? – user65526 Mar 31 '18 at 22:34

In the former view, we think of a type as representing a proposition and that proposition has a proof if and only if there is a lambda term of that type. This is the propositions-as-types/Curry-Howard perspective. We can prove that there is a one-to-one correspondence between the types, terms, and term reductions of the simply typed lambda calculus and the propositions, natural deduction proofs, and proof rewrites of the natural deduction presentation of minimal/intuitionistic propositional logic. $$\beta$$-reduction corresponds to local soundness, and $$\eta$$-expansion to local completeness.
In the latter view, used by e.g. the HOL family of theorem provers and described in The Seven Virtues of Simple Type Theory, the simply typed lambda terms are just terms in an equational logic. In this case, a proof is a proof in this logic which can be classical or intuitionistic or whatever. Typically it is classical and a Boolean type $$\mathbb B$$ is added with axioms to ensure that it has only two values, $$\mathsf{F}$$ and $$\mathsf{T}$$. We can then identify propositions with terms of type $$\mathbb B$$, and more generally, predicates with terms of type $$(\tau_1\to(\tau_2\to\cdots(\tau_n\to\mathbb B)\cdots))$$. Due to the use of higher-order terms (lambda terms), just a handful of rules and axioms for equality and Booleans produces a fairly powerful higher-order logic. See sections 2.3.1 and 2.4.3 of the HOL4 Logic manual for details of the deductive system in the case of HOL4 (which actually uses the polymorphic lambda calculus, not the simply typed lambda calculus as that is much more convenient). So in HOL4, the proofs would be deductions in this deductive system.