Lecture Notes onThe Curry-Howard Isomorphism15-312: Foundations of Programming LanguagesFrank PfenningLecture 23November 18, 2004In this lecture we explore an interesting connection between logic andprogramming languages. In brief, logical proofs embody certain construc-tions which may be interpreted as programs. Under this interpretation,propositions become types. It was first observed by the logicians HaskellCurry [˜1960] and William Howard [˜1969] in different contexts that this isin fact an isomorphism: in a certain fragment of logic, every proof describesa program and every program describes a proof.We will make the same observation here, using the methodology ofjudgments that we have used to far in the course, applied to the devel-opment of principles of logical reasoning. This formulation is due to PerMartin-L¨of [˜1983].What is the meaning of a proposition? Martin-L¨of argues that to under-stand the meaning of a proposition means to understand when it is true.Consequently, in order to explain the meaning of a logical connective, wehave to explain how to derive that a proposition with this connective istrue.Thus the most basic of all judgments of logic is that of truth, written asA true.As the simplest example of a connective, consider conjunction. We saythat A ∧ B true if A true and B true. Written as an inference rule:A true B trueA ∧ B true∧IWe refer to this as an introduction rule because it introduces a connectivein the conclusion (here ‘∧’). The introduction rule tells us how to concludethat A ∧ B is true, thereby defining its meaning.LECTURE NOTES NOVEMBER 18, 2004L23.2 The Curry-Howard IsomorphismThe next question is how can we use the information that A ∧ B true.According to the above explanation, if we know A ∧ B true, we shouldknow the two premises, that is A true and B true.A ∧ B trueA true∧E1A ∧ B trueB true∧E2We refer to these as elimination rules, because they eliminate a connective inthe premise (here ‘∧’).If we think of the introduction rule as defining the meaning of the con-nective, how do we know that the elimination rules that we developedfrom it are actually correct? We will consider this question later in thislecture by introducing the notions of local soundness and completeness ofthe rules. For now, we continue by filling out the store of available logicalconnectives.The next one we want to consider is implication. When is A ⊃ Btrue? From our experience with proofs we know that in order to concludeA ⊃ B true we assume that A is true and try to prove that B is true. Ifwe want to take this as a definition, we need a hypothetical judgment. Wewrite A1true, . . . , Antrue ` A true for such a hypothetical judgment withassumptions A1true through Antrue. We abbreviate a collection of hy-potheses with H. From the nature of reasoning from hypotheses we obtainfor free a hypothesis rule and a substitution principle.H1, A true, H2` A trueHypUnfortunately, there is a small ambiguity here: there may be severalhypotheses A true and from the form of the rule above we cannot tell whichone was meant. In order to make this unambiguous we record the numberof the assumption that was used.Hypothesis rule.A1true, . . . , Aitrue, . . . , Antrue ` AitrueHypiSubstitution principle.If H1` A true and H1, A true, H2` C true then H1, H2` C true.The latter is called a substitution principle because in order to obtainevidence for C true we substitute derivations of A true for uses of the as-sumption A true.LECTURE NOTES NOVEMBER 18, 2004The Curry-Howard Isomorphism L23.3Now we have the concepts in place to be able to define implication byits introduction rule.H, A true ` B trueH ` A ⊃ B true⊃IThe elimination rule is based on the substitution principle. Assume weknow that A ⊃ B true. By the above rule this means B true under the as-sumption that A true. Now, if we had a proof of A true we could substituteit for uses of the assumption in the proof of B true. As a rule:H ` A ⊃ B true H ` A trueH ` B true⊃ENow we can prove, for example, that (A ∧ B) ⊃ (B ∧ A) true.A ∧ B true ` A ∧ B trueHyp1A ∧ B true ` B true∧E2A ∧ B true ` A ∧ B trueHyp1A ∧ B true ` A true∧E1A ∧ B true ` B ∧ A true∧I· ` (A ∧ B) ⊃ (B ∧ A) true⊃INote that this is holds for any propositions A and B, that is, it is a schematicderivation just like inference rules are schematic.We continue our analysis of logical connectives with disjunction A ∨ B.The disjunction is true if either of the disjuncts is true. This means we havetwo introduction rules.H ` A trueH ` A ∨ B true∨I1H ` B trueH ` A ∨ B true∨I2In order to determine the elimination rule, we must consider how to usethe knowledge that A ∨ B true. Clearly, we do not know which of A trueor B true holds. This means if we are trying to prove C true and we knowA ∨ B true, we must be able to show C true no matter whether A true orB true. In other words, we must proceed with a proof by cases. In the formof an elimination rule:H ` A ∨ B true H, A true ` C true H, B true ` C trueH ` C true∨EAs a sample proof, consider the statementIf A or B implies C, then A implies C.LECTURE NOTES NOVEMBER 18, 2004L23.4 The Curry-Howard IsomorphismFormally:((A ∨ B) ⊃ C) ⊃ (A ⊃ C) trueThe proof:(A ∨ B) ⊃ C true, A true ` A trueHyp2(A ∨ B) ⊃ C true, A true ` A ∨ B true∨I1(A ∨ B) ⊃ C true, A true ` (A ∨ B) ⊃ C trueHyp1(A ∨ B) ⊃ C true, A true ` C true⊃E(A ∨ B) ⊃ C true ` A ⊃ C true⊃I· ` ((A ∨ B) ⊃ C) ⊃ (A ⊃ C) true⊃INext we look at some degenerate cases. Consider truth (>) as a logicalconstant. It should be provable no matter what assumptions we have.H ` > true>IBecause we put no information into the proof of >, we can obtain no infor-mation out. Therefore, there is no elimination rule for >. We can observethat > is like a 0-ary version of conjunction: ∧I has two premises and con-sequently we have two elimination rules (∧E1and ∧E2), while >I has nopremises and consequently no elimination rules.Now consider falsehood (⊥). It represents a contradiction and shouldtherefore not be provable. In other words, there is no introduction rule.Conversely, if we know ⊥ true we should be able to conclude anything.H ` ⊥ trueH ` C true⊥EWe can recognize falsehood as a disjunction of zero alternatives. Whereasthere are two introduction rules for ∨ and therefore two cases to considerin the elimination rule, there are no introduction rules