Analytic Proof - Structural Proof Theory

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)

    O, popular applause! what heart of man
    Is proof against thy sweet, seducing charms?
    William Cowper (1731–1800)

    The whole theory of modern education is radically unsound. Fortunately in England, at any rate, education produces no effect whatsoever. If it did, it would prove a serious danger to the upper classes, and probably lead to acts of violence in Grosvenor Square.
    Oscar Wilde (1854–1900)