MRI masterclass Type Theory and Proof Assistants
Exercises 1 (by Andrew Polonsky)

Prove the following formulae using the CurryHoward 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 nonatomic 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 CH?
herman
Last modified: Tue Feb 27 19:42:44 CET 2007