# Proofs part

## Course 2

• blackboard copy
• course notes pages 16-19
• Homework: prove correctness and completeness of LK with implication only (use completeness of Hilbert's system)

## Course 4

• blackboard copy
• course notes pages 24-25, 29-36, 85-86
• Homework: prove the following properties, or justify why they are not provable (we admit that cut-elimination holds)
1. A ⊢ A ⊗ A
2. A ⊢ A & A
3. A ⊢ A ⅋ A
4. A ⊢ A ⊕ A
5. A ⊗ B ⊢ B ⊗ A
6. A ⊕ B ⊢ B ⊕ A
7. (A ⅋ B) ⅋ C ⊢ A ⅋ (B ⅋ C)
8. A ⊗ (B ⅋ C) ⊢ (A ⊗ B) ⅋ C
9. (A ⊗ B) ⅋ C ⊢ A ⊗ (B ⅋ C)
10. (A ⅋ A) ⊗ (A ⅋ A) ⊢ A ⅋ A
11. (A ⊗ B) & (A ⊗ C) ⊢ A ⊗ (B & C)
12. A ⊗ (B & C) ⊢ (A ⊗ B) & (A ⊗ C)
13. (A ⅋ B) & (A ⅋ C) ⊢ A ⅋ (B & C)
14. A ⅋ (B & C) ⊢ (A ⅋ B) & (A ⅋ C)
15. (A ⅋ B) ⊕ (A ⅋ C) ⊢ A ⅋ (B ⊕ C)
16. A ⅋ (B ⊕ C) ⊢ (A ⅋ B) ⊕ (A ⅋ C)
17. A ⊗ 1 ⊢ A
18. A ⅋ 1 ⊢ A
19. A ⊗ 0 ⊢ 0
20. A & 0 ⊢ 0

## Course 6

• blackboard copy
• course notes pages 91-92, 95-99
• course notes on proof nets pages 1-7
• Homework:
1. Give the rules of LJ (sequent calculus for intuitionistic logic) with connectives: implication, conjunction, disjunction only.
2. Define ILL (sequent calculus for intuitionistic linear logic) with connectives: linear implication, tensor, with, plus, of course.
3. Define Girard's translation (_) from LJ (as above) to ILL (as above)
1. formulas
2. sequents
3. rules
4. Prove that "!Γ ⊢ A" in ILL implies "Γ ⊢ A" in LJ.
5. Prove that "Γ ⊢ A" in ILL implies "⊢ Γ, A" in LL.
6. Conclude that "Γ ⊢ A" in LJ if and only if "⊢ ?(Γ), A" in LL.