# Logical Foundations of Programming Languages (2020-2021)

# Proofs part

## Course 1

## 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 3

## 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)
- A ⊢ A ⊗ A
- A ⊢ A & A
- A ⊢ A ⅋ A
- A ⊢ A ⊕ A
- A ⊗ B ⊢ B ⊗ A
- A ⊕ B ⊢ B ⊕ A
- (A ⅋ B) ⅋ C ⊢ A ⅋ (B ⅋ C)
- A ⊗ (B ⅋ C) ⊢ (A ⊗ B) ⅋ C
- (A ⊗ B) ⅋ C ⊢ A ⊗ (B ⅋ C)
- (A ⅋ A
^{⊥}) ⊗ (A ⅋ A^{⊥}) ⊢ A ⅋ A^{⊥}
- (A ⊗ B) & (A ⊗ C) ⊢ A ⊗ (B & C)
- A ⊗ (B & C) ⊢ (A ⊗ B) & (A ⊗ C)
- (A ⅋ B) & (A ⅋ C) ⊢ A ⅋ (B & C)
- A ⅋ (B & C) ⊢ (A ⅋ B) & (A ⅋ C)
- (A ⅋ B) ⊕ (A ⅋ C) ⊢ A ⅋ (B ⊕ C)
- A ⅋ (B ⊕ C) ⊢ (A ⅋ B) ⊕ (A ⅋ C)
- A ⊗ 1 ⊢ A
- A ⅋ 1 ⊢ A
- A ⊗ 0 ⊢ 0
- A & 0 ⊢ 0

## Course 5

## Course 6

- blackboard copy
- course notes pages 91-92, 95-99
- course notes on proof nets pages 1-7
**Homework:**
- Give the rules of LJ (sequent calculus for intuitionistic logic) with connectives: implication, conjunction, disjunction only.
- Define ILL (sequent calculus for intuitionistic linear logic) with connectives: linear implication, tensor, with, plus, of course.
- Define Girard's translation (_)
^{•} from LJ (as above) to ILL (as above)
- formulas
- sequents
- rules

- Prove that "!Γ
^{•} ⊢ A^{•}" in ILL implies "Γ ⊢ A" in LJ.
- Prove that "Γ ⊢ A" in ILL implies "⊢ Γ
^{⊥}, A" in LL.
- Conclude that "Γ ⊢ A" in LJ if and only if "⊢ ?(Γ
^{•})^{⊥}, A^{•}" in LL.

## Course 7

## Course 8