---
tag: TH8EGSCFYY
kind: definition
name: Proof theory
msc: ["03F03", "03F05"]
defines: N4EDJNMTEF
uses: [0B94TKFQJX, 086QKPF0A6]
sources:
  - url: https://en.wikipedia.org/wiki/Proof_theory
---

## Definition

A *formal system* consists of a formal language, a set of axioms, and a finite set of inference rules.
A *formal proof* in such a system is a finite sequence or tree of formulas.
In it, each formula is an axiom or follows from earlier formulas by an inference rule.
*Proof theory* is the branch of mathematical logic whose objects of study are formal proofs.
The proofs are taken in systems of [[predicate logic|086QKPF0A6]] and in theories such as arithmetic.
It studies their structure, their transformations and their length, and what follows for the theories in which they are written.

## Remarks

Example: the question whether every proof in the sequent calculus can be turned into a proof without the cut rule is a question of proof theory.
Its answer is the cut-elimination theorem of Gentzen.
Non-example: the question whether a given group is abelian is not a question of proof theory, because its object is a group and not a formal proof.
Main parts of the field are structural proof theory, ordinal analysis, provability logic, reverse mathematics and proof complexity.
The informal notion that formal proofs model is [[mathematical proof|0B94TKFQJX]].