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}}