tag

#sequent calculus

2 pages tagged

Maths › 03. Logic and Foundations ›

3.5 Cut Elimination

The cut rule allows a proof to introduce an intermediate formula and then eliminate it, and while this rule can shorten derivations by reusing previously proved statements, it is not essential for the power of the sequent calculus, and its elimination reveals a deeper structural property of proofs. The Cut Rule The cut rule has the form: $$ \frac{\Gamma \vdash \Delta, A \qquad \Gamma, A \vdash \Delta}{\Gamma \vdash \Delta} $$...

Maths › 03. Logic and Foundations ›

3.2 Sequent Calculus

The sequent calculus is a proof system in which reasoning is expressed in terms of sequents, and it makes the structure of logical arguments explicit by separating assumptions from conclusions and by allowing multiple formulas to appear on both sides of a derivation. A sequent has the form: $$ \Gamma \vdash \Delta $$ where $\Gamma$ and $\Delta$ are finite collections of formulas, and it is understood that $\Gamma$ represents assumptions...