Propositions as types (graduate only)

Now would be a good time to bring up the Curry-Howard isomorphism (pages 108-109). Forget about type systems for a moment and think about propositional logic.

We define a syntax of formulas:

φ ::= x
      true
      false
      φ → φ
      φ ∧ φ
      φ ∨ φ

And inference rules for Γ ⊢ φ (“under the assumptions in Γ, φ is provable”):

――――――――
Γ ⊢ true

――――――――
Γ, φ ⊢ φ

 Γ, φ1 ⊢ φ2
――――――――――――                              (→ introduction)
Γ ⊢ φ1 → φ2                              
                                          
Γ ⊢ φ1 → φ2  Γ ⊢ φ1                      
――――――――――――――――――――                      (→ elimination, or modus ponens)
       Γ ⊢ φ2                             
                                          
Γ ⊢ φ1  Γ ⊢ φ2                            
――――――――――――――                            (∧ introduction)
 Γ ⊢ φ1 ∧ φ2                              
                                          
Γ ⊢ φ1 ∧ φ2                               
―――――――――――   i ∈ {1,2}                   (∧ elimination)
  Γ ⊢ φi                                  
                                          
   Γ ⊢ φi                                 
―――――――――――   i ∈ {1,2}                   (∨ introduction)
Γ ⊢ φ1 ∨ φ2

Γ ⊢ φ1 ∨ φ2   Γ ⊢ φ1 → φ   Γ ⊢ φ1 → φ
―――――――――――――――――――――――――――――――――――――――   (∨ elimination)
                Γ ⊢ φ

This is a restriction of propositional logic called intuitionistic propositional logic that doesn’t have negation.

The Curry-Howard isomorphism is a correspondence between proof systems in logic and type systems in programming language theory. Notice the similarity between these rules and the typing rules we’ve built up so far.

This naturally leads to a number of questions, like:

• What does false correspond to? The empty type, usually written ⊥.
• What do ∀ and ∃ correspond to?
• What does negation correspond to?