On Computable Numbers, with an Application to the Entscheidungsproblem

Reference: Turing, Alan M. (1936). “On computable numbers, with an application to the Entscheidungsproblem.” Proceedings of the London Mathematical Society, series 2, vol. 42, pp. 230–265 (read 1936, published 1937); correction in vol. 43 (1937), pp. 544–546. DOI 10.1112/plms/s2-42.1.230. Scan: cs.virginia.edu/~robins.

Summary

Turing’s 1936 paper is, with Church 1936, one of the two founding documents of computability theory. Its purpose is to make precise the informal idea of an effective procedure, and then to settle Hilbert’s Entscheidungsproblem — the question of whether there is a mechanical decision procedure for validity in first-order logic. Turing’s answer is negative, and the machinery he builds to reach it defines the field.

The central construction is the abstract computing machine (Turing’s “a-machine”, now the Turing machine): a device with a finite set of internal m-configurations, a two-way infinite tape divided into squares, and a head that reads and writes symbols and moves one square at a time according to a finite table of behaviour. A real number is computable when its digits can be written out by such a machine. Turing then shows how to encode any machine’s table as a single integer — its standard description / description number — and constructs a universal machine that, given the description number of any machine M, reproduces M’s behaviour. This is the theoretical origin of the stored-program computer: one machine that runs any program supplied as data.

From here the negative results follow by a diagonal argument. Turing distinguishes circle-free machines (which go on printing digits forever) from circular ones, and proves that no machine can decide, of an arbitrary machine’s description number, whether it is circle-free — the ancestor of the modern halting problem. Applying the same self-referential technique to logic, he shows there can be no general effective procedure deciding whether a first-order formula is provable, so the Entscheidungsproblem is unsolvable. An appendix argues that Turing-computability coincides with Church’s λ-definability (and hence with Herbrand–Gödel–Kleene general recursiveness), the equivalence that grounds the Church–Turing thesis.

Key Ideas

Turing machine (a-machine): finite m-configurations + unbounded tape + read/write head governed by a finite behaviour table — a precise model of effective calculation.
Computable numbers/functions: reals (and functions) whose digits an a-machine can generate; the computable reals are countable.
Standard description / description number: an arithmetic encoding of a machine’s table, letting machines take other machines as input.
Universal Turing Machine (U): a single machine that simulates any machine from its description number — the conceptual root of the stored-program computer.
Circle-free vs circular machines, and the undecidability of circle-freeness by diagonalisation — ancestor of the Halting Problem.
Undecidability of the Entscheidungsproblem: no effective procedure decides validity/provability in first-order logic.
Church–Turing equivalence: Turing-computability = λ-definability = general recursiveness (appendix).

Connections

Conceptual Contribution

Claim: The informal notion of effective calculability is captured exactly by the Turing machine; there is no machine that decides circle-freeness, and consequently the Entscheidungsproblem for first-order logic is unsolvable.
Mechanism: Model computation as a finite-state machine over an unbounded tape; arithmetise machines as description numbers so a universal machine can simulate any machine; diagonalise over description numbers to produce a problem no machine can decide, then transport that undecidability into first-order provability.
Concepts introduced/used: Universal Turing Machine, Computability, Halting Problem, Diagonalization, Church–Turing thesis, Entscheidungsproblem, First-Order Logic
Stance: foundational theorem paper (mathematical logic / computability)
Relates to: Independent of and contemporaneous with Church 1936, with which it is equated in the appendix; extends the self-reference lineage of Cantor 1891 and Gödel 1931; the undecidability frontier it opens is generalised by Rice 1953 and its universal machine anticipates von Neumann’s universal construction.

Backlinks

Linked Pages

Theory of Self-Reproducing Automata

Theory of Self-Reproducing Automata (Fourth Lecture: The Role of High and of Extremely High Complication)

Reference: von Neumann, J. (edited and completed by Arthur W. Burks) (1966). University of Illinois Press. Source file: VonNeumann.pdf. URL

Summary

This excerpt is the Fourth Lecture of von Neumann’s posthumously edited Theory of Self-Reproducing Automata. Von Neumann compares natural automata (nervous systems) with artificial computing machines across size, speed, energy dissipation per elementary act of information, and error characteristics. He observes that although vacuum tubes are vastly larger and less energy-efficient than neurons, both are far above the thermodynamic minimum — suggesting physics does not fully explain the size gap; reliability likely does.

The core argument concerns complication: below a threshold, a system cannot perform certain tasks at all; above it, qualitatively new behaviors (including self-reproduction and evolution) become possible. Natural automata tolerate errors locally rather than halting on any single fault, an architectural stance he contrasts with the “single-error” fragility of contemporary computers. The discussion foreshadows modern views on redundancy, fault tolerance, and emergent capabilities with scale.

Key Ideas

Complication threshold enables qualitatively new behavior.
Natural automata survive local errors; artificial automata halt.
Analog-digital mixture characterizes biological computation.
Size and reliability trade-offs shape architecture.
Precursor to self-reproducing and evolvable systems theory.

Connections

Self-Adaptive Systems
Multi-Agent Systems
Edge Intelligence
Large Population Models
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — modern self-replicating agent, direct lineal descendant
Myconet Fungi Inspired Superpeer Overlay — biological self-organisation
Computational Boundary of a Self — selfhood extended to scale-free cognition
Programming Erlang Second Edition — engineered local-error-tolerance

Conceptual Contribution

Claim: There exists a threshold of “complication” below which automata can only degrade and above which qualitatively new capacities (self-reproduction, evolvable organisation) become possible; biological automata survive precisely because their architecture tolerates local error rather than halting on any single fault.
Mechanism: Von Neumann juxtaposes nervous systems and vacuum-tube computers along size, energy-per-information-act, speed, and error characteristics, noting both far exceed thermodynamic minima so the gap must be architectural. He then argues that digital-analog hybrids with distributed redundancy exhibit error-tolerant behaviour that Turing-style halting-on-first-error machines cannot match, and frames this as a prerequisite for crossing the complication threshold that enables open-ended evolution.
Concepts introduced/used: Complication Threshold, Self-Reproducing Automata, Fault Tolerance, Redundancy, Digital-Analog Hybrid, Error Halting, Natural vs Artificial Automata
Stance: foundational
Relates to: A philosophical wellspring for the “let it crash” supervision of Programming Erlang Second Edition, the fault-tolerance patterns of Architectural Patterns for Dependable Software Systems - SOL, the robustness concerns of Are Multiagent Systems Resilient to Communication Failures, and the emergent-complexity framing behind Computational Boundary of a Self.

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.

Ü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.

Über eine elementare Frage der Mannigfaltigkeitslehre

Reference: Cantor, Georg (1891). “Über eine elementare Frage der Mannigfaltigkeitslehre.” Jahresbericht der Deutschen Mathematiker-Vereinigung 1, 75–78. English (“On an Elementary Question of the Theory of Manifolds”) in Ewald, From Kant to Hilbert, vol. 2, Oxford 1996.

Summary

The four-page note in which Cantor introduces the diagonal argument and, with it, the modern proof that there are different sizes of infinity. Having already shown in 1874 (by a nested-intervals argument) that the real numbers cannot be enumerated, Cantor here gives a far simpler and more general method. He considers the collection of all infinite sequences over two symbols (he uses m and w) — equivalently, all functions from the natural numbers into a two-element set. Assume such sequences could be listed as E₁, E₂, E₃, …. Define a new sequence E₀ whose n-th entry is chosen to differ from the n-th entry of Eₙ (flip m↔w down the diagonal). Then E₀ differs from every Eₙ in at least one place, so it is absent from the list — contradiction. The collection of such sequences is therefore not enumerable.

Cantor immediately generalises. For any set M, the totality of functions from M into a two-element set — i.e. the power set of M — has a strictly greater cardinality than M itself. This is Cantor’s theorem: |M| < |𝒫(M)|. Its consequence is that there is no largest cardinality and no “set of all sets” of maximal size; instead the transfinite cardinalities form an unending ascending hierarchy. The argument is purely combinatorial — no analysis, no topology of the line — which is exactly why it became the template for every later self-referential limitative result.

The diagonal method is the paper’s lasting bequest. Gödel’s incompleteness construction, Turing’s and Church’s undecidability proofs, Russell’s paradox, and Tarski’s undefinability of truth are all recognisably the same move: build an object that disagrees, along the diagonal, with every member of a purported complete enumeration. The 1891 note is where that move is first made explicit and abstracted away from the particular case of the reals.

Key Ideas

The diagonal argument: from any enumeration of sequences, construct one differing from the n-th at position n; it cannot be in the list.
Uncountability of the set of infinite binary sequences (hence of the reals, of 𝒫(ℕ)).
Cantor’s theorem: for every set M, |M| < |𝒫(M)| — the power set is strictly larger.
No largest cardinal: transfinite cardinalities form an unbounded ascending hierarchy.
Combinatorial, not analytic: the proof needs nothing about the continuum beyond counting, making it general.
Template for self-reference: the structural seed of Gödel, Turing, Church, Russell, Tarski.

Connections

Conceptual Contribution

Claim: For any set M, there are strictly more subsets of M than elements of M; hence infinite sets come in distinct, unboundedly increasing sizes.
Mechanism: Suppose an enumeration of all sequences/subsets exists; diagonalise to manufacture one that differs from each listed item at its own index; the manufactured item is therefore unlisted — contradiction.
Concepts introduced/used: Diagonalization, Cardinality, Power Set, Cantor’s Theorem, Transfinite Numbers
Stance: foundational theorem paper (set theory / foundations of mathematics)
Relates to: Furnishes the diagonal method later turned into a limitative weapon by Gödel 1931 and Church 1936; the cardinality questions it opens (how large is 𝒫(ℕ)?) become the Continuum Hypothesis, settled as independent by Cohen 1963.

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.

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).

Diagonalization

A self-referential proof technique: given any purported complete enumeration of objects, construct a new object that disagrees with the n-th listed object at “position n”, so the new object cannot appear anywhere in the list — a contradiction. Introduced by Cantor (1891) to prove that the infinite binary sequences (equivalently 𝒫(ℕ), the reals) cannot be enumerated, establishing distinct sizes of infinity and Cantor’s Theorem. The same structural move recurs throughout the limitative results of logic and computation: Gödel’s incompleteness construction (a sentence asserting its own unprovability), Turing’s halting problem and Church’s undecidability of the Entscheidungsproblem (a program that contradicts any decider applied to itself), Russell’s Paradox, and Tarski’s undefinability of truth. Diagonalization is thus the common engine behind “no system can completely capture / enumerate / decide its own scope.”

In this vault

Über eine elementare Frage der Mannigfaltigkeitslehre — Cantor 1891 (origin)
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I — Gödel 1931
An Unsolvable Problem of Elementary Number Theory — Church 1936
Classes of Recursively Enumerable Sets and Their Decision Problems — Rice 1953
Set 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.

Universal Turing Machine

A Turing machine that, given the encoding of an arbitrary machine and an input, simulates that machine’s behaviour on the input. Its existence is the foundation of general-purpose computation and of algorithmic information theory.

In this vault

General Recursive Functions of Natural Numbers

Reference: Kleene, Stephen C. (1936). “General recursive functions of natural numbers.” Mathematische Annalen 112, 727–766. DOI 10.1007/BF01565439. Open scan: GDZ Göttingen.

Summary

Kleene’s 1936 paper develops the theory of the general recursive functions — the class proposed by Herbrand in correspondence with Gödel and given a precise definition by Gödel in his 1934 Princeton lectures. Kleene formalises the Herbrand–Gödel scheme (systems of equations closed under substitution and replacement of equals) as the official definition of effectively calculable function in the recursion-theoretic tradition, and he proves the equivalence of this class with the λ-definable functions of Church and Kleene. After this paper, “general recursive,” “λ-definable,” and (shortly thereafter) “Turing computable” are known to name the same class of functions — the empirical content of Church’s thesis.

The central technical result is the normal form theorem. Kleene shows that every general recursive function can be written as φ(x) = U(μy. T(e, x, y) = 0), where T is a primitive recursive Kleene T-predicate encoding “y is the Gödel number of a computation of machine/equation-system e on input x,” U is a primitive recursive result-extracting function, and μy. is the unbounded minimisation (least-y) operator. All of the apparent complexity of recursive definitions is thereby pushed into one unbounded search over a primitive-recursive predicate. The theorem provides a canonical form for every partial recursive function — the starting point of computability as a structural theory rather than a list of closure rules.

The paper also clarifies the role of partial functions, introduces the use of indices e as first-class objects (each function gets a Gödel number so one can reason about φ_e), and establishes the technology — T-predicate, μ-operator, index encoding, normal form — that Kleene and others use in every subsequent paper on recursion theory.

Key Ideas

General recursive functions (Herbrand–Gödel equation calculus) adopted as the working definition of effective calculability.
Equivalence with λ-definable functions: Church’s thesis gains an additional leg.
Kleene normal form theorem: every partial recursive function φ_e(x) = U(μy. T(e, x, y) = 0).
T-predicate T(e, x, y): a primitive recursive relation formalising “y codes a computation of e on x.”
μ-operator (unbounded minimisation) as the one non-primitive-recursive ingredient needed.
Indices e for recursive functions — functions become numbers, enabling self-reference and universal machines.

Connections

Conceptual Contribution

Claim: The general recursive functions coincide with the λ-definable functions and admit a single normal form U(μy. T(e, x, y) = 0) reducing all partial recursive computation to unbounded search over a primitive recursive predicate.
Mechanism: Take Herbrand–Gödel equation calculus as primitive. Arithmetise derivations to get a primitive recursive “is-a-computation” predicate T. Use unbounded search (μy) to locate the first terminating computation; extract its result with a primitive recursive U. Cross-simulate with λ-calculus to prove equivalence.
Concepts introduced/used: general recursive function, T-predicate, μ-operator, normal form, index, Recursive Function, Computability
Stance: foundational theorem paper (recursion theory)
Relates to: Second leg (with Church 1936) of Church’s thesis; the normal form becomes the tool by which Kleene 1943 constructs the arithmetical hierarchy and Post 1944 organises r.e. sets; supplies the machinery that Rice 1953 takes for granted.

Lambda Calculus

A formal system introduced by Church that expresses computation via function abstraction and application. It serves as a foundational model of computation and the theoretical basis for functional programming languages.

In this vault

Security Kernel Lambda Calculus
An Unsolvable Problem of Elementary Number Theory — Church 1936, the λ-calculus applied to the Entscheidungsproblem.

Recursive Function

Function defined in terms of itself; McCarthy’s Lisp made recursion — not iteration — the default mechanism of computation.

In this vault

Recursive Functions of Symbolic Expressions and Their Computation by Machine
Foundations of Logic Programming - Lloyd
General Recursive Functions of Natural Numbers — Kleene 1936, the defining paper for the general-recursive class.
Recursive Predicates and Quantifiers — Kleene 1943, extends the theory to predicates and the arithmetical hierarchy.

On Computable Numbers, with an Application to the Entscheidungsproblem

Summary

Key Ideas

Connections

Conceptual Contribution

Tags

Backlinks