It is recommended to start with the C1ick ⅋ c⊗LLec⊥ tutorial first.
Not all sequents below are provable!
Multiplicative Connectives
- ⊢ A⊥⅋A
- ⊢ A, B⊥⊗A⊥, B
- A⊗B ⊢ B⊗A
- ⊢ A⊗A⊥, B, B⊥
- ⊢ (A⊗A)⅋(A⊥⅋A⊥)
- ⊢ (A⊥⊗A)⅋(A⊥⅋A)
- A ⊢ A⊗A
- A⊗A ⊢ A
- (A⅋A⊥)⊗(A⅋A⊥) ⊢ A⅋A⊥
- ⊢ A⊥⅋B, B⊥⊗C, C⊥⊗D, A⊗D⊥
- ⊢ 1, ⊥
- A⊗1 ⊢ A
- A ⊢ ⊥⊗A
- ⊢ 1, A⊥⊗A
- ⊢ (1⅋1)⊗⊥
- ⊢ A⊥⅋B, B⊥⅋A, ⊥⊗⊥
- ⊢ A⊗(B⊥⅋C), (A⊥⅋B)⅋(⊥⊗C⊥)
- A ⊢ A&A
- A ⊢ A⊕A
- A⊕B ⊢ B⊕A
- ⊢ A⊥⊕A
Multiplicative and Additive Connectives
- A&B ⊢ A⊗B
- A&B, A&B ⊢ A⊗B
- (A⊗B)&(A⊗C) ⊢ A⊗(B&C)
- (A⊗B)⊕(A⊗C) ⊢ A⊗(B⊕C)
- (A&1)⊗(B&1) ⊢ A&B
- ⊢ (1⊕A⊥)&(A⊥⅋B), A⊗(B⊥⅋(⊥⊕B))
- ⊢ 1⊕⊤
- ⊢ (A⊥⅋B)⊗⊤, A⊗⊤
- ⊢ ((((⊤⅋1)⊗⊥)⅋0)⊗⊤)⅋1
- ⊢ ?A⅋1
- 1 ⊢ !?1
- ?A ⊢ !A
- !A ⊢ !A⊗!A
- ?!A ⊢ ?!?!A
- ⊢ 1⅋!?⊥, ?1⊗?1
- ⊢ (1⅋1)⊗⊥, ?(?1⊗?1)
- !A⊗!B ⊢ !(A⊗B)
- ?(!A⊕!B) ⊢ ?!(A⊕B)
- !?!A⊗!?!B ⊢ !?!(A⊗B)
- ⊢ (?0⅋1)⊗(⊥⅋!⊤)
- !A⊗!B ⊢ !(A&B)
- ?A⅋?B ⊢ ?(A⊕B)