|
Proof theory, a form of metamathematics, studies the
ways in which proofs are used in mathematics. However, in contrast to common mathematics, statements and proofs in proof theory are purely
formal. This means that they are specified in a formal language that usually employs some symbolic logic.
Therefore, on the one hand, proof theory admits no ambiguity. On the other hand, it is restricted to those statements that can
be expressed in the chosen language. In this strictly formal sense, proof theory is not necessarily a form of metamathematics,
but can have immediate applications in artificial
intelligence, where automated deduction plays an important role.
Proof theory studies how tautologies can be proven with the help of some
formal calculus. Based on the axioms and
rules of inference of such a system, derivations of logical
statements are constructed. These derivations constitute formal proofs of the statements.
As such, proof theory is related to syntax in logic; model theory correspondingly relates
to semantics. The
method of proof theory is to consider proofs as combinatorial objects, or examples of data structures, in their own right. As
such they may be manipulated or operated on systematically, the set of all proofs in a formal language being itself a formal
language.
In some situations, the term proof theory may be used to refer to a concrete calculus. For example, one may
state that there is no proof theory for second-order logic,
meaning that there is no syntactical calculus for this logic that simultaneously (1) is sound, and (2) is complete, and (3) is decidable (admits a proof-checking algorithm). First-order logic and many logics "below" admit a proof theory.
Historically, the field was established by David Hilbert, generally
considered one of the greatest mathematicians of the late 19th and early 20th century.
The major step forward technically speaking was the work of Gerhard
Gentzen on the method of cut-elimination. See the pages sequent and sequent calculus.
Proof theory, model theory, axiomatic set theory, and
recursion theory are the so-called "four theories" of the foundations of mathematics.
See also
|