MRI masterclass Type Theory and Proof Assistants

Exercises 1 (by Andrew Polonsky)

• Prove the following formulae using the Curry-Howard isomorphism. (Recall that ~A abbreviates (A -> 0), where 0 is uninhabited, but 0->S is inhabited for every type S):
  • ((A -> B) -> A) -> (A -> B) -> B
  • (A -> B -> C) -> ((B -> A) -> B) -> A -> C
  • ~~~A -> ~A
  • (A -> B) -> (~B -> ~A)
• Find a tautology which has countably many distinct normalized proofs. Describe them.
• Give a formula which can only be proved from assumptions (contexts) containing a non-atomic premise.
• Which operations in natural deduction are the analogues of the weakening and contraction rules of sequent calculus? What properties of the term's structure do these correspond to under C-H?