In structural proof theory, an analytical proof is a proof whose structure is simple in a special way. The term does not admit an uncontroversial definition, but for several proof calculi there is an accepted notion of analytic proof. For example:
- In Gentzen's natural deduction calculus the analytic proofs are those in normal form; that is, no formula occurrence is both the principal premise of an elimination rule and the conclusion of an introduction rule;
- In Gentzen's sequent calculus the analytic proofs are those that do not use the cut rule.
However it is possible to extend both calculi so that there are proofs that satisfy the condition but are not analytic: a particularly tricky example of this is the analytic cut rule: this is a special case of the cut rule where the cut formula is a subformula of side formulae of the cut rule; a proof that contains an analytic cut is by virtue of that rule not analytic.
See also