Linear Logic Tutorial

It is recommended to start with the C1ick ⅋ c⊗LLec⊥ tutorial first.

Not all sequents below are provable!

Multiplicative Connectives

1. ⊢ A^⊥⅋A
2. ⊢ A, B^⊥⊗A^⊥, B
3. A⊗B ⊢ B⊗A
4. ⊢ A⊗A^⊥, B, B^⊥
5. ⊢ (A⊗A)⅋(A^⊥⅋A^⊥)
6. ⊢ (A^⊥⊗A)⅋(A^⊥⅋A)
7. A ⊢ A⊗A
8. A⊗A ⊢ A
9. (A⅋A^⊥)⊗(A⅋A^⊥) ⊢ A⅋A^⊥
10. ⊢ A^⊥⅋B, B^⊥⊗C, C^⊥⊗D, A⊗D^⊥

Multiplicative Units

11. ⊢ 1, ⊥
12. A⊗1 ⊢ A
13. A ⊢ ⊥⊗A
14. ⊢ 1, A^⊥⊗A
15. ⊢ (1⅋1)⊗⊥
16. ⊢ A^⊥⅋B, B^⊥⅋A, ⊥⊗⊥
17. ⊢ A⊗(B^⊥⅋C), (A^⊥⅋B)⅋(⊥⊗C^⊥)

Additive Connectives

18. A ⊢ A&A
19. A ⊢ A⊕A
20. A⊕B ⊢ B⊕A
21. ⊢ A^⊥⊕A

Multiplicative and Additive Connectives

22. A&B ⊢ A⊗B
23. A&B, A&B ⊢ A⊗B
24. (A⊗B)&(A⊗C) ⊢ A⊗(B&C)
25. (A⊗B)⊕(A⊗C) ⊢ A⊗(B⊕C)
26. (A&1)⊗(B&1) ⊢ A&B
27. ⊢ (1⊕A^⊥)&(A^⊥⅋B), A⊗(B^⊥⅋(⊥⊕B))

Additive Units

28. ⊢ 1⊕⊤
29. ⊢ (A^⊥⅋B)⊗⊤, A⊗⊤
30. ⊢ ((((⊤⅋1)⊗⊥)⅋0)⊗⊤)⅋1

Exponential Connectives

31. ⊢ ?A⅋1
32. 1 ⊢ !?1
33. ?A ⊢ !A
34. !A ⊢ !A⊗!A
35. ?!A ⊢ ?!?!A
36. ⊢ 1⅋!?⊥, ?1⊗?1
37. ⊢ (1⅋1)⊗⊥, ?(?1⊗?1)
38. !A⊗!B ⊢ !(A⊗B)
39. ?(!A⊕!B) ⊢ ?!(A⊕B)
40. !?!A⊗!?!B ⊢ !?!(A⊗B)
41. ⊢ (?0⅋1)⊗(⊥⅋!⊤)
42. !A⊗!B ⊢ !(A&B)
43. ?A⅋?B ⊢ ?(A⊕B)