Sequent calculus cheat sheet


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

- +

Additive

1 A AB 2 B AB
, A , B
, AB
A, B,
AB,
A AB 1 B AB 2
(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
RE ER

Implicative

A B
AB
A, , B , AB
A, , B BA,
A B
BA
(AB)BA
ABAB
(BA)AB
BAAB

Negation

A A A, , A
, A A, A A
AA
AAR
AA
AAE

Assertion

A A , A , A
A, A, A A
AA
AEA
AA
ARA

Shifts

A, A A , A
A A, , A A
(AB)N = (AN)B (AB)V = (AV(BV))

Quantification

A{B/X} X.A , A
Xfv()
, X.A
Xfv()
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