Proof theory

From Wikipedia for FEVERv2
Jump to navigation Jump to search

Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proof theory_sentence_0

Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Proof theory_sentence_1

As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Proof theory_sentence_2

Some of the major areas of proof theory include structural proof theory, ordinal analysis, provability logic, reverse mathematics, proof mining, automated theorem proving, and proof complexity. Proof theory_sentence_3

Much research also focuses on applications in computer science, linguistics, and philosophy. Proof theory_sentence_4

History Proof theory_section_0

Proof theory_unordered_list_0

  • Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of ω-consistency to simple consistency;Proof theory_item_0_0
  • Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;Proof theory_item_0_1
  • Transfinite iteration of theories, due to Alan Turing and Solomon Feferman;Proof theory_item_0_2
  • The discovery of self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the diagonal argument that is the key to Gödel's unprovability argument.Proof theory_item_0_3

In parallel to the rise and fall of Hilbert's program, the foundations of structural proof theory were being founded. Proof theory_sentence_5

Jan Łukasiewicz suggested in 1926 that one could improve on Hilbert systems as a basis for the axiomatic presentation of logic if one allowed the drawing of conclusions from assumptions in the inference rules of the logic. Proof theory_sentence_6

In response to this, Stanisław Jaśkowski (1929) and Gerhard Gentzen (1934) independently provided such systems, called calculi of natural deduction, with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in introduction rules, and the consequences of accepting propositions in the elimination rules, an idea that has proved very important in proof theory. Proof theory_sentence_7

Gentzen (1934) further introduced the idea of the sequent calculus, a calculus advanced in a similar spirit that better expressed the duality of the logical connectives, and went on to make fundamental advances in the formalisation of intuitionistic logic, and provide the first combinatorial proof of the consistency of Peano arithmetic. Proof theory_sentence_8

Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of analytic proof to proof theory. Proof theory_sentence_9

Structural proof theory Proof theory_section_1

Main article: Structural proof theory Proof theory_sentence_10

Structural proof theory is the subdiscipline of proof theory that studies the specifics of proof calculi. Proof theory_sentence_11

The three most well-known styles of proof calculi are: Proof theory_sentence_12

Proof theory_unordered_list_1

Each of these can give a complete and axiomatic formalization of propositional or predicate logic of either the classical or intuitionistic flavour, almost any modal logic, and many substructural logics, such as relevance logic or linear logic. Proof theory_sentence_13

Indeed, it is unusual to find a logic that resists being represented in one of these calculi. Proof theory_sentence_14

Proof theorists are typically interested in proof calculi that support a notion of analytic proof. Proof theory_sentence_15

The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are cut-free. Proof theory_sentence_16

Much of the interest in cut-free proofs comes from the subformula property: every formula in the end sequent of a cut-free proof is a subformula of one of the premises. Proof theory_sentence_17

This allows one to show consistency of the sequent calculus easily; if the empty sequent were derivable it would have to be a subformula of some premise, which it is not. Proof theory_sentence_18

Gentzen's midsequent theorem, the Craig interpolation theorem, and Herbrand's theorem also follow as corollaries of the cut-elimination theorem. Proof theory_sentence_19

Gentzen's natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz. Proof theory_sentence_20

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. Proof theory_sentence_21

More exotic proof calculi such as Jean-Yves Girard's proof nets also support a notion of analytic proof. Proof theory_sentence_22

A particular family of analytic proofs arising in reductive logic are focused proofs which characterise a large family of goal-directed proof-search procedures. Proof theory_sentence_23

The ability to transform a proof system into a focused form is a good indication of its syntactic quality, in a manner similar to how admissibility of cut shows that a proof system is syntactically consistent. Proof theory_sentence_24

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. Proof theory_sentence_25

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. Proof theory_sentence_26

Other research topics in structural theory include analytic tableau, which apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics, and the proof theory of substructural logics. Proof theory_sentence_27

Ordinal analysis Proof theory_section_2

Main article: Ordinal analysis Proof theory_sentence_28

Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for subsystems of arithmetic, analysis, and set theory. Proof theory_sentence_29

Gödel's second incompleteness theorem is often interpreted as demonstrating that finitistic consistency proofs are impossible for theories of sufficient strength. Proof theory_sentence_30

Ordinal analysis allows one to measure precisely the infinitary content of the consistency of theories. Proof theory_sentence_31

For a consistent recursively axiomatized theory T, one can prove in finitistic arithmetic that the well-foundedness of a certain transfinite ordinal implies the consistency of T. Gödel's second incompleteness theorem implies that the well-foundedness of such an ordinal cannot be proved in the theory T. Proof theory_sentence_32

Consequences of ordinal analysis include (1) consistency of subsystems of classical second order arithmetic and set theory relative to constructive theories, (2) combinatorial independence results, and (3) classifications of provably total recursive functions and provably well-founded ordinals. Proof theory_sentence_33

Ordinal analysis was originated by Gentzen, who proved the consistency of Peano Arithmetic using transfinite induction up to ordinal ε0. Proof theory_sentence_34

Ordinal analysis has been extended to many fragments of first and second order arithmetic and set theory. Proof theory_sentence_35

One major challenge has been the ordinal analysis of impredicative theories. Proof theory_sentence_36

The first breakthrough in this direction was Takeuti's proof of the consistency of Π 1-CA0 using the method of ordinal diagrams. Proof theory_sentence_37

Provability logic Proof theory_section_3

Main article: Provability logic Proof theory_sentence_38

Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. Proof theory_sentence_39

The point is to capture the notion of a proof predicate of a reasonably rich formal theory. Proof theory_sentence_40

As basic axioms of the provability logic GL (Gödel-Löb), which captures provable in Peano Arithmetic, one takes modal analogues of the Hilbert-Bernays derivability conditions and Löb's theorem (if it is provable that the provability of A implies A, then A is provable). Proof theory_sentence_41

Some of the basic results concerning the incompleteness of Peano Arithmetic and related theories have analogues in provability logic. Proof theory_sentence_42

For example, it is a theorem in GL that if a contradiction is not provable then it is not provable that a contradiction is not provable (Gödel's second incompleteness theorem). Proof theory_sentence_43

There are also modal analogues of the fixed-point theorem. Proof theory_sentence_44

Robert Solovay proved that the modal logic GL is complete with respect to Peano Arithmetic. Proof theory_sentence_45

That is, the propositional theory of provability in Peano Arithmetic is completely represented by the modal logic GL. Proof theory_sentence_46

This straightforwardly implies that propositional reasoning about provability in Peano Arithmetic is complete and decidable. Proof theory_sentence_47

Other research in provability logic has focused on first-order provability logic, polymodal provability logic (with one modality representing provability in the object theory and another representing provability in the meta-theory), and interpretability logics intended to capture the interaction between provability and interpretability. Proof theory_sentence_48

Some very recent research has involved applications of graded provability algebras to the ordinal analysis of arithmetical theories. Proof theory_sentence_49

Reverse mathematics Proof theory_section_4

Main article: Reverse mathematics Proof theory_sentence_50

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Proof theory_sentence_51

The field was founded by Harvey Friedman. Proof theory_sentence_52

Its defining method can be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. Proof theory_sentence_53

The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. Proof theory_sentence_54

The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory. Proof theory_sentence_55

In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems. Proof theory_sentence_56

For example, to study the theorem "Every bounded sequence of real numbers has a supremum" it is necessary to use a base system that can speak of real numbers and sequences of real numbers. Proof theory_sentence_57

For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. Proof theory_sentence_58

To show that a system S is required to prove a theorem T, two proofs are required. Proof theory_sentence_59

The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. Proof theory_sentence_60

The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T. Proof theory_sentence_61

One striking phenomenon in reverse mathematics is the robustness of the Big Five axiom systems. Proof theory_sentence_62

In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and Π 1-CA0. Proof theory_sentence_63

Nearly every theorem of ordinary mathematics that has been reverse mathematically analyzed has been proven equivalent to one of these five systems. Proof theory_sentence_64

Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT 2 (Ramsey's theorem for pairs). Proof theory_sentence_65

Research in reverse mathematics often incorporates methods and techniques from recursion theory as well as proof theory. Proof theory_sentence_66

Functional interpretations Proof theory_section_5

Functional interpretations are interpretations of non-constructive theories in functional ones. Proof theory_sentence_67

Functional interpretations usually proceed in two stages. Proof theory_sentence_68

First, one "reduces" a classical theory C to an intuitionistic one I. Proof theory_sentence_69

That is, one provides a constructive mapping that translates the theorems of C to the theorems of I. Proof theory_sentence_70

Second, one reduces the intuitionistic theory I to a quantifier free theory of functionals F. These interpretations contribute to a form of Hilbert's program, since they prove the consistency of classical theories relative to constructive ones. Proof theory_sentence_71

Successful functional interpretations have yielded reductions of infinitary theories to finitary theories and impredicative theories to predicative ones. Proof theory_sentence_72

Functional interpretations also provide a way to extract constructive information from proofs in the reduced theory. Proof theory_sentence_73

As a direct consequence of the interpretation one usually obtains the result that any recursive function whose totality can be proven either in I or in C is represented by a term of F. If one can provide an additional interpretation of F in I, which is sometimes possible, this characterization is in fact usually shown to be exact. Proof theory_sentence_74

It often turns out that the terms of F coincide with a natural class of functions, such as the primitive recursive or polynomial-time computable functions. Proof theory_sentence_75

Functional interpretations have also been used to provide ordinal analyses of theories and classify their provably recursive functions. Proof theory_sentence_76

The study of functional interpretations began with Kurt Gödel's interpretation of intuitionistic arithmetic in a quantifier-free theory of functionals of finite type. Proof theory_sentence_77

This interpretation is commonly known as the Dialectica interpretation. Proof theory_sentence_78

Together with the double-negation interpretation of classical logic in intuitionistic logic, it provides a reduction of classical arithmetic to intuitionistic arithmetic. Proof theory_sentence_79

Formal and informal proof Proof theory_section_6

Main article: Formal proof Proof theory_sentence_80

The informal proofs of everyday mathematical practice are unlike the formal proofs of proof theory. Proof theory_sentence_81

They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time and patience. Proof theory_sentence_82

For most mathematicians, writing a fully formal proof is too pedantic and long-winded to be in common use. Proof theory_sentence_83

Formal proofs are constructed with the help of computers in interactive theorem proving. Proof theory_sentence_84

Significantly, these proofs can be checked automatically, also by computer. Proof theory_sentence_85

Checking formal proofs is usually simple, whereas finding proofs (automated theorem proving) is generally hard. Proof theory_sentence_86

An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors. Proof theory_sentence_87

Proof-theoretic semantics Proof theory_section_7

Main articles: proof-theoretic semantics and logical harmony Proof theory_sentence_88

In linguistics, type-logical grammar, categorial grammar and Montague grammar apply formalisms based on structural proof theory to give a formal natural language semantics. Proof theory_sentence_89

See also Proof theory_section_8

Proof theory_unordered_list_2

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: theory.