Proof theory

Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. 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. As such, proof theory is closer to syntax, while model theory is more purely semantical. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics.

Related Topics:
Mathematical logic - Proofs - Data structures - Axiom - Rules of inference - Syntax - Model theory - Semantical - Axiomatic set theory - Recursion theory - Foundations of mathematics

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

That represents the position as of about 1940 onwards. The subject of proof theory has a significant if somewhat opaque prehistory as metamathematics, the proposed theory under development since the start of the twentieth century, which was, for a generation, under the influence of David Hilbert. The aim of a convincing consistency proof for mathematics was not to be realised, for reasons only later understood: proof theory can only sweep the metaphysical dust into tidier heaps under carpets with more attractive patterns. Hilbert's ideas seem to have been based on an analogy, in fact false, with the elimination theory of algebraic geometry familiar to him from his early work in algebra. The real insights of proof theory, such as cut-elimination and the isolation of the structural rules, were not to come from this direction.

Related Topics:
1940 - Metamathematics - Twentieth century - David Hilbert - Consistency proof - Elimination theory - Algebraic geometry

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Proof theory can also be considered a branch of philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible.

Related Topics:
Philosophical logic - Proof-theoretic semantics

~ ~ ~ ~ ~ ~ ~ ~ ~ ~