Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
1931 · paper · Mathematics and statistics
Shows that formal systems such as Principia Mathematica and Zermelo-Fraenkel set theory contain relatively simple statements about ordinary whole numbers that cannot be decided from their axioms. The result holds for a very broad class of formal systems.
Checked: PDF from w-k-essler.de, fetched 4 Oct 2026. Page numbers are those of that PDF.
1 finding
Substance Definition (5) prints "Bw_κ(x) ≡ (n)[n ≤ l(x) → Ax(n Gl x) ∨ (n Gl x) ε κ ∨ ...]" without the lower bound "0 < n" that appears in Definition 44, which (5) cites as its analogue ("vgl. den analogen Begriff 44").
- p. 16 Formula (5), definition of Bw_κ(x)
(vgl. den analogen Bcgriff 44)
- p. 15 Definition 44, Bw(x)
44. Bw(x) _~(n) {0 < .~@)
- p. 16 Equation (5)
(vgl. den analogen Begriff 44)
- p. 15 Definition 44
Bw(x) ≡ (n) {0 < n ≤ l(x) → Ax (n Gl x) ∨
Judge's note: Compared the crop of (5) on printed p. 187 with the crop of Definition 44 on printed p. 186. Definition 44 has "0 < n ≤ l(x)"; (5) has "n ≤ l(x)". For n = 0, 0 Gl x = 0, which is not an axiom, not a formula in κ, and has no predecessors p, q < 0. Read literally, Bw_κ(x) could therefore never hold. The evident fix is to insert 0 < n.
Second check: another model agreed
Report a problem with this finding
1 minor (typos and the like; most checked by the judge only)
Typo In the proof sketch on printed p. 175 the text reads "Wäre dagegen die Negation von [R(q); q] beweisbar, so würde n ε K" (overlined), where the specific number q is meant (q ε K overlined).
- p. 4 Section 1, proof sketch of undecidability of [R(q); q]
so würde n ε K,
Judge's note: Checked page 4. The overlined "n ε K" is printed. Every other step of the paragraph uses q, and the argument concerns the particular q with S = R(q), so n is a slip for q. The intended meaning is recoverable from context.
Second check: none (judge only)