Proof theory

The proof theory is a branch of mathematical logic that treats proofs as formal mathematical objects, which makes their analysis by mathematical techniques. Evidence is typically represented as an inductively -defined data structures such as lists or trees. These are designed in accordance with the axioms and rules of inference of the considered logical system. The proof theory is syntactic nature in contrast to the model theory, which is of a semantic nature.

Sometimes the proof theory is seen as part of philosophical logic, it is above all the idea of ​​the proof-theoretic semantics of interest.

History

Although the formalization of logic was already well developed by the works of Gottlob Frege, Giuseppe Peano, Bertrand Russell, Richard Dedekind and others, the beginning of modern proof theory David Hilbert is attributed, who initiated the Hilbert program called and in the 1920s in the wake of the basic dispute systematic goal for. Kurt Gödel's work has led to major advances first, but eventually refuted this program: the completeness theorem promised good prospects for Hilbert's goal is to reduce all mathematics to a finitistisches formal system; the incompleteness theorem showed, however later that this is unattainable. These results were carried out in a proof calculus, which is called Hilbert calculus.

Coinciding with the proof-theoretic work of Gödel, Gerhard Gentzen laid the foundations for what is known as structural proof theory today. In a few years Gentzen introduced the basic formalisms of natural deduction ( at the same time as, and independently of Jaskowski ) and of a sequent calculus, made substantial progress in the formalization of intuitionistic logic. In addition, he also introduced the important idea of the analytical evidence and gave the first combinatorial proof of the consistency of Peano arithmetic.

Formal and informal proofs

The informal proofs that are commonly used in mathematics, are not to be confused with the formal proofs of evidence theory. The informal proofs same sketches, from which experts could reconstruct formal proofs in principle. The letter of formal proofs, however, would have the same drawbacks as programming in machine language for mathematicians.

In the field of machine-assisted formal proofs proving with the aid of computers are produced. Such evidence can be checked automatically by means of computers. The checking of proofs is usually trivial, in contrast to the finding of evidence, which is typically very difficult. Informal proofs in the mathematical literature, however, be verified by peer review. This can take several weeks and such evidence may still contain errors.

Types of proof calculi

The three known types of proof calculi are:

• The Hilbert calculus
• The natural deduction systems
• The sequent calculus

Each of these calculi can be used for an axiomatic formalization of propositional logic or predicate logic of classical or intuitionistic type. Most calculi are also perfect for most modal logics and for many substrukturelle logics, such as the linear logic or relevance logic. It is rather unusual to find logics that can not be represented with one of these calculi.

Consistency proofs

As mentioned earlier, the Hilbert program was the motivation for the mathematical investigation of proofs in formal theories. The central idea of this program was to demonstrate the consistency of formal theories that are used by mathematicians with a finitistic proof and thus to substantiate with a metamathematical argument these theories. More specifically, it is important to show that purely universal statements (technical: it is the provable sentences meant Π01 ) are finitistic true.

The failure of the program was brought about by Gödel's incompleteness theorem. This theorem showed that every ω - consistent theory that is sufficiently strong to express certain simple arithmetic statements, their own consistency can not prove it. The claim that a theory is consistent, is a set in Gödel's formulation.

In this area, much research has been done and, among others, the following results were found:

• Refinement of Gödel's result, especially John Barkley Rosser showed that instead of ω - consistency, the weaker consistency condition is sufficient to show the incompleteness
• The axiomatization of the core statements of Gödel's result with expressions of modal logic, Beweisbarkeitslogik
• Transfinite iterations of theories by Alan Turing and Solomon Feferman
• The discovery of self-checking theories, ie systems that are strong enough to talk about himself, but too weak to perform the diagonalisation argument, which is used in Gödel's incompleteness theorem

Structural proof theory

Structural proof theory is a branch of proof theory that studies proof calculi in which the notion of analytic proof is useful. The notion of analytic proof was introduced by Gentzen for the sequent calculus. In this case, analytical proofs are those proofs that are cut free. In natural deduction systems, you can also an interpretation of the notion of analytic proof, as was shown by Dag Prawitz. In this case, the definition is complicated. More unusual proof calculi such as Jean -Yves Girard's proof nets also allow a definition of the notion of analytic proof.

Structural proof theory is connected through the Curry - Howard isomorphism with the type theory. The Curry - Howard isomorphism shows an analogy between normalization in natural deduction systems and the beta - reduction in typed lambda calculus. This is the basis for intuitionistic type theory, which was developed by Per Martin- Löf, created. This relationship can be also extended to cartesian closed categories.

In linguistics, type- logical grammar, categorical grammar and Montague grammar formalisms, which originate from the structural proof theory, used to find a formal semantics of natural language.

More

• Tableau calculi or tree using the central idea of the analytical proof of the structural proof theory to provide decision-making and semi - decision procedure for many logics are available.

• The Ordinalzahlanalyse is a powerful technique to provide combinatorial proofs of consistency theories that formalize the arithmetic or Analysis.

• Substrukturelle logics have fewer structural rules.