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.

  • 2
    $\begingroup$ 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. $\endgroup$ – DanielV Mar 31 '18 at 16:52
  • $\begingroup$ 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? $\endgroup$ – user65526 Mar 31 '18 at 17:14
  • 1
    $\begingroup$ @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. $\endgroup$ – spaceisdarkgreen Mar 31 '18 at 18:14
  • 1
    $\begingroup$ @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 $\endgroup$ – spaceisdarkgreen Mar 31 '18 at 18:23
  • $\begingroup$ 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? $\endgroup$ – user65526 Mar 31 '18 at 22:34

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.

  • $\begingroup$ @ Derek Elkins I'll have to check out the reference you cited. If you know any other it would be good to know. What I am gathering so far is that you can have a classical theory (Montague's IL, Gallin's TY2, Church's simple theory of types), whose typing patterns correspond to Intuitionistic propositional logic. What you can't have is a classical logic (on the logic side) which corresponds to to the simply typed lambda calculus, unless you have (certain types of ?) continuations on the lambda side. Is that correct? $\endgroup$ – user65526 Apr 1 '18 at 7:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.