Analytic proof
1007110
146125202
2007-07-21T14:04:40Z
CBM
1108292
/* See also */ switch stub type
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-elimination|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.
<!-- To add:
Why is analytic proof interesting?
Analytic proof in other systems
The connection to proof-theoretic semantics -->
==See also==
* [[Proof-theoretic semantics]]
[[Category:Proof theory]]
{{logic-stub}}