Proof theory

The proof theory is a branch of mathematical logic , the evidence treated as formal mathematical objects, allowing their analysis by mathematical techniques. Evidence is usually represented as inductively defined data structures , such as lists or trees . These are constructed according to the axioms and inference rules of the logical system under consideration. Proof theory is syntactic in nature as opposed to model theory , which is semantic in nature.

Sometimes the theory of proof is also understood as part of philosophical logic , the idea of ​​the theory of proof semantics is of particular interest.

history

Although the formalization of logic by the works of Gottlob Frege , Giuseppe Peano , Bertrand Russell , Richard Dedekind and others was well developed, the beginning of modern proof theory is attributed to David Hilbert , who initiated the so-called Hilbert program and followed it up in the 1920s of the fundamental dispute systematically expanded. Kurt Gödel's work led to great advances at first, but finally refuted this program: the completeness theorem promised good prospects for Hilbert's goal of reducing all mathematics to a finitistic formal system; however, the incompleteness theorem later showed that this is unattainable. These results were carried out in a proof calculus called the Hilbert calculus .

At the same time as Gödel's proof-theoretical work, Gerhard Gentzen laid the cornerstone for what is now known as structural proof theory . In a few years Gentzen introduced the basic formalisms of natural deduction (simultaneously with and independent of Jaskowski) and the sequent calculus and made substantial progress in the formalization of intuitionistic logic . Furthermore, he introduced the important idea of analytical proof and gave the first combinatorial proof of the consistency of Peano arithmetic .

Formal and informal evidence

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

In the field of machine- aided proof , formal proofs are generated with the help of computers. Such evidence can also be checked automatically using computers. Checking evidence is usually trivial, as opposed to finding evidence, which is typically very difficult. Informal evidence in the mathematical literature, on the other hand, is verified through peer review. This can take several weeks and such evidence can still contain errors.

Types of Evidence Calculations

The three best known types of proof calculations are:

Each of these calculi can be used for an axiomatic formalization of propositional logic or predicate logic of the classical or intuitionistic kind. Most calculi are also suitable for most modal logics and for many sub-structural logics , e.g. B. the linear logic or the relevance logic . It is rather unusual to find logic that cannot be represented with one of these calculations.

Proofs of consistency

As mentioned earlier, the Hilbert program spurred the mathematical study of evidence in formal theories. The central idea of ​​this program was to show the consistency of the formal theories used by mathematicians with a finitistic proof and thus to substantiate these theories with a metamathematic argument. To put it more precisely, it is necessary to show that purely universal statements (technical: the provable Π 0 1 sentences are meant) are finitistically true.

The failure of the program was caused by Gödel's incompleteness theorem . This theorem showed that any ω-consistent theory strong enough to express certain simple arithmetic statements cannot prove its own consistency. The statement that a theory is consistent is a sentence in Gödel's formulation . ${\ displaystyle \ Pi _ {1} ^ {0}}$

Much research has been carried out in this area and the following results have been found:

• Refinement of Gödel's result, in particular John Barkley Rosser was able to show that instead of ω-consistency the weaker requirement consistency is sufficient to show the incompleteness theorem
• The axiomatization of the core statements of Gödel's result with expressions of the modal logic, the logic of provability
• Transfinite iterations of theories by Alan Turing and Solomon Feferman
• The discovery of self-checking theories , that is, systems that are strong enough to talk about themselves but too weak to carry out the diagonalization argument used in Godel's incompleteness theorem

Structural proof theory

Structural proof theory is a branch of proof theory that studies proof calculi in which the concept of analytical proof makes sense. The concept of analytical proof was introduced by Gentzen for the sequential calculus. In this case, analytical proofs are those proofs that are cut-free . In systems of natural reasoning one can also find an interpretation for the concept of analytical proof, as shown by Dag Prawitz . In this case, the definition is complicated. More unusual proof calculations, such as Jean-Yves Girard's proof nets , also allow a definition of the concept of analytical proof.

Structural proof theory is also linked to type theory through the Curry-Howard isomorphism . The Curry-Howard isomorphism shows an analogy between normalization in systems of natural reasoning and beta reduction in the typified lambda calculus . This creates the basis for the intuitionist type theory developed by Per Martin-Löf . This relationship can also be extended to Cartesian closed categories .

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

Further

• Tableau or tree calculi use the central idea of ​​analytical proof from structural proof theory to provide decision procedures and semi-decision procedures for many logics.
• The Ordinalzahlanalyse is a powerful technique to provide combinatorial consistency evidence of theories that formalize the arithmetic or analysis.

literature

• J. Avigad, EH Reck: “Clarifying the nature of the infinite”: the development of metamathematics and proof theory . (PDF; 318 kB). Carnegie-Mellon Technical Report CMU-PHIL-120, 2001.
• Karel Berka , Lothar Kreiser: Logic texts. Annotated selection on the history of modern logic . 4th edition. Academy, Berlin 1986
• Stephen Cole Kleene : Introduction to Metamathematics . Amsterdam / Groningen 1952
• Paul Lorenzen : Metamathematics . Mannheim 1962
• Gerhard Gentzen : The Collected Papers of Gerhard Gentzen . Ed .: ME Szabo. Amsterdam 1969
• Wolfram Pohlers: Proof theory: the first step into impredicativity . Springer, Berlin / Heidelberg 2009, ISBN 978-3-540-69318-5 .
• Kurt Schütte: Proof theory (=  The basic teachings of the mathematical sciences in individual representations . Volume 225 ). Springer, Berlin / Heidelberg 1977, ISBN 3-540-07911-4 .
• Gaisi Takeuti: Proof theory (=  Studies in logic and the foundations of mathematics . Volume 81 ). 2nd Edition. North-Holland, Amsterdam 1987, ISBN 0-444-87943-9 .
• AS Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, ISBN 0-521-77911-1