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?
Last modified: Tue Feb 27 19:42:44 CET 2007