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

## Summary

Proof theory is the branch of mathematical logic that treats [[proofs|0B94TKFQJX]] as mathematical objects.
It studies formal proofs in systems of [[predicate logic|086QKPF0A6]] and of arithmetic by combinatorial means.
It began with Hilbert's aim to prove the consistency of mathematics by finitary methods.
Its main tools include normal forms of proofs, cut elimination and ordinal analysis.

## Explanations

### L1 human

In most of mathematics, a proof is a tool to reach a theorem.
In proof theory, the proof itself is the object of study, like a number or a graph.
A formal proof is a finite tree of formulas built by fixed rules.
So one can count its steps, transform it, and ask what it can never reach.
For example, one can show that a system never proves $0 = 1$.
One way is to put every proof in a simple normal form, and to check that no proof in normal form ends with $0 = 1$.