View source for Sequent calculus

=== Expansion of identities ===

Let us write <math>\pi:\Gamma\vdash\Delta</math> to signify that
<math>\pi</math> is a proof with conclusion <math>\Gamma\vdash\Delta</math>.

{{Proposition|title=<math>\eta</math>-expansion|
For every proof <math>\pi</math>, there is a proof <math>\pi'</math> with the
same conclusion as <math>\pi</math> in which the axiom rule is only used with
atomic formulas.
If <math>\pi</math> is cut-free, then there is a cut-free <math>\pi'</math>.}}
{{Proof|It suffices to prove that for every formula <math>A</math>, the sequent
<math>A\vdash A</math> has a cut-free proof in which the axiom rule is used
only for atomic formulas.
We prove this by induction on <math>A</math>.
* If <math>A</math> is atomic, then <math>A\vdash A</math> is an instance of the atomic axiom rule.
* If <math>A=A_1\tens A_2</math> then we have<br><math>
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \tens_R }
\BinRule{ A_1, A_2 \vdash A_1 \tens A_2 }
\LabelRule{ \tens_L }
\UnaRule{ A_1 \tens A_2 \vdash A_1 \tens A_2 }
\DisplayProof
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
* If <math>A=A_1\parr A_2</math> then we have<br><math>
\AxRule{ \pi_1 : A_1 \vdash A_1 }
\AxRule{ \pi_2 : A_2 \vdash A_2 }
\LabelRule{ \parr_L }
\BinRule{ A_1 \parr A_2 \vdash A_1, A_2 }
\LabelRule{ \parr_R }
\UnaRule{ A_1 \parr A_2 \vdash A_1 \parr A_2 }
\DisplayProof
</math><br>where <math>\pi_1</math> and <math>\pi_2</math> exist by induction hypothesis.
* All other connectives follow the same pattern.}}

The interesting thing with <math>\eta</math>-expansion is that, we can always assume that
each connective is explicitly introduced by its associated rule (except in the
case where there is an occurrence of the <math>\top</math> rule).