Beta Phase: Square45 is currently in beta testing. Expect some features or content to be incomplete or missing.
45

Proof Theory (Definition)

The study of proofs as formal mathematical objects, analyzing their structure and properties (like consistency and completeness).
📜

The statement of the theorem

Let L\mathcal{L} be a formal language (e.g., the language of arithmetic LPA\mathcal{L}_{PA}). A formal proof system S\mathbf{S} is defined by a set of axioms Σ\Sigma and a set of inference rules R\mathcal{R} (e.g., Modus Ponens, Cut\text{Cut} rule in sequent calculus). We denote the derivability relation by ⊢S\vdash_{\mathbf{S}}.\n\nThe core object of study is the provability predicate, ProvS(A)\text{Prov}_{\mathbf{S}}(A), which is a formula in L\mathcal{L} asserting that AA is derivable in S\mathbf{S}. If S\mathbf{S} is sufficiently strong (e.g., S=PA\mathbf{S} = \mathbf{PA}), ProvS(A)\text{Prov}_{\mathbf{S}}(A) is typically formalized as a Σ1\Sigma_{1} formula (a bounded existential quantification over sequences of formulas).\n\n**Definition (Proof Theory):** Proof Theory is the mathematical study of the meta-theory of formal systems S\mathbf{S}, specifically investigating the properties of the derivability relation ⊢S\vdash_{\mathbf{S}} and the provability predicate ProvS\text{Prov}_{\mathbf{S}}. Key areas of investigation include:\n\n1. **Consistency:** The statement Con(S):=¬ProvS(⊥)\text{Con}(\mathbf{S}) := \neg \text{Prov}_{\mathbf{S}}(\perp), asserting that the system S\mathbf{S} cannot prove a contradiction (⊥\perp).\n2. **Completeness:** The statement Comp(S)\text{Comp}(\mathbf{S}), which asserts that every logically valid formula ϕ\phi (i.e., ⊨ϕ\vDash \phi) is provable in S\mathbf{S} (i.e., ⊢Sϕ\vdash_{\mathbf{S}} \phi).\n3. **Ordinal Analysis:** The determination of the proof-theoretic ordinal PTO(S)\text{PTO}(\mathbf{S}), which is the smallest ordinal α\alpha such that the system S\mathbf{S} cannot prove the well-foundedness of the ordering relation <α<_{\alpha} on α\alpha. This is often achieved by embedding S\mathbf{S} into a system of transfinite induction up to α\alpha.\n\nFormally, Proof Theory investigates the truth value and provability of statements like Con(S)\text{Con}(\mathbf{S}) and the relationship between PTO(S)\text{PTO}(\mathbf{S}) and the strength of S\mathbf{S}. For instance, for S=PA\mathbf{S} = \mathbf{PA}, the consistency statement Con(PA)\text{Con}(\mathbf{PA}) is a Π1\Pi_{1} statement that cannot be proven within PA\mathbf{PA} itself, as per Gödel's Second Incompleteness Theorem.