Structural Proof Theory
In proof theory, the notion of analytic proof provides the fundamental concept that brings out the similarities between a number of essentially distinct proof calculi, so defining the subfield of structural proof theory. There is no uncontroversial general definition of analytic proof, but for several proof calculi there is an accepted notion. For example:
- In Gerhard 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 the inference rules of both calculi so that there are proofs that satisfy the condition but are not analytic. For example, a particularly tricky example of this is the analytic cut rule, used widely in the tableau method, which 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.
Furthermore, structural proof theories that are not analogous to Gentzen's theories have other notions of analytic proof. For example, the calculus of structures organises its inference rules into pairs, called the up fragment and the down fragment, and an analytic proof is one that only contains the down fragment.
Read more about this topic: Analytic Proof
Famous quotes containing the words structural, proof and/or theory:
“The reader uses his eyes as well as or instead of his ears and is in every way encouraged to take a more abstract view of the language he sees. The written or printed sentence lends itself to structural analysis as the spoken does not because the reader’s eye can play back and forth over the words, giving him time to divide the sentence into visually appreciated parts and to reflect on the grammatical function.”
—J. David Bolter (b. 1951)
“He who has never failed somewhere, that man can not be great. Failure is the true test of greatness. And if it be said, that continual success is a proof that a man wisely knows his powers,—it is only to be added, that, in that case, he knows them to be small.”
—Herman Melville (1819–1891)
“Thus the theory of description matters most.
It is the theory of the word for those
For whom the word is the making of the world,
The buzzing world and lisping firmament.”
—Wallace Stevens (1879–1955)