On Computable Numbers, with an Application to the Entscheidungsproblem
1936 · paper · Computer science
Defines computable numbers as those whose decimals a machine can write down, and shows they form an enumerable class that excludes some definable numbers. It concludes that Hilbert's Entscheidungsproblem (decision problem) has no solution.
Checked: PDF from cs.virginia.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance Table for U, row sh2 / D: "R, R, R, R sh2"; the final m-configuration should evidently be sh3.
- p. 16 Table for U, m-configuration sh2 (p. 245)
R, R, R, R
Judge's note: Page 16 image: the D row of sh2 ends in sh2, and the subscript 2 is legible. No other entry in the table leads to sh3, so as printed sh3, sh4 and sh5 can never be reached. The machine could then never print the 0: or 1: that the sh gloss describes. The fix is evident: replace sh2 with sh3 in that row.
Second check: another model agreed
Report a problem with this finding
Substance §11, p. 260, definition of Inst{q_i S_j S_k L q_l}: the last conjunct "(z)[F(y', z) v (R_{S_j}(x, z) → R_{S_k}(x', z))]" does not say that squares other than y are unchanged.
- p. 31 Definition of Inst{q_i S_j S_k L q_l}
& (z)[F(y', z) v (R_Sj(x, z) → R_Sk(x', z))]
Only the authors can say what is right here.
Judge's note: I reworked the formula from the image on page 31. The antecedent contains F(y', y), so y' is the square to the left of y, and F(y', z) holds exactly when z = y. For every other square z the conjunct only requires that if z bears S_j in x, it bears S_k in x'. Squares bearing any other symbol S_m (m ≠ j) in x are left unconstrained in x', and other S_j squares are forced to S_k. A frame condition would need R_{S_m}(x, z) → R_{S_m}(x', z) for every symbol m. As printed, the step on p. 261 that Inst & F^(n+1) → (CC_n → CC_{n+1}) cannot be derived: CC_{n+1} asserts the symbols on all squares, and Inst gives no information about squares holding symbols other than S_j. So the proof of Lemma 1 fails as printed. No correction notice is in the files.
Second check: another model agreed
Report a problem with this finding
Reference or label §11, p. 260: "Let us put the description of M into the first standard form of § 6". The first standard form is defined in § 5 (Enumeration of computable sequences), not § 6.
- p. 31 §11, paragraph after definition of Inst
Let us put the description of .11 into the first standard form of § 6.
- p. 12 §5, worked example
Our first standard form would be
- p. 31 §11, paragraph defining Des(M)
Let us put the description of .U into the first standard form of § 6.
- p. 10 §5, Enumeration of computable sequences
It will be useful to put these tables into a kind of standard form.
Judge's note: Page 31 prints "§ 6". In the text, the §5 heading is at line 572 and the §6 heading (The universal computing machine) at line 695. The standard form is introduced at line 578 ("put these tables into a kind of standard form"), and "Our first standard form would be" is at line 679, both inside §5. §6 defines no standard form. No correction notice is in the files.
Second check: another model agreed
Report a problem with this finding
Wording Proof of Lemma 1, p. 261: "r(n, i(n)) = a, r(n+1, i(n+1)) = c, k(i(n)) = b, and k(i(n+1)) = d". The indices are mixed up for Inst{q_a S_b S_d L q_c}.
- p. 32 Lemma 1 proof, definition of a, b, c, d
r(n-\-l, i(n-\-l)} = c, k(i(n)j =b, and k(i(n-\-l)) =d,
- p. 32 Proof of Lemma 1, case of a move to the left
r(n, i(n)) = a, r(n+1, i(n+1)) = c, k(i(n)) = b, and k(i(n+1)) = d
Only the authors can say what is right here.
Judge's note: I checked page 32. In Inst{q_a S_b S_d L q_c}, a and c index m-configurations and b and d index symbols. The same page defines the m-configuration as q_{k(n)} (k takes the configuration index n) and the symbols as S_{r(n, ·)}. The printed text gives a and c symbol values via r, gives b and d m-configuration values via k, and applies k to i(n). An assignment consistent with the definitions is a = k(n), b = r(n, i(n)), d = r(n+1, i(n)), c = k(n+1). The intended argument is clear, so the result is not affected by this slip.
Second check: another model agreed
Report a problem with this finding
17 minor (typos and the like; most checked by the judge only)
Wording Introduction claims computability of "the real parts of the zeros of the Bessel functions", but §10 only states "From (vi) and (x) we deduce that the real zeros of the Bessel functions are computable."
- p. 1 Introduction, paragraph 2
the real parts of the zeros of the Bessel functions
- p. 28 §10, end of examples
we deduce that the real zeros of the Bessel functions are computable
Judge's note: Rests on outside knowledge: whether Bessel functions in general have non-real zeros. Viewed both crops. The introduction (p.1) points to §§9, 10 for the claim, and §10 (p.28) derives only the result for real zeros, using (vi), which is about roots of a continuous increasing function. The claim as worded in the introduction is broader than what §10 derives. For the usual orders the zeros are all real, so this is a scope mismatch in the wording.
Second check: another model agreed
Report a problem with this finding
Wording Intro: "it is almost equally easy to define and investigate computable functions of an integral variable or a real or computable variable"; §10: "We cannot define general computable functions of a real variable, since there is no general method of describing a real number".
- p. 1 Introduction, paragraph 1
it is almost equally easy to define and investigate computable functions of an integral variable or a real or computable variable
- p. 25 §10, definitions
We cannot define general computable functions of a real variable, since there is no general method of describing a real number
Judge's note: Viewed both crops. The introduction lists functions of 'a real or computable variable' as almost equally easy to define. §10 says general computable functions of a real variable cannot be defined and defines them only for a computable variable. The wording is in tension. It may be loose phrasing, so this is classed as an observation.
Second check: another model agreed
Report a problem with this finding
Wording Table for U row kmp: "cpe(e(kom, x, y), sim, x, y)" uses e with arguments (m-config, symbol, symbol), which matches neither defined form e(C, B, α) nor e(B, α).
- p. 15 Table for U, row kmp
cpe(e(kom, x, y), sim, x, y)
- p. 8 Definition of e
From e(C, B, α) the first α is erased and → C. If there is no α → B.
Judge's note: The p.8 image defines e(C, B, α), with B an m-configuration, and e(B, α). The p.15 image shows 'cpe(e(kom, x, y), sim, x, y)' with the gloss 'It erases all letters x and y.' The intended call appears to be e(e(kom, x), y).
Second check: another model agreed
Report a problem with this finding
Wording "We also give numbers to the symbols S1, ..., Sm and, in particular, blank = S0, 0 = S1, 1 = S2": the stated range S1…Sm excludes S0, which is then used for the blank.
- p. 10 §5, last line
We also give numbers to the symbols S1, ..., Sm
- p. 11 §5, first line
blank = S0, 0 = S1, 1 = S2.
Judge's note: Pages 10-11 images confirm the wording. 'In particular' presents S0 as one of the numbered symbols, but the range starts at S1. PS0 is used later on p.11. The evident fix is S0, ..., Sm.
Second check: another model agreed
Report a problem with this finding
Wording (C1) is printed "DA : DCCCDCCCDAADCDDC : ..." but (C2), said to be (C1) with figures inserted, is printed "DDA : 0 : 0 : DCCCDCCCDAADCDDC : DCCC...." with an extra leading D.
- p. 13 §6, display (C1)
DA:DCCCDCCCDAADCDDC:DCCCDCCCDAAADCDDC:... (C1)
- p. 13 §6, display (C2)
DDA:0:0:DCCCDCCCDAADCDDC:DCCC....
Only the authors can say what is right here.
Judge's note: Page 13 image confirms both displays. The text says 'Then (C1) becomes' (C2) by printing figures between successive configurations, so the first configuration should stay 'DA'. The extra 'D' is unexplained. The authors would need to confirm the intended form.
Second check: another model agreed
Report a problem with this finding
Wording "The machine U is to be capable of printing "A", "C", "D", "0", "1", "u", "v", "w", "x", "y", "z"" omits ":", which U's table prints (b1 "P:", mk5 "P:", pe2(inst, 0, :)).
- p. 14 §7, end
The machine U is to be capable of printing "A", "C", "D", "0", "1", "u", "v", "w", "x", "y", "z".
- p. 15 Table for U, b1
R, R, P:, R, R, PD, R, R, PA
- p. 16 Table for U, mk5
P:
Judge's note: Page 14 image shows the list. Page 15 image shows b1 'R, R, P:, R, R, PD, R, R, PA'. Page 16 image shows mk5 'None P:' and sh4/sh5 pe2(inst, 0, :) and pe2(inst, 1, :). The colon is printed but not listed.
Second check: another model agreed
Report a problem with this finding
Wording Proof of (ii), p. 257: the axiom 𝔄_η uses a two-place predicate G ("(F(x, y)→G(x, y)) & (G(x, y) & G(y, z)→G(x, z))") that is never defined, although H and K are defined just before it.
- p. 28 Proof of (ii), axiom 𝔄_η
(F(x, y)→G(x, y)) & (G(x, y) & G(y, z)→G(x, z))
Only the authors can say what is right here.
Judge's note: I read page 28 (p. 257). H(x, y) and K(x, y, z) are defined explicitly. G(x, y) appears in 𝔄_η and again in the formulae at the foot of p. 257 and on p. 258, but no meaning is given. A search of the text found G only as G(n) in §8, G_α(x) in §9 and G(α) in (v), none of them two-place. The axioms suggest an ordering is meant, so a reader can probably infer it; this is an ambiguity rather than an error.
Second check: another model agreed
Report a problem with this finding
Typo Description of re(C, B, α, β) reads "replaces the first α by β and → C → B if there is no α"; a separator is missing ("→ C; → B if there is no α").
- p. 9 Description of re(C, B, α, β)
β and → C → B if there is no α.
Judge's note: Page 9 image: the two arrow clauses run together with no punctuation between them. The parallel description of e on p.8 reads '→ C. If there is no α → B.'
Second check: none (judge only)
Report a problem with this finding
Typo In §8 the instruction "calculate the first R(K) figures computed by H and write down the R(K)-th" sets the machine as a plain italic H, whereas elsewhere it is the script letter.
- p. 18 §8, verdict 's' paragraph
calculate the first R(K) figures computed by H and write down the R(K)-th
Judge's note: In the crop of p.18 the surrounding mentions of the machine use the script glyph, but this one is a plain italic H. The difference is typographic only.
Second check: none (judge only)
Report a problem with this finding
Typo "The differences from our point of view between the single and compound symbols is that ...": the plural subject takes a singular verb.
- p. 21 §9 I, first paragraph
differences from our point of view between the single and compound symbols is that
Judge's note: The crop of p.21 confirms the published wording 'differences ... is'.
Second check: none (judge only)
Report a problem with this finding
Typo Proof of (ii): "if M′ ≥ M and M′ ≥ m and m ≠ η(u), then" should read η(n); the next formula uses u^(η(n)).
- p. 28 Proof of (ii), last lines
and m ≠ η(u), then
Judge's note: Page 28 image: the condition is printed 'm ≠ η(u)', and the formula that follows is G(u^(η(n)), u^(m)) ∨ G(u^(m), u^(η(n))). Here u is the individual symbol, not the integer n under discussion, so η(n) is evidently intended. The stated result is not affected.
Second check: none (judge only)
Report a problem with this finding
Typo §11, p. 259: "R_{S_l}(x, y) is to be interpreted as 'in the complete configuration x (of M) the symbol on the square y is S'". The subscript l is missing from the final S; it should be S_l.
- p. 30 §11, interpretation of R_Sl
the symbol on the square y is S".
Judge's note: On page 30 the predicate is printed R_{S_l} but the gloss ends with a plain "S" and no subscript. This is a typographic slip.
Second check: none (judge only)
Report a problem with this finding
Typo Definition of CC_n, p. 261: "& (y)F((y, u') v F(u, y) v F(u', y) v ... v F(u^(n−1), y) v R_{S_0}(u^(n), y))". The F stands outside the parenthesis, so the formula is not well-formed.
- p. 32 Lemma 1, proposition CC_n
& (y)F((y, u') v F(u, y) v F(u', y) v ... v F(u^(n−1), y) v R_S0(u^(n), y))
- p. 32 Proof of Lemma 1, definition of CC_n
(y)F((y, u') v F(u, y) v F(u', y) v ... v F(u^(n-1), y) v R_S0(u^(n), y))
Judge's note: Page 32 shows "(y)F((y, u') v F(u, y) v ...", which applies the binary predicate F to a disjunction. The intent is evidently the quantified disjunction (y)(F(y, u') v F(u, y) v ...). This is not an extraction artefact.
Second check: none (judge only)
Report a problem with this finding
Typo Proof of Lemma 1, p. 262: "A(M) & F^(N) → CC^N" has a superscript N where the subscript CC_N is meant.
- p. 33 Lemma 1 proof
A(M) & F^(N) → CC^N.
Judge's note: Page 33 prints a raised N in CC^N. The line directly above prints CC_N with a subscript, as does the rest of the proof.
Second check: none (judge only)
Report a problem with this finding
Typo Appendix, p. 263: "according as the n-th figure of λ is 1 or 0". The sequence under discussion is γ, so this should read "the n-th figure of γ".
- p. 34 Appendix, definition of λ-definable sequence
the n-th figure of λ is 1 or 0.
- p. 34 Appendix, definition of λ-definability
according as the n-th figure of λ is 1 or 0
Judge's note: Page 34 prints λ. The surrounding definition concerns the sequence γ with n-th figure φ_γ(n), and λ is the abstraction operator.
Second check: none (judge only)
Report a problem with this finding
Typo Appendix, p. 263: "calculable if 1+φ_γ(u) is a λ-definable function of n". The argument should be n, not u.
- p. 34 Appendix, definition
calculable if 1+φγ(u) is a λ-definable function of n
Judge's note: Page 34 prints φ_γ(u). The sentence says "function of n", and the display that follows uses N_{φ_γ(n)+1}.
Second check: none (judge only)
Report a problem with this finding
Typo Appendix, p. 264: the formula is introduced as "Let U stand for" but is used immediately afterwards as "{U_γ}(N_n) conv N_ξ(n)".
- p. 35 Appendix, second proof
Let U stand for
- p. 35 Appendix, next line
{U_γ}(N_n) conv N_ξ(n).
- p. 35 Appendix, following display
{Uγ}(Nn) conv N_ξ(n)
Judge's note: Page 35 prints a plain U in the definition and U_γ in the display directly below it. This does not follow the γ-subscript convention used for A_γ and M_γ.
Second check: none (judge only)