Sequent Calculus

Contents

Category

Tautology

‘Identity’.

\frac{}{A ⊢ A}

Syllogism

‘Composition’.

\frac{A ⊢ B B ⊢ C}{A ⊢ C}

Monoidal Category

?

‘Monoid product’.

\frac{A ⊢ B C ⊢ D}{A, C ⊢ B, D}

?

‘Composition’.

Symmetric Monoidal Category

Exchange

‘Symmetry’.

\frac{}{A, B ⊢ B, A}

Cartesian Monoidal Category

?

‘Diagonal’.

\frac{}{A ⊢ A, A}

?

‘’.

\frac{}{A ⊢ I}

Cartesian Closed Category

?

\frac{A, B ⊢ C}{A ⊢ B \to C}

?

‘Evaluation’.

\frac{}{A, A \to B ⊢ B}

References