Last changed 2026-04-15 · stable 1d · history

Extensions of Some Theorems of Gödel and Church

Reference: Rosser, J. Barkley (1936). “Extensions of some theorems of Gödel and Church.” Journal of Symbolic Logic 1(3), 87–91. DOI 10.2307/2269028. Open scan: JSTOR.

Summary

A five-page paper that sharpens Gödel’s first incompleteness theorem and Church’s undecidability theorem by replacing the hypothesis of ω-consistency with the weaker hypothesis of simple consistency. Gödel 1931 constructed, for an ω-consistent, effectively axiomatised theory P interpreting arithmetic, a sentence G ≡ "I am not provable in P"; Gödel could prove G is unprovable from simple consistency alone, but needed ω-consistency to exclude ¬G being provable. Rosser shows that by a clever modification of the self-referential sentence one can drop this stronger hypothesis.

The technical device — now universally known as the Rosser trick — replaces the Gödel sentence with a Rosser sentence R that says, informally, “for every proof of me, there is a smaller proof of my negation.” Formally, if Bew(y, x) is the proof predicate, R encodes ∀y. Bew(y, ⌜R⌝) → ∃z ≤ y. Bew(z, ⌜¬R⌝). Analysing the two cases — R provable or ¬R provable — now requires only simple consistency: from either provability claim together with consistency one extracts a contradiction by a primitive recursive comparison of proof lengths. Hence for any consistent, effectively axiomatised, sufficiently strong theory, R is independent. The same idea extends Church’s 1936 result: the set of theorems is not recursive, given only simple consistency.

Rosser’s paper is short, elegant, and methodologically paradigmatic: replacing an ω-style hypothesis by a simple hypothesis via a bounded-quantifier device is now a stock move in proof theory and recursion theory. The Rosser sentence itself is the standard presentation of the first incompleteness theorem in modern textbooks; Gödel’s original form is cited for historical reasons but Rosser’s is what students actually prove.

Key Ideas

Rosser sentence R: “every proof of me is matched by a smaller proof of my negation.”
Weakening hypothesis from ω-consistency to simple consistency in Gödel’s first theorem.
Rosser trick: bounded quantifiers comparing proof lengths resolve the two cases without ω-consistency.
Corresponding sharpening of Church’s undecidability theorem: theoremhood is not recursive under simple consistency alone.
Methodological template: ω-style hypotheses can often be replaced by simple hypotheses via bounded-quantifier comparisons.

Connections

Conceptual Contribution

Claim: Gödel’s first incompleteness theorem and Church’s theorem on the undecidability of first-order logic hold under the weaker hypothesis of simple consistency; ω-consistency is not needed.
Mechanism: Replace the Gödel sentence G ≡ ¬∃y. Bew(y, ⌜G⌝) with the Rosser sentence R ≡ ∀y. Bew(y, ⌜R⌝) → ∃z ≤ y. Bew(z, ⌜¬R⌝). Using only simple consistency, analyse supposed proofs of R or ¬R by comparing proof-length witnesses via bounded quantifiers; derive a contradiction in each case.
Concepts introduced/used: Rosser sentence, Rosser trick, simple vs. ω-consistency, bounded-quantifier self-reference, Consistency and Completeness
Stance: foundational technical paper (mathematical logic)
Relates to: Directly strengthens Gödel 1931 and Church 1936; the bounded-quantifier device is a methodological template reused throughout recursion theory and Kleene 1943’s hierarchy work.

Backlinks

Linked Pages

Recursive Predicates and Quantifiers

Reference: Kleene, Stephen C. (1943). “Recursive predicates and quantifiers.” Transactions of the American Mathematical Society 53(1), 41–73. DOI 10.2307/1990131. Open scan: ams.org / archive.org.

Summary

This paper is the single most influential structural paper of classical recursion theory. Kleene defines what is now called the arithmetical hierarchy: a stratification of sets and predicates on ℕ by the number and alternation of number-quantifiers prefixed to a decidable (recursive) matrix. A predicate is Σ⁰_n if it can be written ∃x₁ ∀x₂ ∃x₃ … R with n alternations and R recursive; Π⁰_n is the dual; Δ⁰_n = Σ⁰_n ∩ Π⁰_n. The recursive sets are precisely Δ⁰_1; the recursively enumerable sets are precisely Σ⁰_1. Each level of the hierarchy is strictly larger than the preceding one — the hierarchy theorem — and Kleene gives universal / complete predicates at each level.

The technical engine is a generalised normal form theorem: any Σ⁰_n predicate can be written with a single bounded block of quantifiers over a primitive recursive matrix, using Kleene’s T-predicate T_n for n-ary partial recursive functions and result-extractor U. The T-predicate first appears here in its mature form. Kleene then proves the enumeration theorem (there is a universal Σ⁰_1 predicate), the s-m-n theorem (recursive parameterisation of indices), and the hierarchy theorem (each level is strictly included in the next), and relates the hierarchy to the jump operator: A' (the halting problem relativised to A) moves one level up.

After 1943 every textbook treatment of computability theory — Rogers, Soare, Odifreddi — is organised around this hierarchy. Rice 1953’s classification of non-trivial index sets is a direct application: the index set of any non-trivial property is at least Σ⁰_1-hard or Π⁰_1-hard, and Rice–Shapiro and later refinements pin them to specific levels.

Key Ideas

Arithmetical hierarchy: Σ⁰_n, Π⁰_n, Δ⁰_n defined by alternation depth of number-quantifiers over a recursive matrix.
Recursive = Δ⁰_1; recursively enumerable = Σ⁰_1: the two “effective” classes located inside the hierarchy.
T-predicate T_n(e, x₁,…,x_n, y): primitive recursive “y codes a computation of {e}(x₁,…,x_n)”; canonical tool of the subject.
Normal form theorem at each level: one bounded matrix of primitive recursive content under n alternating quantifiers.
Enumeration theorem: universal predicate at each Σ⁰_n level.
s-m-n theorem: effective parameterisation of indices.
Hierarchy theorem: strict inclusions Σ⁰_n ⊊ Σ⁰_{n+1}; complete sets exist at each level (e.g. ∅^{(n)}, the nth jump).

Connections

Conceptual Contribution

Claim: The first-order definable subsets of ℕ are organised into a strict hierarchy by quantifier-alternation depth over a recursive matrix; recursive and r.e. sets are its first two levels.
Mechanism: Define Σ⁰_n / Π⁰_n / Δ⁰_n by prefixing n alternating number-quantifiers to recursive matrices; prove normal form via the T-predicate and unbounded search; prove enumeration, s-m-n, and hierarchy theorems by diagonalisation and the jump operator.
Concepts introduced/used: arithmetical hierarchy, T-predicate, s-m-n theorem, enumeration theorem, jump operator, Halting Problem, Recursive Function
Stance: foundational technical paper (recursion theory)
Relates to: Takes the normal form of Kleene 1936 and uses it to build the structural scaffolding that organises all of recursion theory; supplies the classification into which Post 1944 places simple and creative sets and which Rice 1953 uses to classify non-trivial index sets; second-order analogue developed by Mostowski 1946.

An Unsolvable Problem of Elementary Number Theory

Reference: Church, Alonzo (1936). “An unsolvable problem of elementary number theory.” American Journal of Mathematics 58(2), 345–363. DOI 10.2307/2371045. Scan: archive.org via JSTOR mirror.

Summary

Church’s 1936 paper is one of the two founding documents of computability theory (the other being Turing 1936). It formulates and defends what came to be called Church’s thesis: the identification of the informal notion of an effectively calculable function of positive integers with the precisely defined class of λ-definable functions (equivalently, the general recursive functions of Herbrand–Gödel–Kleene, as Church and Kleene had shown earlier that year). Against that identification, Church exhibits a problem of elementary number theory that no effectively calculable procedure can solve, thereby producing the first concrete undecidable problem in mathematics.

The technical core is a diagonal construction inside the λ-calculus. Church shows that the set of λ-terms having a normal form is not recursive; equivalently, there is no effective procedure that, given a λ-term, decides whether it is convertible to a normal form. By encoding this into ordinary number theory via Gödel numbering, he obtains an unsolvable problem expressible as a question about positive integers. In the paper’s final sections he applies the technique to the Entscheidungsproblem of first-order logic: the decision problem for provability in pure predicate calculus is itself undecidable. (Turing 1936, submitted independently, reaches the same conclusion via the halting problem.)

The paper is historically decisive because it provides (i) the first mathematically rigorous definition of effective calculability, (ii) the first proof of an unsolvable mathematical problem, and (iii) the first proof of the undecidability of first-order logic. Every subsequent undecidability result — Post’s correspondence problem, Hilbert’s 10th, word problems in groups, Rice’s theorem — is methodologically descended from this paper.

Key Ideas

Church’s thesis: effectively calculable = λ-definable = general recursive. The informal notion is identified with a precise mathematical class.
λ-definability and the equivalence (with Kleene) of λ-definability and Herbrand–Gödel general recursiveness.
Undecidability of normal-form existence for λ-terms — the first explicit undecidable problem.
Undecidability of the Entscheidungsproblem: no algorithm decides validity in first-order logic.
Diagonal / self-referential construction as the standard technique for undecidability.
Gödel-numbering of λ-terms brings the result back into elementary number theory.

Connections

Conceptual Contribution

Claim: There exist problems of elementary number theory for which no effective procedure exists; in particular, the decision problem for first-order logic is unsolvable.
Mechanism: Identify effectively calculable with λ-definable. Diagonalise over λ-terms to produce a set whose characteristic function is not λ-definable. Transport the result into first-order logic via arithmetisation, yielding undecidability of the Entscheidungsproblem.
Concepts introduced/used: Lambda Calculus, Recursive Function, Church’s thesis, Entscheidungsproblem, Computability, First-Order Logic
Stance: foundational theorem paper (mathematical logic / computability)
Relates to: Independent and contemporaneous with Turing 1936; together they establish the computability frontier that Rice 1953 later generalises; provides the undecidability backdrop against which Gödel 1931 is read today.

Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I

Reference: Gödel, Kurt (1931). “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I” [“On formally undecidable propositions of Principia Mathematica and related systems I”]. Monatshefte für Mathematik und Physik 38, 173–198. English translation in van Heijenoort (ed.), From Frege to Gödel (Harvard 1967), and in Gödel, Collected Works I (Oxford 1986). Scan: monatshefte-fuer-mathematik @ archive.org; English: Meltzer/Braithwaite 1962.

Summary

Gödel’s 1931 paper proves the two incompleteness theorems that permanently reshaped mathematical logic. The first theorem states that for any ω-consistent, effectively axiomatised formal system P strong enough to formalise elementary arithmetic, there exists a sentence G in the language of P such that neither G nor ¬G is provable in P. The second theorem states that if P is consistent, then P cannot prove its own consistency statement Con(P). Together they show that Hilbert’s programme — to secure classical mathematics by a finitary consistency proof of a sufficiently strong formal system — cannot succeed in its original form.

The technical machinery is the one mathematicians still use. Gödel introduces Gödel numbering, an injective encoding of formulas and proofs as natural numbers, which allows syntactic notions (“x is the Gödel number of a proof of the formula with Gödel number y”) to be expressed as arithmetic predicates. He then establishes the representability of all primitive recursive predicates in P and constructs, via a fixed-point / diagonal lemma, a sentence G that is in effect self-referential: G says “I am not provable in P.” An analysis of the two cases — G provable, ¬G provable — using ω-consistency yields the first theorem. Formalising that analysis inside P itself yields the second.

The paper is the mathematical origin of self-reference as a tool, of arithmetisation of syntax, and of the technique — later generalised by Tarski, Church, Turing, and Kleene — for transferring undecidability phenomena between formal systems. It also establishes the class of primitive recursive functions as the workhorse notion of effectivity in the paper, the direct ancestor of Kleene’s general recursive functions. The incompleteness theorems remain the single most cited and philosophically consequential results of twentieth-century logic.

Key Ideas

Gödel numbering: arithmetisation of syntax, turning formulas and proofs into natural numbers.
First incompleteness theorem: every ω-consistent, effectively axiomatised, sufficiently expressive theory contains a true-but-unprovable sentence.
Second incompleteness theorem: no such theory can prove its own consistency.
Diagonal / fixed-point lemma: every arithmetic predicate has a self-referential instance.
Primitive recursive functions as the effective-syntax layer (precursor to general recursive functions).
Representability: every primitive recursive relation is definable in P.
The shattering of Hilbert’s programme in its finitist form.

Connections

Conceptual Contribution

Claim: No effectively axiomatised, ω-consistent theory that interprets arithmetic is complete; no such consistent theory proves its own consistency.
Mechanism: Encode syntax as natural numbers (Gödel numbering). Represent primitive recursive predicates (including the proof relation Bew) inside the theory. Construct a self-referential sentence G ≡ ¬∃y. Bew(y, ⌜G⌝) via a diagonal lemma; analyse cases using ω-consistency for theorem I; formalise that analysis to obtain theorem II.
Concepts introduced/used: Gödel numbering, primitive recursive functions, representability, diagonal lemma, ω-consistency, Consistency and Completeness, First-Order Logic
Stance: foundational theorem paper (mathematical logic)
Relates to: The methodological parent of Church 1936 and Turing 1936; sharpened by Rosser 1936 (dropping ω-consistency); the arithmetisation technique underwrites all later work on effectively axiomatised theories, including the hierarchies of Kleene 1943 and Mostowski 1946.

Consistency and Completeness

Two classical axiomatic-method properties of a deductive system: consistency (no contradictions provable) and completeness (every semantically valid statement is provable); Floyd’s program-proof method depends on analogous properties for the inductive-assertion method.

In this vault

Assigning Meanings to Programs
Hoare Logic
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I — Gödel 1931, the incompleteness theorems.
Extensions of Some Theorems of Gödel and Church — Rosser 1936, strengthens Gödel’s result to assume only simple consistency.

Classes of Recursively Enumerable Sets and Their Decision Problems

Reference: Rice, H. G. (1953). Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2), 358–366. DOI 10.2307/1990888. Based on Rice’s 1951 Princeton PhD thesis under Alonzo Church.

Summary

A nine-page paper that established one of the most consequential results in computability theory — now universally known as Rice’s Theorem. Rice’s question: given a class C of recursively enumerable (r.e.) sets, is there an effective procedure that, applied to a Gödel number (index) of an r.e. set W, decides whether W ∈ C? The paper’s central result is that the answer is no whenever C is a non-trivial extensional property — i.e. whenever C is neither empty nor the whole collection of r.e. sets, and membership in C depends only on which set is described, not on how it is described. Every property of the computed function itself (as opposed to syntactic properties of the program text) is therefore undecidable.

The proof is a reduction from the halting problem (Turing’s K). Rice constructs, for an arbitrary index i, a machine whose r.e. set is either a fixed element of C or a fixed element of its complement depending on whether φ_i(i) halts; a decision procedure for C would then decide K, which is known impossible. The technique — parametric construction of “switch” machines that toggle semantic behaviour based on a halting oracle — is the template used throughout undecidability theory for subsequent results (Rogers’ isomorphism theorem, the Myhill isomorphism, the theory of m-reducibility).

Beyond the headline theorem, the paper classifies decision problems about r.e. sets by the logical complexity of the class C: some non-trivial classes are Σ₁-hard, others Π₁-hard, others fall at higher levels of the arithmetical hierarchy. This classification anticipates the later development of degree theory. The paper is short, elementary, and entirely foundational: it tells us, once and for all, that semantic questions about arbitrary programs cannot be answered by mechanical inspection. Every program-analysis, verification, and capability-bounding enterprise since has been organised around the frontier Rice drew — by restricting the class of programs considered, approximating (sound-but-incomplete), or proving properties syntactically rather than semantically.

Key Ideas

Theorem B (Rice’s Theorem): for any non-trivial class C of r.e. sets, the problem of deciding whether a given r.e. set belongs to C is undecidable.
Extensional vs. intensional properties: C must depend on what is computed (the set), not on how (the index/program text). Intensional properties (program size, presence of a given opcode) can be decidable.
Proof by reduction from the halting problem, via a parametric “switch” construction that conditionally produces an element of C or its complement depending on whether a reference computation halts.
Arithmetical hierarchy classification of classes of r.e. sets by the quantifier complexity of their defining predicates, foreshadowing Kleene’s and Rogers’ later work.
Implicit corollary: every tool that claims to decide a non-trivial semantic property of arbitrary programs must either (i) restrict the input class, (ii) approximate, or (iii) violate computability.

Connections

Conceptual Contribution

Claim: There is no uniform effective procedure that decides any non-trivial extensional property of recursively enumerable sets; equivalently, every non-trivial semantic property of the partial function computed by an arbitrary program is undecidable.
Mechanism: Given a hypothesised decision procedure for a non-trivial class C, and a distinguishing pair A ∈ C, B ∉ C, construct for each index i a machine M_i that simulates φ_i(i) and, if it halts, begins enumerating A; otherwise enumerates B. The set enumerated by M_i is in C iff φ_i(i) halts, so a decision procedure for C would decide the halting problem — contradiction.
Concepts introduced/used: Rice’s Theorem, Halting Problem, Computability, Recursive Function, Universal Turing Machine
Stance: foundational theorem paper (computability theory)
Relates to: Generalises Turing’s halting theorem from the specific property “halts on input x” to all non-trivial semantic properties; sets the decidability frontier that all subsequent work in Formal Verification, Static Analysis, and LangSec (Security Applications Of Formal Language Theory, The Halting Problems of Network Stack Insecurity) must respect; directly underwrites the Rice’s-theorem argument in House on Rock - LangSec in Ethereum Classic that Ethereum’s gas mechanism cannot deliver a semantic safety guarantee.

Recursively Enumerable Sets of Positive Integers and Their Decision Problems

Reference: Post, Emil L. (1944). “Recursively enumerable sets of positive integers and their decision problems.” Bulletin of the American Mathematical Society 50(5), 284–316. Open scan: projecteuclid.org / ams.org.

Summary

Post’s 1944 paper is the programmatic manifesto of modern recursion theory. Writing in a remarkable, informal expository voice, Post sets aside the technical frameworks of his predecessors and asks a simple structural question: among the recursively enumerable (r.e.) sets — those arising as ranges of partial recursive functions — which can be solved (are recursive) and which cannot, and what is the structure of the unsolvable ones? He introduces the central reducibility notions, exhibits several families of non-recursive r.e. sets of different kinds, and poses the question that dominated recursion theory for the next dozen years.

Post defines many-one reducibility (A ≤_m B: a total recursive f with x ∈ A ↔ f(x) ∈ B), its injective restriction one-one reducibility (A ≤_1 B), and truth-table reducibility, alongside Turing’s relative computability. He defines a set to be creative if, roughly, one can effectively produce, for any r.e. set W_e disjoint from the set, a witness outside both — showing that the complement cannot be enumerated. The halting problem K is creative; every creative set is m-complete for r.e. sets (i.e. “maximally unsolvable” under ≤_m). To show that m-unsolvability is not the whole story, Post constructs simple sets: r.e. sets whose complements are infinite but contain no infinite r.e. subset. Simple sets are not creative and their construction uses the first real priority argument in the literature — finite-injury in embryo.

The paper closes with Post’s problem: does there exist a non-recursive r.e. set that is not Turing-complete — i.e. an r.e. Turing-degree strictly between 0 and 0'? Post could not answer it. The problem was solved affirmatively by Friedberg and Muchnik in 1956 via the finite-injury priority method, launching modern degree theory. Every notion here — reducibility, creative sets, simple sets, the priority technique, the question of intermediate degrees — became foundational. Rice’s 1953 theorem is a direct descendant: Rice’s index sets are all m-complete for r.e. sets, hence creative, hence undecidable.

Key Ideas

Recursively enumerable set: range of a partial recursive function; equivalently Σ⁰_1.
Many-one, one-one, and truth-table reducibilities, distinct from Turing reducibility, organising r.e. sets into degree-like structures.
Creative sets: r.e. sets whose complements cannot be effectively enumerated in the strongest sense; equivalent to m-complete r.e. sets; K is creative.
Simple sets: r.e. sets with infinite complement containing no infinite r.e. subset — not m-complete, so “less unsolvable” than creative sets.
Priority argument (embryonic): construction of simple sets by meeting infinitely many requirements with finite injury.
Post’s problem: existence of an r.e. set of intermediate Turing degree — open in 1944, solved 1956.
Programmatic style: readable English prose, motivating the entire subject.

Connections

Conceptual Contribution

Claim: The class of r.e. sets has rich internal structure under various reducibilities; there exist m-complete (creative) r.e. sets and non-m-complete non-recursive (simple) r.e. sets; whether there are r.e. sets of intermediate Turing degree is open.
Mechanism: Introduce m-, 1-, and tt-reducibilities; prove K is creative and creative sets are m-complete; construct simple sets by a finite-injury priority argument enumerating r.e. sets W_e and injecting a witness from each into the set while protecting the complement’s infinity; raise the existence of intermediate Turing degrees as the central open problem.
Concepts introduced/used: r.e. set, many-one / one-one / truth-table reducibility, creative set, simple set, priority argument, Post’s problem, Halting Problem
Stance: programmatic / foundational paper (recursion theory)
Relates to: Extends the undecidability of Church 1936 and Gödel 1931 into a structural theory of unsolvable problems; furnishes the reducibilities and completeness notions that Rice 1953 uses; its priority argument is the engine of all subsequent degree theory.

Halting Problem

Turing’s theorem that no algorithm can decide, for every program-input pair, whether execution terminates. Sassaman et al. invoke it to argue that recognising arbitrary network inputs is equivalently undecidable, so protocols must be restricted to decidable (ideally regular or context-free) languages.

In this vault

The Halting Problems of Network Stack Insecurity
LangSec
An Unsolvable Problem of Elementary Number Theory — Church 1936, the co-originating undecidability result (Entscheidungsproblem).
Recursively Enumerable Sets of Positive Integers and Their Decision Problems — Post 1944, foundational treatment of unsolvability and degrees.
General Recursive Functions of Natural Numbers — Kleene 1936, the recursive-function framing equivalent to Turing/Church.

Computability

Theory of which functions can be computed by a Turing machine; the undecidability of the halting problem is the load-bearing result behind LangSec arguments about parser safety.

In this vault

Exploit Programming - From Buffer Overflows To Weird Machines
The Halting Problems of Network Stack Insecurity
Chomsky Hierarchy
An Unsolvable Problem of Elementary Number Theory — Church 1936.
General Recursive Functions of Natural Numbers — Kleene 1936.
Recursive Predicates and Quantifiers — Kleene 1943, arithmetical hierarchy.
Recursively Enumerable Sets of Positive Integers and Their Decision Problems — Post 1944.

First-Order Logic

The classical logic of quantifiers over individuals, predicates and functions, with sound and complete proof systems. It provides the baseline expressiveness against which logic-programming, description and modal logics are measured.

In this vault

Foundations of Logic Programming - Lloyd
Horn Clauses
Description Logics
An Unsolvable Problem of Elementary Number Theory — Church 1936, undecidability of first-order logic (the Entscheidungsproblem).

Extensions of Some Theorems of Gödel and Church

Summary

Key Ideas

Connections

Conceptual Contribution

Tags

Backlinks