Structural Proof Theory
Structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are cut-free. His natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz. The definition is slightly more complex: we say the analytic proofs are the normal forms, which are related to the notion of normal form in term rewriting. More exotic proof calculi such as Jean-Yves Girard's proof nets also support a notion of analytic proof.
Structural proof theory is connected to type theory by means of the Curry-Howard correspondence, which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the typed lambda calculus. This provides the foundation for the intuitionistic type theory developed by Per Martin-Löf, and is often extended to a three way correspondence, the third leg of which are the cartesian closed categories.
Read more about this topic: Proof Theory
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)
“It comes to pass oft that a terrible oath, with a swaggering accent sharply twanged off, gives manhood more approbation than ever proof itself would have earned him.”
—William Shakespeare (1564–1616)
“It is not enough for theory to describe and analyse, it must itself be an event in the universe it describes. In order to do this theory must partake of and become the acceleration of this logic. It must tear itself from all referents and take pride only in the future. Theory must operate on time at the cost of a deliberate distortion of present reality.”
—Jean Baudrillard (b. 1929)