Meta-theoretic results about the limits of formal systems: Gödel's incompleteness, undecidability, the halting problem, and the open-ended class of yet-undiscovered results of this kind. The only Layer-0 tree with high generativity.
formal-systems-limits
Gödel's first incompleteness theorem
Any consistent formal system F capable of expressing elementary arithmetic contains a true statement that F cannot prove.
Undecidability of the halting problem
There is no algorithm that decides, for every pair (program, input), whether the program halts on that input.
Gödel's second incompleteness theorem
No consistent formal system F capable of expressing elementary arithmetic can prove its own consistency.
Church-Turing thesis
Every effectively calculable function is computable by a Turing machine; equivalently, the class of intuitively 'computable' functions…
Undiscovered limitative results
Beyond currently-known limitative results (incompleteness, undecidability, Rice's theorem, Chaitin's incompleteness, etc.), further results…
Ω (Chaitin's constant)
The halting probability of a prefix-free universal Turing machine — a real number encoding, in its binary expansion, the halting behaviour…
Löwenheim–Skolem theorem
A countable FOL theory with an infinite model has a model of every infinite cardinality. Sources the 'Skolem paradox' and undermines…
Compactness theorem (FOL)
A FOL theory T has a model iff every finite subset of T has a model. A cornerstone of model theory; proves existence of non-standard…
Model theory
The study of classes of structures satisfying given first-order theories. Central results: compactness, Löwenheim–Skolem, Łoś ultraproduct…
Proof theory
The syntactic study of formal proofs: structural analysis, cut elimination, ordinal analysis, reverse mathematics. Dual to model theory.
Ordinal analysis
Assigns to each consistent theory T an ordinal |T| measuring its proof-theoretic strength — the least α such that T ⊬ TI(α). |PA|=ε₀,…
Reverse mathematics
Friedman/Simpson programme: for each mathematical theorem φ, identify the minimal set-existence axioms over RCA₀ required to prove φ. The…
Tarski's undefinability of truth
No consistent extension of arithmetic can define its own truth predicate. A semantic analogue of Gödel's incompleteness; motivates…
Rice's theorem
Any non-trivial semantic property of the partial-computable functions is undecidable — e.g. 'computes total function', 'outputs 42 on input…
Tarski semantic definition of truth
Alfred Tarski's recursive, compositional definition of truth-in-a-structure for a formal language: given an object language L and a…
Kolmogorov complexity
Length of the shortest program on a fixed universal machine U outputting x. Invariant up to O(1) across choices of U. Uncomputable: if K…
Busy beaver function
Maximum number of steps executed by an n-state 2-symbol Turing machine that halts on empty input. Uncomputable (grows faster than any…
Kleene's second recursion theorem
Every total computable f: ℕ → ℕ has an index e such that φ_e and φ_{f(e)} compute the same partial function. Proof by s_m_n plus diagonal.…
Gödel's completeness theorem (FOL)
For first-order logic, semantic validity coincides with syntactic provability. Proven by Gödel in his 1929 dissertation; Henkin's 1949…
Hilbert's 10th problem (Matiyasevich)
Matiyasevich 1970 (building on Davis-Putnam-Robinson 1961): every r.e. set has a Diophantine representation, so deciding integer…
Löb's theorem
In any Σ₁-complete theory containing PA, if the theory proves 'provability of φ implies φ', then it already proves φ. Generalises the…
Deduction theorem (propositional / FOL)
In classical propositional logic and in first-order logic (with suitable side conditions on free variables), assuming an extra hypothesis φ…
Arithmetical hierarchy
Stratification of arithmetic formulas by alternation depth of quantifiers over a Δ₀ (bounded) kernel. Σ₁ = r.e. sets, Π₁ = Con(T)-style…
Craig interpolation theorem
In classical first-order logic, whenever ⊢ φ → ψ there exists an interpolant χ — a formula whose non-logical symbols appear in both φ and ψ…
Herbrand's theorem
A purely existential first-order sentence ∃x⃗ φ(x⃗) (with φ quantifier-free) is provable iff a finite disjunction ⋁_i φ(t⃗_i) of ground…
Cut-elimination (Gentzen Hauptsatz)
Gentzen's Hauptsatz: every LK (or LJ) proof can be transformed into a cut-free proof. Gentzen 1935. Immediate corollaries: subformula…
Gentzen's consistency proof of PA (ε₀-induction)
Primitive recursive arithmetic plus transfinite induction up to (but not including) ε₀ — the first fixed point of α ↦ ω^α — proves the…
ω-consistency
A theory T extending PA is ω-consistent if there is no formula φ(x) such that T proves φ(n) for every standard numeral n yet also proves…
Turing reduction and degrees
A ≤_T B means A is computable by a Turing machine with oracle access to B. Equivalent to A being effectively decidable once membership…
Friedberg–Muchnik theorem
There exist computably enumerable sets A and B that are Turing-incomparable and both strictly below the halting problem — solving Post's…
Blum speed-up theorem
Blum 1967: for every total computable function r there exists a computable set A such that every TM M_i computing A admits another TM M_j…