#
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 i*dentity* 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