Sequent calculus

Warning: This page is under construction.

Proofs

Formulas - Sequents and rules - Basic equivalences and second order definability

See also: Denotational semantics

Alternative formulations: Two-sided sequent calculus - Hybrid sequent calculus

Variations: Intuitionistic Linear Logic - More structural rules

See also:  Classical Logic and Unified Logic

Reductions

Theorem: Cut can be eliminated and identity can be restricted to the atomic case.

Cut elimination (key cases) - Cut elimination (commutative cases) - Expansion of identities

See also: Phase semantics - Proof nets - Denotational semantics

Corollaries: subformula property, strong and weak consistency, splitting property, disjunction property, and existence property.

About provable formulas

Translations

Polarities - Intuitionistic Logic - Classical Logic

See also: Proof nets - Denotational semantics - Classical Logic and Unified Logic

Miscellaneous

Invariants

See also: Phase semantics - Proof nets

About exponential rules

See also: Proof nets - Denotational semantics - Geometry of interaction