Sequent calculus cheat sheet

Rules for sequent calculus connectives, formatted as a cheat sheet.

- +
Additive
₁ `A` `AB` ₂ `B` `AB` , `A` , `B` , `AB` `A`, `B`, `AB`, `A` `AB` ₁ `B` `AB` ₂
(`AB`) ≈ `AB` (`AB`) ≈ `AB`
no left rule for , , no right rule for
≈ ≈
Multiplicative
`A` `B` `AB` , `A`, `B` , `AB` `A`, `B`, `AB`, `A` `B` `AB`
(`AB`) ≈ `AB` (`AB`) ≈ `AB`
_R _R _R _R _R , _R _R _E _E _E, _E _E _E _E
_R ≈ _E _E ≈ _R
Implicative
`A` `B` `AB` `A`, , `B` , `AB` `A`, , `B` `BA`, `A` `B` `BA`
(`AB`) ≈ `BA` (`BA`) ≈ `AB` `AB` ≈ `AB` `BA` ≈ `AB`
Negation
`A` `A` `A`, , `A` , `A` `A`, `A` `A`
`A` ≈ `A` `A` ≈ `A`_R `A` ≈ `A` `A` ≈ `A`_E
Assertion
`A` `A` , `A` , `A` `A`, `A`, `A` `A`
`A` ≈ `A` `A` ≈ _E`A` `A` ≈ `A` `A` ≈ _R`A`
Shifts
`A`, `A` `A` , `A` `A` `A`, , `A` `A`
(`AB`)^N = (`A^N`)`B` (`AB`)^V = (`A^V`(`B^V`))
Quantification
`A`{`B`/`X`} `X`.`A` , `A` `X` ∉ fv() , `X`.`A` `X` ∉ fv() `A`, `X`.`A`, `A`{`B`/`X`} `X`.`A`
(`X`.`A`) ≈ `X`.`A` (`X`.`A`) ≈ `X`.`A`
Core
init `A` `A` cut , `A` `A`,
Structural
`weaken` `A`, `weaken` , `A` `contract` `A`, `A`, `A`, `contract` , `A`, `A` , `A`
Legend `A`: negative variable `A`: positive variable `A`: arbitrary polarity variable Show polarities