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

Question

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.

Answer 1

As DanielV and spaceisdarkgreen state, there are two ways you can use the simply typed lambda calculus. One way is to use it as a proof theory via propositions-as-types (i.e. Curry-Howard), the other is to consider the equational theory with lambda terms as terms.

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.

Summarizing, in the former view the logic is about arbitrary propositions and the lambda terms corresponds to proofs of those propositions. In the latter view, the logic is about lambda terms, i.e. you prove facts about lambda terms, e.g. whether two are equal.