Proof theory is a major branch
[According to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with ]model theory
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
, axiomatic set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
, and recursion theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has sinc ...
. Barwise (1978) consists of four corresponding parts, with part D being about "Proof Theory and Constructive Mathematics". of
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
that represents
proof
Proof most often refers to:
* Proof (truth), argument or sufficient evidence for the truth of a proposition
* Alcohol proof, a measure of an alcoholic drink's strength
Proof may also refer to:
Mathematics and formal logic
* Formal proof, a c ...
s as formal
mathematical object
A mathematical object is an abstract concept arising in mathematics.
In the usual language of mathematics, an ''object'' is anything that has been (or could be) formally defined, and with which one may do deductive reasoning and mathematical p ...
s, facilitating their analysis by mathematical techniques. Proofs are typically presented as
inductively-defined data structures
In computer science, a data structure is a data organization, management, and storage format that is usually chosen for efficient access to data. More precisely, a data structure is a collection of data values, the relationships among them, ...
such as
lists
A ''list'' is any set of items in a row. List or lists may also refer to:
People
* List (surname)
Organizations
* List College, an undergraduate division of the Jewish Theological Seminary of America
* SC Germania List, German rugby union ...
, boxed lists, or
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are ...
s, which are constructed according to the
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s and
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
of the logical system. Consequently, proof theory is
syntactic
In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure (constituency) ...
in nature, in contrast to
model theory
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
, which is
semantic
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
in nature.
Some of the major areas of proof theory include
structural proof theory In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formalis ...
,
ordinal analysis
In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength.
If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory ha ...
,
provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic.
Examples
...
,
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
,
proof mining In proof theory, a branch of mathematical logic, proof mining (or proof unwinding) is a research program that studies or analyzes formalized proofs, especially in analysis, to obtain explicit bounds, ranges
In the Hebrew Bible and in the Old Test ...
,
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
, and
proof complexity In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. ...
. Much research also focuses on applications in computer science, linguistics, and philosophy.
History
Although the formalisation of logic was much advanced by the work of such figures as
Gottlob Frege
Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic p ...
,
Giuseppe Peano
Giuseppe Peano (; ; 27 August 1858 – 20 April 1932) was an Italian mathematician and glottologist. The author of over 200 books and papers, he was a founder of mathematical logic and set theory, to which he contributed much notation. The sta ...
,
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, a ...
, and
Richard Dedekind
Julius Wilhelm Richard Dedekind (6 October 1831 – 12 February 1916) was a German mathematician who made important contributions to number theory, abstract algebra (particularly ring theory), and
the axiomatic foundations of arithmetic. His ...
, the story of modern proof theory is often seen as being established by
David Hilbert
David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many ...
, who initiated what is called
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...
in the
''Foundations of Mathematics''. The central idea of this program was that if we could give
finitary
In mathematics and logic, an operation is finitary if it has finite arity, i.e. if it has a finite number of input values. Similarly, an infinitary operation is one with an infinite number of input values.
In standard mathematics, an operation ...
proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely universal assertions (more technically their provable
sentences) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.
The failure of the program was induced by
Kurt Gödel
Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
's
incompleteness theorems
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
, which showed that any
ω-consistent theory
In mathematical logic, an ω-consistent (or omega-consistent, also called numerically segregative)W. V. O. Quine (1971), ''Set Theory and Its Logic''. theory is a theory (collection of sentences) that is not only (syntactically) consistent (that ...
that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a
sentence. However, modified versions of Hilbert's program emerged and research has been carried out on related topics. This has led, in particular, to:
*Refinement of Gödel's result, particularly
J. Barkley Rosser
John Barkley Rosser Sr. (December 6, 1907 – September 5, 1989) was an American logician, a student of Alonzo Church, and known for his part in the Church–Rosser theorem, in lambda calculus. He also developed what is now called the "Rosser siev ...
's refinement, weakening the above requirement of ω-consistency to simple consistency;
*Axiomatisation of the core of Gödel's result in terms of a modal language,
provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic.
Examples
...
;
*Transfinite iteration of theories, due to
Alan Turing
Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical co ...
and
Solomon Feferman
Solomon Feferman (December 13, 1928 – July 26, 2016) was an American philosopher and mathematician who worked in mathematical logic.
Life
Solomon Feferman was born in The Bronx in New York City to working-class parents who had immigrated to th ...
;
*The discovery of
self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the
diagonal argument A diagonal argument, in mathematics, is a technique employed in the proofs of the following theorems:
*Cantor's diagonal argument (the earliest)
*Cantor's theorem
* Russell's paradox
*Diagonal lemma
** Gödel's first incompleteness theorem
**Tarski ...
that is the key to Gödel's unprovability argument.
In parallel to the rise and fall of Hilbert's program, the foundations of
structural proof theory In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formalis ...
were being founded.
Jan Łukasiewicz
Jan Łukasiewicz (; 21 December 1878 – 13 February 1956) was a Polish logician and philosopher who is best known for Polish notation and Łukasiewicz logic His work centred on philosophical logic, mathematical logic and history of logic. ...
suggested in 1926 that one could improve on
Hilbert system
:''In mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C*-algebra.''
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive s ...
s 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. In response to this,
Stanisław Jaśkowski (1929) and
Gerhard Gentzen
Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
(1934) independently provided such systems, called calculi of
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...
, with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in
introduction rule In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...
s, and the consequences of accepting propositions in the
elimination rule In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axio ...
s, an idea that has proved very important in proof theory. Gentzen (1934) further introduced the idea of the
sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
, 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 In mathematics, the term ''combinatorial proof'' is often used to mean either of two types of mathematical proof:
* A proof by double counting. A combinatorial identity is proven by counting the number of elements of some carefully chosen set in t ...
of the consistency of
Peano arithmetic. Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of
analytic proof In mathematics, an analytic proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not predominantly make use of algebraic or geometrical methods. The term was first used by Bernard Bolzano, who first ...
to proof theory.
Structural proof theory
Structural proof theory is the subdiscipline of proof theory that studies the specifics of
proof calculi In mathematical logic, a proof calculus or a proof system is built to prove statements.
Overview
A proof system includes the components:
* Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...
. The three most well-known styles of proof calculi are:
*The
Hilbert calculi
*The
natural deduction calculi
*The
sequent calculi
Each of these can give a complete and axiomatic formalization of
propositional or
predicate logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
of either the
classical or
intuitionistic
In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
flavour, almost any
modal logic, and many
substructural logic
In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are r ...
s, such as
relevance logic Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but ...
or
linear logic. Indeed, it is unusual to find a logic that resists being represented in one of these calculi.
Proof theorists are typically interested in proof calculi that support a notion of
analytic proof In mathematics, an analytic proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not predominantly make use of algebraic or geometrical methods. The term was first used by Bernard Bolzano, who first ...
. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are
cut-free. Much of the interest in cut-free proofs comes from the : every formula in the end sequent of a cut-free proof is a subformula of one of the premises. 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. Gentzen's midsequent theorem, the Craig interpolation theorem, and Herbrand's theorem also follow as corollaries of the cut-elimination theorem.
Gentzen's natural deduction calculus also supports a notion of analytic proof, as shown by
Dag Prawitz
Dag Prawitz (born 1936, Stockholm) is a Swedish philosopher and logician. He is best known for his work on proof theory and the foundations of natural deduction.
Prawitz is a member of the Norwegian Academy of Science and Letters, of the Roya ...
. The definition is slightly more complex: we say the analytic proofs are the
normal forms
Database normalization or database normalisation (see spelling differences) is the process of structuring a relational database in accordance with a series of so-called normal forms in order to reduce data redundancy and improve data integri ...
, which are related to the notion of normal form in term rewriting. More exotic proof calculi such as
Jean-Yves Girard
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the ...
's
proof net In proof theory, proof nets are a geometrical method of representing proofs that
eliminates two forms of ''bureaucracy'' that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, and (B) the order of rules applied in ...
s also support a notion of analytic proof.
A particular family of analytic proofs arising in
reductive logic are
focused proofs which characterise a large family of goal-directed proof-search procedures. 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.
Structural proof theory is connected to
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
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
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...
. This provides the foundation for the
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
developed by
Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer scie ...
, and is often extended to a three way correspondence, the third leg of which are the
cartesian closed categories
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in ma ...
.
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.
Ordinal analysis
Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for subsystems of arithmetic, analysis, and set theory.
Gödel's second incompleteness theorem is often interpreted as demonstrating that finitistic consistency proofs are impossible for theories of sufficient strength. Ordinal analysis allows one to measure precisely the infinitary content of the consistency of theories. 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.
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.
Ordinal analysis was originated by Gentzen, who proved the consistency of Peano Arithmetic using
transfinite induction
Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC.
Induction by cases
Let P(\alpha) be a property defined for ...
up to ordinal ε
0. Ordinal analysis has been extended to many fragments of first and second order arithmetic and set theory. One major challenge has been the ordinal analysis of impredicative theories. The first breakthrough in this direction was Takeuti's proof of the consistency of Π-CA
0 using the method of ordinal diagrams.
Provability logic
''Provability logic'' is a
modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich
formal theory. 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
In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula ''P'', if it is provable in PA that "if ''P'' is provable in PA then ''P'' is true", then ''P'' is provable in PA. If Pr ...
(if it is provable that the provability of A implies A, then A is provable).
Some of the basic results concerning the incompleteness of Peano Arithmetic and related theories have analogues in provability logic. 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). There are also modal analogues of the fixed-point theorem.
Robert Solovay
Robert Martin Solovay (born December 15, 1938) is an American mathematician specializing in set theory.
Biography
Solovay earned his Ph.D. from the University of Chicago in 1964 under the direction of Saunders Mac Lane, with a dissertation on ' ...
proved that the modal logic GL is complete with respect to Peano Arithmetic. That is, the propositional theory of provability in Peano Arithmetic is completely represented by the modal logic GL. This straightforwardly implies that propositional reasoning about provability in Peano Arithmetic is complete and decidable.
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 logic Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability or various related metamathematical properties and relations such as weak interpretability, Π1-conservativity, cointerpretability ...
s intended to capture the interaction between provability and interpretability. Some very recent research has involved applications of graded provability algebras to the ordinal analysis of arithmetical theories.
Reverse mathematics
Reverse mathematics is a program in
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
that seeks to determine which axioms are required to prove theorems of mathematics.
[Simpson 2010] The field was founded by
Harvey Friedman
__NOTOC__
Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on reverse mathematics, a project intended to derive the axi ...
. Its defining method can be described as "going backwards from the
theorem
In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
s to the
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
and
Zorn's lemma are equivalent over
ZF set theory ZF, Z-F, or Zf may refer to:
Businesses and organizations
* ZF Friedrichshafen, a German supplier of automobile transmissions
* Zionist Federation of Great Britain and Ireland, an organization established to campaign for a permanent homeland for th ...
. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory.
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. For example, to study the theorem "Every bounded sequence of
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s has a
supremum" it is necessary to use a base system that can speak of real numbers and sequences of real numbers.
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. To show that a system ''S'' is required to prove a theorem ''T'', two proofs are required. 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. The reversal establishes that no axiom system ''S′'' that extends the base system can be weaker than ''S'' while still proving ''T''.
One striking phenomenon in reverse mathematics is the robustness of the ''Big Five'' axiom systems. In order of increasing strength, these systems are named by the initialisms RCA
0, WKL
0, ACA
0, ATR
0, and Π-CA
0. Nearly every theorem of ordinary mathematics that has been reverse mathematically analyzed has been proven equivalent to one of these five systems. Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT (Ramsey's theorem for pairs).
Research in reverse mathematics often incorporates methods and techniques from
recursion theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has sinc ...
as well as proof theory.
Functional interpretations
Functional interpretations are interpretations of non-constructive theories in functional ones. Functional interpretations usually proceed in two stages. First, one "reduces" a classical theory C to an intuitionistic one I. That is, one provides a constructive mapping that translates the theorems of C to the theorems of I. 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. Successful functional interpretations have yielded reductions of infinitary theories to finitary theories and impredicative theories to predicative ones.
Functional interpretations also provide a way to extract constructive information from proofs in the reduced theory. 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. 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. Functional interpretations have also been used to provide ordinal analyses of theories and classify their provably recursive functions.
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. This interpretation is commonly known as the
Dialectica interpretation In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to pr ...
. Together with the double-negation interpretation of classical logic in intuitionistic logic, it provides a reduction of classical arithmetic to intuitionistic arithmetic.
Formal and informal proof
The ''informal'' proofs of everyday mathematical practice are unlike the ''formal'' proofs of proof theory. 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. For most mathematicians, writing a fully formal proof is too pedantic and long-winded to be in common use.
Formal proofs are constructed with the help of computers in
interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
.
Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, whereas ''finding'' proofs (
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
) is generally hard. An informal proof in the mathematics literature, by contrast, requires weeks of
peer review
Peer review is the evaluation of work by one or more people with similar competencies as the producers of the work (peers). It functions as a form of self-regulation by qualified members of a profession within the relevant field. Peer review ...
to be checked, and may still contain errors.
Proof-theoretic semantics
In
linguistics
Linguistics is the scientific study of human language. It is called a scientific study because it entails a comprehensive, systematic, objective, and precise analysis of all aspects of language, particularly its nature and structure. Linguis ...
,
type-logical grammar,
categorial grammar
Categorial grammar is a family of formalisms in natural language syntax that share the central assumption that syntactic constituents combine as functions and arguments. Categorial grammar posits a close relationship between the syntax and seman ...
and
Montague grammar apply formalisms based on structural proof theory to give a formal
natural language semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
.
See also
*
Intermediate logic In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate l ...
*
Model theory
*
Proof (truth)
*
Proof techniques
A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proo ...
*
Sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
Notes
References
* J. Avigad and E.H. Reck (2001)
"'Clarifying the nature of the infinite': the development of metamathematics and proof theory. Carnegie-Mellon Technical Report CMU-PHIL-120.
*
J. Barwise, ed. (1978). ''Handbook of Mathematical Logic''. North-Holland.
* S. Buss, ed. (1998)
Handbook of Proof Theory'' Elsevier.
* G. Gentzen (1935/1969).
Investigations into logical deduction. In M. E. Szabo, ed. ''Collected Papers of Gerhard Gentzen''. North-Holland. Translated by Szabo from "Untersuchungen über das logische Schliessen", ''Mathematisches Zeitschrift'' v. 39, pp. 176–210, 405 431.
*
J.-Y. Girard, P. Taylor, Y. Lafont (1988)
"Proofs and types" Cambridge University Press.
*
D. Prawitz (1965). ''Natural deduction: A proof-theoretical study'', Dover Publications,
* S.G. Simpson (2010). ''Subsystems of Second-order Arithmetic'', second edition. Cambridge University Press, .
*
A. S. Troelstra and H. Schwichtenberg (1996). ''Basic Proof Theory'', Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, .
*
H. Wang (1981). ''Popular Lectures on Mathematical Logic'',
Van Nostrand Reinhold Company
John Wiley & Sons, Inc., commonly known as Wiley (), is an American multinational publishing company founded in 1807 that focuses on academic publishing and instructional materials. The company produces books, journals, and encyclopedias, in p ...
, .
External links
*
*J. von Plato (2008)
The Development of Proof Theory Stanford Encyclopedia of Philosophy.
{{Mathematical logic
P
Metalogic