---
slug: godel-incompleteness
passed: 2026-10-14
by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex and a Claude agent
checked: 187
confirmed: 149
wrong: 32
unverifiable: 0
stale: 6
---

This was the directed repair pass for queue-1014c, read at f5e5f84f34. I re-read the evidence for all 39 triage items, checked the authored page and scripts, reproduced the reported Goodstein behavior, and applied only supported layer-local fixes. The record gives each triage item its own claim and disposition, then retains 148 distinct CONFIRMED claims from the supplied Codex and Claude checker records; those retained source reviews are attributed to their checkers, not claimed as new independent reviews. Triage supersedes conflicting earlier verdicts. The 13 MINOR entries count in wrong and receive no page correction lines. The 6 STALE entries share one Updated line; seven distinct WRONG defects have Corrected lines mirrored in markdown. K8 is rejected with evidence and remains unchanged. Full before/after edits, sources, dated lines and command results are in research/assay-line/queue-1014c/godel-incompleteness/fix-report.md.

## Claims

- MINOR | X1 (code-table-visibility): “The code table is a convention” / “any one-to-one assignment works, and the exact number you get depends on the table chosen (ours is shown by the buttons; the method is Gödel's own prime-power coding1).” | public/strata/godel-incompleteness/index.html | renderPalette prints glyphs only; update prints each chosen code as its prime exponent. The numerical table was not on the buttons.
- MINOR | X2 (conditions-demo-coverage): “The theorem needs all three conditions, and you can watch each one matter.” | public/strata/godel-incompleteness/index.html; https://plato.stanford.edu/entries/goedel-incompleteness/ | The four COND cases are pa, pres, rcf and incons. They illustrate arithmetic strength and consistency; none drops effective axiomatization.
- WRONG | X3 (gentzen-ordinal-date): “Gentzen showed in 1936 that ε₀ is the exact proof-theoretic ordinal of PA: it can prove transfinite induction up to any ordinal below ε₀, and that final rung is the one it can never climb.” | https://www.math.lmu.de/~schwicht/lectures/proofth/ss13/pt.pdf#page=7; https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=21 | Schwichtenberg, printed p. 4, section 1.2, attributes the initial induction segments and their optimality to Gentzen (1943). Sladek lists separate 1936 and 1943 papers.
- WRONG | X4 (goodstein-four-step-count): “For 4 it really does reach 0” / “after” / `3·2<sup>402653211</sup>&nbsp;−&nbsp;2` / “steps” | https://oeis.org/A056041; https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=5 | OEIS gives 3*2^402653211 - 3 transitions. Sladek Definition 8 counts k + 1, with k the first zero index, so his value ending in -2 counts terms.
- WRONG | X5 (goodstein-start-controls): “for 1, 2, 3 you can watch the whole fall above.” | public/strata/godel-incompleteness/index.html; verify-godel-incompleteness.mjs | Only starts 3, 4 and 16 exist. Reproduced start 3 reaching zero in five transitions; starts 1 and 2 have no controls.
- WRONG | X6 (consistency-implies-soundness): “If anything they show how robust the system is: it can't even prove a falsehood about itself.” | https://dspace.library.uu.nl/bitstream/handle/1874/26521/Preprint_no_64.pdf?sequence=1; https://plato.stanford.edu/entries/goedel-incompleteness/ | Visser, printed p. 1 (PDF page 4), explicitly allows a consistent theory proving its own inconsistency. Consistency excludes a statement together with its negation, not all false theorems.
- MINOR | X7 (physical-theory-exclusion): “Presburger arithmetic and real closed fields are complete and decidable; physical theories aren't formal systems in the required sense.” | https://ctp.itp.ac.cn/EN/Y2016/V66/I01/19; https://plato.stanford.edu/entries/goedel-incompleteness/ | Luo et al. present the first-order axiomatization SpecRel+. A physical interpretation alone neither establishes nor defeats the arithmetic and effectiveness hypotheses.
- MINOR | X8 (paris-harrington-priority): “Paris, J. & Harrington, L. (1977). “A mathematical incompleteness in Peano arithmetic” (in the Handbook of Mathematical Logic)” / “the first natural arithmetical statement shown independent of PA. Gentzen, G. (1936/1943)” / “the consistency of PA by transfinite induction up to ε₀, the proof-theoretic ordinal of PA.” | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf#page=2; https://plato.stanford.edu/entries/goedel-incompleteness/ | Read OCR of printed pp. 1133-1134: the editor mentions several early-1977 examples and the authors credit earlier examples to Paris. SEP section 4.5 also discusses Gentzen before Paris-Harrington.
- MINOR | X9 (paris-harrington-priority): “the first natural arithmetical statement shown independent of PA.” | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf#page=2; https://plato.stanford.edu/entries/goedel-incompleteness/ | Read OCR of printed pp. 1133-1134: the editor mentions several early-1977 examples and the authors credit earlier examples to Paris. SEP section 4.5 also discusses Gentzen before Paris-Harrington.
- MINOR | X10 (encoding-interface-scope): “a live Gödel-numbering machine that turns any formula into a single integer and decodes it back” | public/strata/godel-incompleteness/index.html | MAXLEN is 12 and the palette contains 15 symbols; the append handler enforces that cap. The mathematical encoding is broader than this interface.
- STALE | X11 (misuse-count-six): “the six famous misuses corrected against Gödel 1931 and Franzén 2005” | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- WRONG | X12 (goodstein-instance-unprovability): “a real, runnable Goodstein machine: an ordinary number that explodes past 10^150 and then crashes to zero, true and watchable, that Peano arithmetic provably cannot prove (its shadow ordinal descends while the integer skyrockets; that descent is the proof PA can't make).” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- STALE | X13 (misuse-count-six): “corrects the six most common misuses against the primary and standard secondary sources.” | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- WRONG | X14 (ordinal-coefficient-order): “▼ strictly smaller than the previous ordinal” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=10; public/strata/godel-incompleteness/index.html; research/godel-incompleteness/goodstein.mjs | Definition 19 puts finite coefficients on the right. Reproduced coefficient-first outputs at start-4 steps 3 and 4; under ordinal multiplication those expressions increase. The underlying tree comparison already decreases.
- WRONG | X15 (goodstein-pause-reason): “Paused: the value is now exact but very long to print.” | public/strata/godel-incompleteness/index.html; verify-godel-incompleteness.mjs | Reproduced start 4 stopping at step 40001, base 40003, value 1600769196: ten digits, so only the step guard triggered. Start 16 instead triggers the digit guard.
- WRONG | X16 (goodstein-start-controls): “For 1, 2, 3 you can watch the whole fall.” | public/strata/godel-incompleteness/index.html; verify-godel-incompleteness.mjs | Only starts 3, 4 and 16 exist. Reproduced start 3 reaching zero in five transitions; starts 1 and 2 have no controls.
- MINOR | X17 (paris-harrington-priority): “the first natural arithmetical statement shown independent of PA.” | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf#page=2; https://plato.stanford.edu/entries/goedel-incompleteness/ | Read OCR of printed pp. 1133-1134: the editor mentions several early-1977 examples and the authors credit earlier examples to Paris. SEP section 4.5 also discusses Gentzen before Paris-Harrington.
- WRONG | X18 (goodstein-instance-unprovability): “that Peano arithmetic provably cannot prove” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- WRONG | X19 (ordinal-coefficient-order): (added) “2·ω<sup>2</sup> + 2·ω” followed by “2·ω<sup>2</sup> + ω + 5”, with “▼ strictly smaller than the previous ordinal”. | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=10; public/strata/godel-incompleteness/index.html; research/godel-incompleteness/goodstein.mjs | Definition 19 puts finite coefficients on the right. Reproduced coefficient-first outputs at start-4 steps 3 and 4; under ordinal multiplication those expressions increase. The underlying tree comparison already decreases.
- MINOR | K1 (quine-description-roles): [b8-2] It carries a description of its own body as data (the string s), and then it uses that description twice: once as text to print, once as code to run. | public/strata/godel-incompleteness/index.html; research/godel-incompleteness/quine.js | The actual expression prints JSON.stringify(s) and s. It emits quoted data and the program body; it does not evaluate s during that run.
- MINOR | K2 (diagonal-lemma-credit): [diagonal-lemma] His diagonal lemma proves that for any property P expressible in arithmetic (a formula with one free variable, of any complexity), there is a sentence G for which the system itself proves that G holds exactly when G's own Gödel number has property P - so G, in effect, ascribes property P to itself. | https://plato.stanford.edu/entries/goedel-incompleteness/ | SEP section 5 distinguishes the provability special case used by Gödel from the general lemma attributed to Carnap in 1934. The mathematical lemma itself is correct.
- MINOR | K3 (conditions-demo-coverage): [b14-2] The theorem needs all three conditions, and you can watch each one matter. | public/strata/godel-incompleteness/index.html; https://plato.stanford.edu/entries/goedel-incompleteness/ | The four COND cases are pa, pres, rcf and incons. They illustrate arithmetic strength and consistency; none drops effective axiomatization.
- WRONG | K4 (gentzen-ordinal-date): [b21-3] Gentzen showed in 1936 that ε₀ is the exact proof-theoretic ordinal of PA: it can prove transfinite induction up to any ordinal below ε₀, and that final rung is the one it can never climb. | https://www.math.lmu.de/~schwicht/lectures/proofth/ss13/pt.pdf#page=7; https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=21 | Schwichtenberg, printed p. 4, section 1.2, attributes the initial induction segments and their optimality to Gentzen (1943). Sladek lists separate 1936 and 1943 papers.
- WRONG | K5 (goodstein-four-step-count): [four-step-count] For 4 it really does reach 0 - after 3·2402653211 − 2 steps | https://oeis.org/A056041; https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=5 | OEIS gives 3*2^402653211 - 3 transitions. Sladek Definition 8 counts k + 1, with k the first zero index, so his value ending in -2 counts terms.
- WRONG | K6 (goodstein-start-controls): [small-falls] for 1, 2, 3 you can watch the whole fall above. | public/strata/godel-incompleteness/index.html; verify-godel-incompleteness.mjs | Only starts 3, 4 and 16 exist. Reproduced start 3 reaching zero in five transitions; starts 1 and 2 have no controls.
- WRONG | K7 (consistency-implies-soundness): [card-1-4] If anything they show how robust the system is: it can't even prove a falsehood about itself. | https://dspace.library.uu.nl/bitstream/handle/1874/26521/Preprint_no_64.pdf?sequence=1; https://plato.stanford.edu/entries/goedel-incompleteness/ | Visser, printed p. 1 (PDF page 4), explicitly allows a consistent theory proving its own inconsistency. Consistency excludes a statement together with its negation, not all false theorems.
- CONFIRMED | K8 (anti-mechanist-debate-balance): [card-4-3] Genuinely open; honestly disputed both ways. | https://plato.stanford.edu/entries/goedel-incompleteness/#GodArgAgaMec; public/strata/godel-incompleteness/index.html | REJECTED: the whole card calls this a contested philosophical argument, states the consistency objection and does not claim an equal division of experts. SEP section 6.3 reports broad criticism, Searle partly defending Penrose, and replies by Lucas and Penrose. That supports dispute in both directions; it does not establish a false contextual claim.
- WRONG | K9 (goodstein-instance-unprovability): [card-7-3] You can run Goodstein's above and watch the shadow ordinal that PA can't follow. | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- MINOR | K10 (paris-harrington-priority): [ref-first-natural] the first natural arithmetical statement shown independent of PA. | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf#page=2; https://plato.stanford.edu/entries/goedel-incompleteness/ | Read OCR of printed pp. 1133-1134: the editor mentions several early-1977 examples and the authors credit earlier examples to Paris. SEP section 4.5 also discusses Gentzen before Paris-Harrington.
- MINOR | K11 (encoding-interface-scope): [meta-any-formula] a live Gödel-numbering machine that turns any formula into a single integer and decodes it back | public/strata/godel-incompleteness/index.html | MAXLEN is 12 and the palette contains 15 symbols; the append handler enforces that cap. The mathematical encoding is broader than this interface.
- STALE | K12 (misuse-count-six): [meta-six] the six famous misuses corrected against Gödel 1931 and Franzén 2005 | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- WRONG | K13 (goodstein-instance-unprovability): [meta-goodstein] a real, runnable Goodstein machine: an ordinary number that explodes past 10^150 and then crashes to zero, true and watchable, that Peano arithmetic provably cannot prove (its shadow ordinal descends while the integer skyrockets; that descent is the proof PA can't make). | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- STALE | K14 (misuse-count-six): [body-six-common] corrects the six most common misuses against the primary and standard secondary sources. | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- STALE | K15 (misuse-count-six): [most-common-misuses] the six most common misuses | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- WRONG | K16 (goodstein-start-controls): [runtime-small] For 1, 2, 3 you can watch the whole fall. | public/strata/godel-incompleteness/index.html; verify-godel-incompleteness.mjs | Only starts 3, 4 and 16 exist. Reproduced start 3 reaching zero in five transitions; starts 1 and 2 have no controls.
- MINOR | K17 (paris-harrington-priority): [ref-first-natural-history] the first natural arithmetical statement shown independent of PA. | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf#page=2; https://plato.stanford.edu/entries/goedel-incompleteness/ | Read OCR of printed pp. 1133-1134: the editor mentions several early-1977 examples and the authors credit earlier examples to Paris. SEP section 4.5 also discusses Gentzen before Paris-Harrington.
- WRONG | K18 (goodstein-instance-unprovability): [meta-beyond-pa] that Peano arithmetic provably cannot prove | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- STALE | K19 (misuse-count-six): (added) page head: meta description "read the precise statements and the six most common misuses corrected against Gödel 1931 and Franzén 2005" (index.html line 15), og:description "Six famous misuses corrected against the sources.", JSON-LD description "the six most common misuses" (line 38); verify.mjs also prints "the six misuse corrections" | git show 772024e65d4^:public/strata/godel-incompleteness/index.html; git show 772024e65d4:public/strata/godel-incompleteness/index.html | Counted six wish cards in the parent and seven in 772024e65d4, dated 2026-06-26 UTC. The count was true before that change. No false frequency ranking is established by the absence of a ranking source.
- WRONG | K20 (goodstein-instance-unprovability): (added) page head: meta description "then run a Goodstein sequence: an ordinary number that explodes then crashes to zero, true but unprovable in Peano arithmetic" (line 15); og:description "a number that explodes then crashes to zero, true but unprovable in Peano arithmetic"; twitter:description "a Goodstein number that explodes then crashes to zero. True, but unprovable in Peano arithmetic." | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf#page=16; public/strata/godel-incompleteness/index.html | Sladek p. 16 distinguishes PA proofs for each fixed start from the unprovable universal theorem. Reproduced start 16 at 175 digits on step 7 and paused positive at 409 digits on step 11; start 3 finishes.
- CONFIRMED | “In 1931 Kurt Gödel built, inside arithmetic, a sentence that asserts its own unprovability” / “and showed it must be true and yet unreachable.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | intro-1931: The translated 1931 paper says "a theorem that states its own unprovability" and "is in fact unprovable (because it is undecidable)". Read with the consistency qualifications stated later on the page, this is supported. Retained from N2-codex.md, entry intro-1931; this is the checker's source review.
- CONFIRMED | “He is enlisted to prove that nothing can be known for certain, that mathematics is broken, that truth is whatever you want it to be, that the mind beats every computer, even that God exists.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | popular-invocations: Franzén p. 2 gives "nothing can be known for sure" and "the human mind can do things that computers can not." These are examples of misuse, not conclusions of incompleteness. Retained from N2-codex.md, entry popular-invocations; this is the checker's source review.
- CONFIRMED | “He proved none of those.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | proved-none: Franzén p. 4: "The incompleteness theorem is a theorem about the consistency and completeness of formal systems." The page correctly distinguishes this technical result from unrestricted claims about knowledge or reality. Retained from N2-codex.md, entry proved-none; this is the checker's source review.
- CONFIRMED | “Give every symbol a number; then any string of symbols” / “any formula” / “gets a single number too, by a recipe that can be undone.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | b3-2: Gödel, translated section 2.2: "one-to-one-correspondence" and "where pk is the kth prime (by magnitude)". The displayed prime-power recipe is invertible for the positive symbol codes used here. Retained from N2-codex.md, entry b3-2; this is the checker's source review.
- CONFIRMED | “Once formulas are numbers, a statement about formulas (“such-and-such is provable”) becomes a statement about numbers” / “the kind arithmetic can already make.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | b3-3: Gödel, translated section 2.2: "one-to-one-correspondence" and "where pk is the kth prime (by magnitude)". The displayed prime-power recipe is invertible for the positive symbol codes used here. Retained from N2-codex.md, entry b3-3; this is the checker's source review.
- CONFIRMED | “What matters is not the particular number but that the coding is injective and decodable: every formula gets exactly one number, and the number alone tells you the formula back.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | injective-decodable: Gödel, translated section 2.2: "one-to-one-correspondence" and "where pk is the kth prime (by magnitude)". The displayed prime-power recipe is invertible for the positive symbol codes used here. Retained from N2-codex.md, entry injective-decodable; this is the checker's source review.
- CONFIRMED | “it's the price of this coding, not of arithmetisation itself: the prime-power scheme buys clean, factor-it-back decodability at the cost of size (other one-to-one codes pack the same sentence far more compactly).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | compact-codings: SEP says "There are many possible ways of accomplishing this" and "the chosen mapping is effective". For example, a finite alphabet can be encoded positionally instead of by growing prime powers, so the size penalty is specific to this encoding. Retained from N2-codex.md, entry compact-codings; this is the checker's source review.
- CONFIRMED | “Numbering lets arithmetic mention formulas.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b6-1: SEP gives an "arbitrary formula" with "only one free variable" and a "(provable) material equivalence" with its self-application. Its historical paragraph attributes the general lemma to Carnap 1934; Gödel originally used the provability special case. The mathematical fixed-point claim is correct. Retained from N2-codex.md, entry b6-1; this is the checker's source review.
- CONFIRMED | “The second gear lets a formula mention itself.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b6-2: SEP gives an "arbitrary formula" with "only one free variable" and a "(provable) material equivalence" with its self-application. Its historical paragraph attributes the general lemma to Carnap 1934; Gödel originally used the provability special case. The mathematical fixed-point claim is correct. Retained from N2-codex.md, entry b6-2; this is the checker's source review.
- CONFIRMED | “That sounds like it should require magic or an infinite regress; it requires neither.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b6-3: SEP gives an "arbitrary formula" with "only one free variable" and a "(provable) material equivalence" with its self-application. Its historical paragraph attributes the general lemma to Carnap 1934; Gödel originally used the provability special case. The mathematical fixed-point claim is correct. Retained from N2-codex.md, entry b6-3; this is the checker's source review.
- CONFIRMED | “A quine is a program that takes no input and prints its own source code, exactly, with no cheating (it can't read its own file).” | https://www.keithschwarz.com/kleene/; https://arxiv.org/pdf/math/0305282 | quine-definition: Schwarz explains that the generated program will "produce its own source code" using Kleene's Second Recursion Theorem. Yanofsky section 4 additionally derives a "self-reproducing machine" by the recursion theorem; the pinned example has no file or input access. Retained from N2-codex.md, entry quine-definition; this is the checker's source review.
- CONFIRMED | “That double use is the entire move” / “and it is exactly the move Gödel makes.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | double-use-godel: SEP gives an "arbitrary formula" with "only one free variable" and a "(provable) material equivalence" with its self-application. Its historical paragraph attributes the general lemma to Carnap 1934; Gödel originally used the provability special case. The mathematical fixed-point claim is correct. Retained from N2-codex.md, entry double-use-godel; this is the checker's source review.
- CONFIRMED | “(This needs the system to represent its own substitution function, which any system with a little arithmetic does.)” | https://plato.stanford.edu/entries/goedel-incompleteness/sup2.html | substitution: SEP supplement: substitution "is purely mechanical" and "can be expressed in the language of arithmetic". This is the representability used in the diagonal construction. Retained from N2-codex.md, entry substitution; this is the checker's source review.
- CONFIRMED | “The quine and the Gödel sentence are not a loose metaphor for each other: they are two instances of one fixed-point phenomenon (Kleene's recursion theorem is the computability twin of the diagonal lemma5; both fall out of a single abstract diagonal argument10).” | https://tac.mta.ca/tac/reprints/articles/15/tr15.pdf; https://arxiv.org/pdf/math/0305282 | fixed-point-twins: Lawvere p. 3 offers a "fixed-point theorem in cartesian closed categories" for the arguments of "Cantor, Russell, Gödel and Tarski". The excerpt itself omits Kleene. Yanofsky section 4 supplies the recursion-theorem and self-reproducing-machine instances of the same construction. Retained from N2-codex.md, entry fixed-point-twins; this is the checker's source review.
- CONFIRMED | “Now point the diagonal lemma at one specific property: “…is not provable in this system.” Out comes a sentence G that says, in the pure language of numbers, “G is not provable here.” And the trap springs shut:” | https://plato.stanford.edu/entries/goedel-incompleteness/ | g-sentence: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry g-sentence; this is the checker's source review.
- CONFIRMED | “If the system could prove G, then there would be a proof” / “so the system also proves the arithmetical statement “G is provable.” But G itself says the opposite: “G is not provable.” The system would then prove both a statement and its negation” / “it would be inconsistent.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b10-1: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry b10-1; this is the checker's source review.
- CONFIRMED | “So a consistent system cannot prove G.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b10-2: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry b10-2; this is the checker's source review.
- CONFIRMED | “But that is exactly what G claims, so what G says is the case: G is true” / “and unprovable in the system.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b10-3: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry b10-3; this is the checker's source review.
- CONFIRMED | “Truth has outrun proof, with nothing up anyone's sleeve.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b10-4: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry b10-4; this is the checker's source review.
- CONFIRMED | “Any consistent, effectively axiomatised formal system strong enough to interpret a modest amount of arithmetic contains a sentence that is true (of the natural numbers) but neither provable nor refutable within the system.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | first-theorem: SEP states incompleteness for a "consistent formal system" with arithmetic and gives "Rosser’s modification of the first theorem (Rosser 1936)". Adding one independent sentence preserves consistency and effective axiomatization, so the theorem applies again; it does not exclude non-effective complete true arithmetic. Retained from N2-codex.md, entry first-theorem; this is the checker's source review.
- CONFIRMED | “You can add it as a new axiom” / “and the bigger system has its own new unprovable truth.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | new-axiom: SEP states incompleteness for a "consistent formal system" with arithmetic and gives "Rosser’s modification of the first theorem (Rosser 1936)". Adding one independent sentence preserves consistency and effective axiomatization, so the theorem applies again; it does not exclude non-effective complete true arithmetic. Retained from N2-codex.md, entry new-axiom; this is the checker's source review.
- CONFIRMED | “The holes can't all be filled at once.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | cannot-fill: SEP states incompleteness for a "consistent formal system" with arithmetic and gives "Rosser’s modification of the first theorem (Rosser 1936)". Adding one independent sentence preserves consistency and effective axiomatization, so the theorem applies again; it does not exclude non-effective complete true arithmetic. Retained from N2-codex.md, entry cannot-fill; this is the checker's source review.
- CONFIRMED | “(Gödel 19311; Rosser 19363) Any consistent, effectively axiomatised formal system strong enough to interpret a modest amount of arithmetic contains a sentence that is true (of the natural numbers) but neither provable nor refutable within the system. You can add it as a new axiom” / “and the bigger system has its own new unprovable truth. The holes can't all be filled at once. (Gödel 1931 proved this assuming ω-consistency; Rosser 1936 weakened the hypothesis to plain consistency.)” | https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/extensions-of-some-theorems-of-godel-and-church/0461E34DC1F219C459EE84CC2FA89068 | rosser-strengthening: Rosser's own abstract says "simple consistency implies the existence of undecidable propositions" and calls it "a strengthening of Gödel’s Satz VI". The journal metadata give September 1936, volume 1, pp. 87-91. Retained from N2-codex.md, entry rosser-strengthening; this is the checker's source review.
- CONFIRMED | “No such system can prove a statement expressing its own consistency” / “written the standard way9” / “unless it is in fact inconsistent (in which case it proves everything).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b13-1: SEP states that consistency "cannot be proved in F itself" and warns that "not just any, merely extensionally adequate provability predicate works". The page includes the standard-predicate qualification; read "modest amount" as sufficient arithmetic for the theorem being stated. Retained from N2-codex.md, entry b13-1; this is the checker's source review.
- CONFIRMED | “A consistent system cannot certify, from the inside, that it is trustworthy” / “not, at least, through the natural statement of its own consistency.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b13-2: SEP states that consistency "cannot be proved in F itself" and warns that "not just any, merely extensionally adequate provability predicate works". The page includes the standard-predicate qualification; read "modest amount" as sufficient arithmetic for the theorem being stated. Retained from N2-codex.md, entry b13-2; this is the checker's source review.
- CONFIRMED | ““Every formal system has unprovable truths” is false.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b14-1: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b14-1; this is the checker's source review.
- CONFIRMED | “Drop “strong enough for arithmetic” and complete, decidable systems appear” / “real ones, not toys:” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b14-3: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b14-3; this is the checker's source review.
- CONFIRMED | “Presburger arithmetic” / “the whole numbers with addition but no multiplication” / “is consistent, complete, and decidable: a machine can settle every statement (Presburger 19294).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b16-1: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b16-1; this is the checker's source review.
- CONFIRMED | “Tarski showed the same for the first-order theory of real closed fields, which contains all of high-school algebra and Euclidean geometry (Tarski 19516).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b16-2: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b16-2; this is the checker's source review.
- CONFIRMED | “Multiplication of integers is the spark that lets a system encode its own syntax” / “and so lights the fuse.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b16-3: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b16-3; this is the checker's source review.
- CONFIRMED | “Incompleteness is not a curse on all formal reasoning; it is the specific price of being rich enough to talk about yourself.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | b16-4: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry b16-4; this is the checker's source review.
- CONFIRMED | ““Granted” / “but Gödel's unprovable sentence is a contrived stunt. It only talks about its own provability. No real mathematics is ever actually out of reach.”” | https://plato.stanford.edu/entries/goedel-incompleteness/ | natural-objection: This is an imagined objection, introduced by "Here is the deepest objection of all". It is not attributed to SEP or a named speaker. SEP supports the underlying question about natural independent mathematics, not this wording as a quotation. The source record itself notes that it is imagined. Retained from N2-codex.md, entry natural-objection; this is the checker's source review.
- CONFIRMED | “For decades that was a fair worry.” | https://plato.stanford.edu/entries/goedel-incompleteness/; https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf | decades-worry: Read as the historical search for simple finitary mathematics rather than ordinal proof theory, this is supported by the Paris-Harrington editor's note: the search ran "Since 1931" until examples found "early in 1977". The separate absolute priority claim needs qualification. Retained from N2-codex.md, entry decades-worry; this is the checker's source review.
- CONFIRMED | Goodstein's universal termination theorem is true but unprovable in PA. | https://arxiv.org/pdf/1405.4484 | natural-statements: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry natural-statements; this is the checker's source review. The visible-run wording is corrected under X12; only the universal mathematical claim is retained here.
- CONFIRMED | “Take a number and write it in hereditary base 2” / “base 2 all the way down, every exponent (and every exponent's exponent) itself written in base 2.” | https://arxiv.org/pdf/1405.4484 | b18-2: Rathjen Definition 2.4 defines the hereditary base change followed by predecessor, and the special sequence with base i+2. It explicitly defines predecessor of zero as zero, so the process stops descending once zero is reached. Retained from N2-codex.md, entry b18-2; this is the checker's source review.
- CONFIRMED | “Now repeat one move forever: bump every base up by one, then subtract one.” | https://arxiv.org/pdf/1405.4484 | b18-3: Rathjen Definition 2.4 defines the hereditary base change followed by predecessor, and the special sequence with base i+2. It explicitly defines predecessor of zero as zero, so the process stops descending once zero is reached. Retained from N2-codex.md, entry b18-3; this is the checker's source review.
- CONFIRMED | “Turn the 2s into 3s, subtract 1, rewrite in base 3; turn the 3s into 4s, subtract 1; and on.” | https://arxiv.org/pdf/1405.4484 | b18-4: Rathjen Definition 2.4 defines the hereditary base change followed by predecessor, and the special sequence with base i+2. It explicitly defines predecessor of zero as zero, so the process stops descending once zero is reached. Retained from N2-codex.md, entry b18-4; this is the checker's source review.
- CONFIRMED | “The value can rocket past anything you can picture” / “and Goodstein proved in 1944 that every such sequence, with no exceptions, eventually crashes to 0.” | https://arxiv.org/pdf/1405.4484 | goodstein-1944: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry goodstein-1944; this is the checker's source review.
- CONFIRMED | The intended shadow ordinal uses the hereditary tree read in base omega and decreases at each nonzero step. | https://arxiv.org/pdf/1405.4484 | b20-3: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry b20-3; this is the checker's source review. The displayed coefficient order is corrected under X14/X19.
- CONFIRMED | “And there is no infinite descending staircase of ordinals” / “any strictly decreasing sequence of them must hit the floor.” | https://arxiv.org/pdf/1405.4484 | b20-4: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry b20-4; this is the checker's source review.
- CONFIRMED | “So however high the integer flies, its shadow is running out of room; when the shadow reaches 0, the number has too.” | https://arxiv.org/pdf/1405.4484 | b20-5: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry b20-5; this is the checker's source review.
- CONFIRMED | “That descent is the proof.” | https://arxiv.org/pdf/1405.4484 | b20-6: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry b20-6; this is the checker's source review.
- CONFIRMED | The ordinal descent proof for all starting values at once cannot be carried out in PA. | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf | b21-1: Sladek p. 16 distinguishes induction below epsilon zero from the full principle. Schwichtenberg p. 4 gives the precise statement and attributes these optimality results to Gentzen 1943. The source record's excerpt says "not formalizable" where the correct distinction is not provable. Retained from N2-codex.md, entry b21-1; this is the checker's source review. The scope is now explicit under X12.
- CONFIRMED | “The descent ranges over the ordinals below ε₀” / “the smallest ordinal PA cannot see all the way to the end of.” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf | b21-2: Sladek p. 16 distinguishes induction below epsilon zero from the full principle. Schwichtenberg p. 4 gives the precise statement and attributes these optimality results to Gentzen 1943. The source record's excerpt says "not formalizable" where the correct distinction is not provable. Retained from N2-codex.md, entry b21-2; this is the checker's source review.
- CONFIRMED | “So Kirby and Paris could prove, in 1982, that Goodstein's theorem is unprovable in PA” / “true, runnable, utterly ordinary, and beyond the system.” | https://arxiv.org/pdf/1405.4484 | kirby-paris-1982: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry kirby-paris-1982; this is the checker's source review.
- CONFIRMED | “itself a number with over 120 million digits” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf | four-digit-count: Sladek p. 5 gives G(4) with exponent 402653211. Independently, floor(log10(3)+402653211*log10(2))+1 = 121210695 digits. The difference of one between the conventions does not affect this digit count. Retained from N2-codex.md, entry four-digit-count; this is the checker's source review.
- CONFIRMED | “Gödel proved mathematics is inconsistent / broken” / “that arithmetic might secretly contradict itself.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | slogan-1: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-1; this is the checker's source review.
- CONFIRMED | “Gödel proved nothing can ever really be proven” / “certainty is an illusion.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | slogan-2: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-2; this is the checker's source review.
- CONFIRMED | “Gödel proved truth is subjective / relative” / “there are no objective facts.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | slogan-3: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-3; this is the checker's source review.
- CONFIRMED | “Gödel proved the human mind is not a machine” / “that we surpass any computer.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | slogan-4: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-4; this is the checker's source review.
- CONFIRMED | “Gödel proved that God exists.” | https://christoph-benzmueller.de/papers/GoedelOntologicalArgument.html | slogan-5: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-5; this is the checker's source review.
- CONFIRMED | “Gödel's theorem applies to everything” / “every system, all of science, any self-reference.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | slogan-6: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-6; this is the checker's source review.
- CONFIRMED | “Gödel's unprovable sentences are contrived self-referential tricks” / “no real, ordinary mathematics is ever actually unprovable.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | slogan-7: This is a rejected slogan under "what people wish", not an attributed verbatim quotation and not a proposition the page endorses. The adjacent correction and the cited source discuss its misuse. The record's own note calls it an "Anonymous slogan"; kind "quote" makes the offline checker demand an attribution that the page does not make. Retained from N2-codex.md, entry slogan-7; this is the checker's source review.
- CONFIRMED | “Incompleteness is not inconsistency.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-1-2: SEP defines consistency as excluding a sentence and its negation together, and says an inconsistent system has "every statement" derivable. This confirms explosion and incompleteness versus inconsistency, but does not imply soundness. Retained from N2-codex.md, entry card-1-2; this is the checker's source review.
- CONFIRMED | “The theorems assume consistency and derive a true-but-unprovable sentence from it; no contradiction in arithmetic is produced or known.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-1-3: SEP defines consistency as excluding a sentence and its negation together, and says an inconsistent system has "every statement" derivable. This confirms explosion and incompleteness versus inconsistency, but does not imply soundness. Retained from N2-codex.md, entry card-1-3; this is the checker's source review.
- CONFIRMED | “Endless things are provable; the theorem locates a specific limit of specific formal systems.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | card-2-2: Franzén p. 4: "The incompleteness theorem is a theorem about the consistency and completeness of formal systems." The page correctly distinguishes this technical result from unrestricted claims about knowledge or reality. Retained from N2-codex.md, entry card-2-2; this is the checker's source review.
- CONFIRMED | “The proof of incompleteness is itself a fully rigorous proof” / “self-undermining if the slogan were true.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | card-2-3: Franzén p. 4: "The incompleteness theorem is a theorem about the consistency and completeness of formal systems." The page correctly distinguishes this technical result from unrestricted claims about knowledge or reality. Retained from N2-codex.md, entry card-2-3; this is the checker's source review.
- CONFIRMED | “The theorem turns on a sharp, objective gap between arithmetical truth and formal provability, and shows truth exceeds proof.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-3-2: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry card-3-2; this is the checker's source review.
- CONFIRMED | “Gödel himself was a thoroughgoing mathematical realist.” | https://plato.stanford.edu/entries/goedel/ | card-3-3: The SEP Gödel entry says he "formulated and defended mathematical Platonism" and regarded "mathematical truth" as "objective". Retained from N2-codex.md, entry card-3-3; this is the checker's source review.
- CONFIRMED | “It is an anti-relativist result wearing a relativist disguise.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-3-4: This is the author's interpretation of the truth/provability distinction, not an additional theorem about relativism. SEP supports the mathematical distinction and Gödel's objective conception of mathematical truth. No separate empirical or historical assertion is inferred from the metaphor. Retained from N2-codex.md, entry card-3-4; this is the checker's source review.
- CONFIRMED | “A real argument (Lucas 1961, Penrose 1989)” / “but a contested philosophical one, not a theorem.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-4-1: SEP identifies Lucas 1961 and Penrose 1989, the consistency objection, and replies by the proponents. It says "there is wide consensus that they fail" about the particular Gödelian arguments. Whether human cognition is mechanistic is not settled by the incompleteness theorem. Retained from N2-codex.md, entry card-4-1; this is the checker's source review.
- CONFIRMED | “The standard objection: to “see” that G is true you must assume the system is consistent, and the Second theorem says you can't establish that from inside either.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-4-2: SEP identifies Lucas 1961 and Penrose 1989, the consistency objection, and replies by the proponents. It says "there is wide consensus that they fail" about the particular Gödelian arguments. Whether human cognition is mechanistic is not settled by the incompleteness theorem. Retained from N2-codex.md, entry card-4-2; this is the checker's source review.
- CONFIRMED | “A conflation of two unrelated things.” | https://christoph-benzmueller.de/papers/GoedelOntologicalArgument.html | card-5-1: Benzmüller's research page separately documents "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence". Adams' primary editorial note presents the ontological proof as a separate modal argument, not a consequence of the 1931 arithmetic theorems. Retained from N2-codex.md, entry card-5-1; this is the checker's source review.
- CONFIRMED | “Gödel did write a modal-logic ontological argument” / “but it is a separate piece of work with no connection to incompleteness, which is about formal systems and arithmetic.” | https://christoph-benzmueller.de/papers/GoedelOntologicalArgument.html | card-5-2: Benzmüller's research page separately documents "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence". Adams' primary editorial note presents the ontological proof as a separate modal argument, not a consequence of the 1931 arithmetic theorems. Retained from N2-codex.md, entry card-5-2; this is the checker's source review.
- CONFIRMED | “It needs an effectively axiomatised system rich enough to interpret arithmetic.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-6-2: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry card-6-2; this is the checker's source review.
- CONFIRMED | “Self-reference alone isn't enough” / “you need self-reference plus arithmetic.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-6-4: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry card-6-4; this is the checker's source review.
- CONFIRMED | “Goodstein's theorem (every Goodstein sequence reaches 0) and the Paris–Harrington principle are perfectly natural statements about whole numbers, with no self-reference and no mention of proof, that are true yet unprovable in Peano arithmetic” / “the second shown independent in 1977, the first in 1982.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-7-2: SEP section on concrete independent statements identifies Paris-Harrington 1977 and Goodstein 1944, with the latter proved unprovable in 1982. It also warns that the claim of no earlier natural independent statements is "not, however, strictly speaking, correct" because of Gentzen. Retained from N2-codex.md, entry card-7-2; this is the checker's source review.
- CONFIRMED | “Franzén 2005, ch. 2.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | card-citation-1: Franzén's actual contents list chapter 2 "The Incompleteness Theorem: An Overview", chapter 4 "Incompleteness Everywhere", chapter 5 "Skepticism and Confidence", chapter 6 "Gödel, Minds, and Computers", and chapter 8 "Incompleteness, Complexity, and Infinity". These verify the cited chapter locations and topics; substantive propositions are checked separately in this record. Retained from N2-codex.md, entry card-citation-1; this is the checker's source review.
- CONFIRMED | “Franzén 2005, ch. 1–2.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | card-citation-2: Franzén's actual contents list chapter 2 "The Incompleteness Theorem: An Overview", chapter 4 "Incompleteness Everywhere", chapter 5 "Skepticism and Confidence", chapter 6 "Gödel, Minds, and Computers", and chapter 8 "Incompleteness, Complexity, and Infinity". These verify the cited chapter locations and topics; substantive propositions are checked separately in this record. Retained from N2-codex.md, entry card-citation-2; this is the checker's source review.
- CONFIRMED | “Franzén 2005, ch. 4–5; Sokal & Bricmont 1998 catalogue the postmodern misreadings.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf; https://dokumen.pub/fashionable-nonsense-postmodern-intellectuals-abuse-of-science-english-edition-0312195451-9780312195458.html | card-citation-3: Franzén's contents support the chapter references. Sokal and Bricmont's actual chapter 11, opened separately, says "Godel’s theorem is an inexhaustible source of intellectual abuses". The record's contents excerpt alone does not support the Sokal/Bricmont half. Retained from N2-codex.md, entry card-citation-3; this is the checker's source review.
- CONFIRMED | “Franzén 2005, ch. 6; Lucas 1961; Penrose 1989; rebuttals by Putnam, Feferman.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf; https://plato.stanford.edu/entries/goedel-incompleteness/ | card-citation-4: Franzén chapter 6 is "Gödel, Minds, and Computers". SEP independently identifies Lucas 1961, Penrose 1989, Putnam 1960, and Feferman 1995; these names and dates are not established by the contents excerpt alone. Retained from N2-codex.md, entry card-citation-4; this is the checker's source review.
- CONFIRMED | “Gödel's ontological proof (written c. 1941; first published 1987 by J. H. Sobel; in his Collected Works Vol. III, 1995) ≠ the 1931 theorems.” | https://www.cambridge.org/core/books/abs/kurt-godel-and-the-foundations-of-mathematics/godels-ontological-proof-and-its-variants/977F358D517E281B342DD3E72074ACEB; https://people.math.ethz.ch/~halorenz/4students/Literatur/GoedelsOntologGottesbeweis.pdf | card-citation-5: Adams, Collected Works III, p. 388, says the earlier sheet is dated "ca. 1941" and the proof appeared as an "appendix to Sobel 1987". This supports the page. The record's Cambridge summary instead says "dated 1940" and "was the proof finally published" in 1995, so it is a misleading source for these dates. Retained from N2-codex.md, entry card-citation-5; this is the checker's source review.
- CONFIRMED | “Franzén 2005, ch. 2 & 8; Presburger 1929; Tarski 1951.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf; https://plato.stanford.edu/entries/goedel-incompleteness/ | card-citation-6: Franzén's contents establish chapters 2 and 8. Stansifer's translation verifies Presburger's 1929 presentation; SEP's bibliography verifies the Tarski 1951 edition. The contents excerpt alone establishes neither date. Retained from N2-codex.md, entry card-citation-6; this is the checker's source review.
- CONFIRMED | “Paris & Harrington 1977; Kirby & Paris 1982; Goodstein 1944.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | card-citation-7: SEP section on concrete independent statements identifies Paris-Harrington 1977 and Goodstein 1944, with the latter proved unprovable in 1982. It also warns that the claim of no earlier natural independent statements is "not, however, strictly speaking, correct" because of Gentzen. Retained from N2-codex.md, entry card-citation-7; this is the checker's source review.
- CONFIRMED | “Code table for the numbering is a convention; the method is Gödel's.” | git show 60ea23c371:public/strata/godel-incompleteness/index.html | b43-4: The source comment says "the SAME convention the page uses"; comparison with Gödel section 2.2 confirms the prime-power method. Only the assignment of small symbol codes is locally chosen. Retained from N2-codex.md, entry b43-4; this is the checker's source review.
- CONFIRMED | “Gödel, K. (1931). “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.” Monatshefte für Mathematik und Physik 38: 173–198. English trans. in van Heijenoort, From Frege to Gödel (1967), and Gödel, Collected Works Vol. I.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | reference-1: The SEP bibliography contains the 1931 title, volume 38, pp. 173-198, and "English translation in van Heijenoort 1967, 596–616, and in Gödel 1986, 144–195." Both automated NOT FOUND verdicts are false negatives: normalization and HTML decoding locate the complete excerpt. Retained from N2-codex.md, entry reference-1; this is the checker's source review.
- CONFIRMED | “Franzén, T. (2005). Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. A K Peters. (The standard reference on what the theorems do and don't say.)” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | reference-2: The preview's copyright/cataloguing pages identify Torkel Franzén, the full title, A K Peters, and 2005. The book explicitly addresses the theorem's uses and abuses. Retained from N2-codex.md, entry reference-2; this is the checker's source review.
- CONFIRMED | “Rosser, J. B. (1936). “Extensions of some theorems of Gödel and Church.” Journal of Symbolic Logic 1: 87–91. (Weakens the hypothesis from ω-consistency to consistency.)” | https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/extensions-of-some-theorems-of-godel-and-church/0461E34DC1F219C459EE84CC2FA89068 | reference-3: Cambridge gives Rosser, the title, "September 1936", "pp. 87 - 91", and the abstract's strengthening from omega-consistency to simple consistency. Retained from N2-codex.md, entry reference-3; this is the checker's source review.
- CONFIRMED | “Presburger, M. (1929). “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.” Comptes-rendus du I Congrès des Mathématiciens des Pays Slaves, Warsaw (proceedings 1930), pp. 92–101. (Addition-only arithmetic is consistent, complete, and decidable.)” | https://cs.fit.edu/~ryan/papers/presburger.pdf | reference-4: Stansifer's translation introduction says the article was presented in Warsaw in 1929 and published in 1930, with "pages 92 through 101". It gives the same German title and explains the constructive decision procedure. Retained from N2-codex.md, entry reference-4; this is the checker's source review.
- CONFIRMED | “Kleene, S. C. (1938). The recursion (fixed-point) theorem” / “the computability-theory twin of the diagonal lemma; guarantees self-referential programs (quines) exist.” | https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/on-notation-for-ordinal-numbers/8E7DD0884850CD48531D480762321541; https://arxiv.org/pdf/math/0305282 | reference-5: Cambridge identifies S. C. Kleene, "On notation for ordinal numbers", December 1938, pp. 150-155. The title/date excerpt alone does not identify its recursion lemma; the Stanford CS103 history explicitly says that this paper included Kleene's Second Recursion Theorem. Retained from N2-codex.md, entry reference-5; this is the checker's source review.
- CONFIRMED | “Tarski, A. (1951). A Decision Method for Elementary Algebra and Geometry. (The first-order theory of real closed fields is complete and decidable.)” | https://plato.stanford.edu/entries/goedel-incompleteness/ | reference-6: SEP bibliography: "A Decision Method for Elementary Algebra and Geometry" was issued in 1948 and "2nd ed." in 1951. The page's 1951 reference is a real edition, not a mistaken discovery year. Retained from N2-codex.md, entry reference-6; this is the checker's source review.
- CONFIRMED | “Sokal, A. & Bricmont, J. (1998). Fashionable Nonsense. (Catalogues misuses of Gödel in postmodern writing.)” | https://dokumen.pub/fashionable-nonsense-postmodern-intellectuals-abuse-of-science-english-edition-0312195451-9780312195458.html | reference-7: The book's copyright page gives Sokal, Bricmont, Fashionable Nonsense, 1998; chapter 11 says "Godel’s theorem is an inexhaustible source of intellectual abuses" and discusses extrapolations to social and political matters. Retained from N2-codex.md, entry reference-7; this is the checker's source review.
- CONFIRMED | “Lucas, J. R. (1961), “Minds, Machines and Gödel”; Penrose, R. (1989), The Emperor's New Mind” / “the contested mind argument; rebutted by Putnam, Feferman, and others.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | reference-8: SEP bibliography identifies Lucas' 1961 article and Penrose's 1989 book. The discussion explicitly cites Putnam 1960 and Feferman 1995 as critics. Retained from N2-codex.md, entry reference-8; this is the checker's source review.
- CONFIRMED | “Feferman, S. (1960). “Arithmetization of metamathematics in a general setting.” Fundamenta Mathematicae 49: 35–92. (The Second theorem is intensional: it concerns the consistency statement built from a standard provability predicate” / “deviant arithmetisations of “this system is consistent” can behave differently.)” | https://pldml.icm.edu.pl/pldml/element/bwmeta1.element.bwnjournal-article-fmv49i1p35bwm; https://plato.stanford.edu/entries/goedel-incompleteness/ | reference-9: The journal catalogue identifies S. Feferman, "Arithmetization of metamathematics in a general setting", volume 49, pp. 35-92. SEP explains the intensional qualification and gives Feferman 1960. Retained from N2-codex.md, entry reference-9; this is the checker's source review.
- CONFIRMED | “Lawvere, F. W. (1969). “Diagonal arguments and cartesian closed categories.” (One abstract fixed-point theorem sitting under Gödel's diagonal lemma, Kleene's recursion theorem, Cantor's and Russell's arguments alike.)” | https://tac.mta.ca/tac/reprints/articles/15/tr15.pdf; https://arxiv.org/pdf/math/0305282 | reference-10: Lawvere's reprint gives the title, author and original publication "pages 134-145, 1969". Its fixed-point framework is real; Yanofsky section 4 supplies the Kleene application not mentioned in the supplied introduction excerpt. Retained from N2-codex.md, entry reference-10; this is the checker's source review.
- CONFIRMED | “Standard precise treatments used to check the statements above: P. Smith, An Introduction to Gödel's Theorems (2nd ed., 2013); the Stanford Encyclopedia of Philosophy, “Gödel's Incompleteness Theorems.”” | https://www.logicmatters.net/igt/ | reference-11: Smith's own site says the "second edition" appeared "in 2013". The committed log records checking precise treatments; SEP itself was read for the theorem statements. Retained from N2-codex.md, entry reference-11; this is the checker's source review.
- CONFIRMED | “Goodstein, R. L. (1944). “On the restricted ordinal theorem.” Journal of Symbolic Logic 9: 33–41. (Every Goodstein sequence terminates at 0” / “proved via descending ordinals.)” | https://fa.ewi.tudelft.nl/~hart/37/onderwijs/verzamelingenleer/materiaal/goodstein.pdf | reference-12: The original Goodstein paper's cover gives R. L. Goodstein, title, June 1944, volume 9, pp. 33-41. Its opening discusses a decreasing ordinal sequence terminating; Rathjen gives the modern explicit theorem and proof. Retained from N2-codex.md, entry reference-12; this is the checker's source review.
- CONFIRMED | “Kirby, L. & Paris, J. (1982). “Accessible independence results for Peano arithmetic.” Bulletin of the London Mathematical Society 14: 285–293. (Goodstein's theorem, and the hydra game, are unprovable in PA.)” | https://plato.stanford.edu/entries/goedel-incompleteness/ | reference-13: SEP bibliography gives Kirby and Paris, 1982, the cited title, volume 14, pp. 285-293. The Coq hydra monograph p. 83 independently attributes both termination and PA unprovability to their article. Retained from N2-codex.md, entry reference-13; this is the checker's source review.
- CONFIRMED | “English trans. in van Heijenoort, From Frege to Gödel (1967), and Gödel, Collected Works Vol. I.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | ref-godel-translations: The SEP bibliography contains the 1931 title, volume 38, pp. 173-198, and "English translation in van Heijenoort 1967, 596–616, and in Gödel 1986, 144–195." Both automated NOT FOUND verdicts are false negatives: normalization and HTML decoding locate the complete excerpt. Retained from N2-codex.md, entry ref-godel-translations; this is the checker's source review.
- CONFIRMED | “The standard reference on what the theorems do and don't say.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | ref-standard-guide: Franzén's introduction states the book's purpose: "the content, scope, and limits of the incompleteness theorem" and "counteract common misconceptions". Calling it a standard guide is consistent with its role in the authoritative SEP bibliography; it is not a measured ranking. Retained from N2-codex.md, entry ref-standard-guide; this is the checker's source review.
- CONFIRMED | “Kleene, S. C. (1938). The recursion (fixed-point) theorem” | https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/on-notation-for-ordinal-numbers/8E7DD0884850CD48531D480762321541; https://web.stanford.edu/class/archive/cs/cs103/cs103.1242/timeline_of_results | ref-kleene-date: Cambridge identifies S. C. Kleene, "On notation for ordinal numbers", December 1938, pp. 150-155. The title/date excerpt alone does not identify its recursion lemma; the Stanford CS103 history explicitly says that this paper included Kleene's Second Recursion Theorem. Retained from N2-codex.md, entry ref-kleene-date; this is the checker's source review.
- CONFIRMED | “guarantees self-referential programs (quines) exist.” | https://www.keithschwarz.com/kleene/ | ref-kleene-quines: Schwarz explains that the generated program will "produce its own source code" using Kleene's Second Recursion Theorem. Yanofsky section 4 additionally derives a "self-reproducing machine" by the recursion theorem; the pinned example has no file or input access. Retained from N2-codex.md, entry ref-kleene-quines; this is the checker's source review.
- CONFIRMED | “The Second theorem is intensional: it concerns the consistency statement built from a standard provability predicate” / “deviant arithmetisations of “this system is consistent” can behave differently.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | ref-feferman-intensional: SEP states that consistency "cannot be proved in F itself" and warns that "not just any, merely extensionally adequate provability predicate works". The page includes the standard-predicate qualification; read "modest amount" as sufficient arithmetic for the theorem being stated. Retained from N2-codex.md, entry ref-feferman-intensional; this is the checker's source review.
- CONFIRMED | “One abstract fixed-point theorem sitting under Gödel's diagonal lemma, Kleene's recursion theorem, Cantor's and Russell's arguments alike.” | https://tac.mta.ca/tac/reprints/articles/15/tr15.pdf; https://arxiv.org/pdf/math/0305282 | ref-lawvere-unification: Lawvere p. 3 offers a "fixed-point theorem in cartesian closed categories" for the arguments of "Cantor, Russell, Gödel and Tarski". The excerpt itself omits Kleene. Yanofsky section 4 supplies the recursion-theorem and self-reproducing-machine instances of the same construction. Retained from N2-codex.md, entry ref-lawvere-unification; this is the checker's source review.
- CONFIRMED | “Every Goodstein sequence terminates at 0” / “proved via descending ordinals.” | https://arxiv.org/pdf/1405.4484 | ref-goodstein-termination: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry ref-goodstein-termination; this is the checker's source review.
- CONFIRMED | “Goodstein's theorem, and the hydra game, are unprovable in PA.” | https://www.labri.fr/perso/casteran/CoqArt/le_teaser/teaser.pdf | ref-hydra: The Coq hydra monograph p. 83 says Kirby and Paris give "a proof that this termination is not provable in Peano arithmetic" for hydra battles as well as Goodstein sequences. Retained from N2-codex.md, entry ref-hydra; this is the checker's source review.
- CONFIRMED | “Gentzen, G. (1936/1943)” / “the consistency of PA by transfinite induction up to ε₀, the proof-theoretic ordinal of PA.” | https://plato.stanford.edu/entries/goedel-incompleteness/; https://www.math.lmu.de/~schwicht/lectures/proofth/ss13/pt.pdf | ref-gentzen-date: SEP connects Gentzen 1936 to PA consistency from induction up to epsilon zero. Schwichtenberg p. 4 states the optimality of initial induction segments and attributes it to 1943, confirming the two dates in the combined reference. Retained from N2-codex.md, entry ref-gentzen-date; this is the checker's source review.
- CONFIRMED | “Both are about what a formal system of symbols can and cannot reach.” | git show 60ea23c371:src/content/strata/two-symbols-are-enough.md | nearby-1: The linked pinned layer describes "a sorting network" and "the zero-one principle". The short nearby sentence compares limits and reach of formal mechanisms; it does not assert that the sorting network is a universal computer. Retained from N2-codex.md, entry nearby-1; this is the checker's source review.
- CONFIRMED | “Two arguments that look like they prove the impossible by an infinite regress.” | git show 60ea23c371:src/content/strata/zeno-paradox.md | nearby-2: The linked layer says "infinitely many stages need not add up to an infinite amount"; the present page explains why its fixed point requires no infinite regress. The relation is an interpretive comparison grounded in both texts. Retained from N2-codex.md, entry nearby-2; this is the checker's source review.
- CONFIRMED | “Two things a formal system lets you reach that feel like they should be forbidden.” | git show 60ea23c371:src/content/strata/banach-tarski.md | nearby-3: The linked Banach-Tarski layer describes "the Axiom of Choice" and a mathematical doubling; this page presents arithmetical incompleteness. The nearby sentence is an interpretive comparison of these constructions. Retained from N2-codex.md, entry nearby-3; this is the checker's source review.
- CONFIRMED | “Both turn undecidability into a precise limit on formal knowledge.” | git show 60ea23c371:src/content/strata/chaitin-omega.md | nearby-4: The linked Chaitin layer says a universal-machine Omega is "uncomputable" and discusses finite certificates. The current page concerns unprovable arithmetic statements. Both concern precise formal limitations; the relation does not identify the two theorems. Retained from N2-codex.md, entry nearby-4; this is the checker's source review.
- CONFIRMED | “Both turn syntax or machine state into exponents of primes, making arithmetic carry information you can decode.” | git show 60ea23c371:src/content/strata/fractran.md | nearby-5: The FRACTRAN layer explicitly uses "exponents of primes" for machine state. The current godel() engine encodes syntax in prime exponents. Both implementations support the comparison. Retained from N2-codex.md, entry nearby-5; this is the checker's source review.
- CONFIRMED | “Gödel did not prove that nothing can be proven, that mathematics is broken, or that truth is subjective.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | meta-no-collapse: Franzén p. 4: "The incompleteness theorem is a theorem about the consistency and completeness of formal systems." The page correctly distinguishes this technical result from unrestricted claims about knowledge or reality. Retained from N2-codex.md, entry meta-no-collapse; this is the checker's source review.
- CONFIRMED | “He built, inside arithmetic, a sentence that asserts its own unprovability, and showed it must be true and yet unreachable.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | meta-unreachable: The translated 1931 paper says "a theorem that states its own unprovability" and "is in fact unprovable (because it is undecidable)". Read with the consistency qualifications stated later on the page, this is supported. Retained from N2-codex.md, entry meta-unreachable; this is the checker's source review.
- CONFIRMED | “drop one and complete, decidable systems appear: Presburger arithmetic, real closed fields)” | https://plato.stanford.edu/entries/goedel-incompleteness/ | meta-drop-condition: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry meta-drop-condition; this is the checker's source review.
- CONFIRMED | “In 1931 Godel built, inside ordinary arithmetic, a sentence saying of itself that it cannot be proved, and showed it must be true yet unprovable.” | https://hirzels.com/martin/papers/canon00-goedel.pdf | plain-1931: The translated 1931 paper says "a theorem that states its own unprovability" and "is in fact unprovable (because it is undecidable)". Read with the consistency qualifications stated later on the page, this is supported. Retained from N2-codex.md, entry plain-1931; this is the checker's source review.
- CONFIRMED | “He is also misquoted: he did not show that nothing can be known for certain.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | plain-certainty: Franzén p. 2 gives "nothing can be known for sure" and "the human mind can do things that computers can not." These are examples of misuse, not conclusions of incompleteness. Retained from N2-codex.md, entry plain-certainty; this is the checker's source review.
- CONFIRMED | “Two symbols are enough to compute anything computable” | https://arxiv.org/pdf/1605.04343 | binary-universality: Yedidia and Aaronson section 8.1 describe compiling machines with larger alphabets to "a single tape, a 2-symbol alphabet". This confirms binary universality as a mathematical claim, although the nearby linked page now concerns sorting networks. Retained from N2-codex.md, entry binary-universality; this is the checker's source review.
- CONFIRMED | “the same arithmetical richness that lets a system encode its own syntax is what lets Gödel build a sentence about itself” / “the price of being expressive enough to talk about yourself is incompleteness.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | richness-price: SEP states incompleteness for a "consistent formal system" with arithmetic and gives "Rosser’s modification of the first theorem (Rosser 1936)". Adding one independent sentence preserves consistency and effective axiomatization, so the theorem applies again; it does not exclude non-effective complete true arithmetic. Retained from N2-codex.md, entry richness-price; this is the checker's source review.
- CONFIRMED | “Zeno's dissolves” / “the infinitely many stages sum to something finite.” | https://plato.stanford.edu/entries/paradox-zeno/ | zeno-series: SEP explains that "some infinite sums are after all finite" and that Zeno did not prove the infinite total. The linked layer further distinguishes the quantitative sum from the philosophical supertask issue; this note is about the finite geometric sum. Retained from N2-codex.md, entry zeno-series; this is the checker's source review.
- CONFIRMED | “Gödel's does not” / “the self-reference is real (a finite fixed point, not a true regress), and the sentence it builds is genuinely undecidable in the system: neither provable nor refutable there.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | self-reference-finite: SEP: "if F is consistent, then G_F is not provable in F" and the standard sentence "cannot be false, and must be true." The true-but-unprovable direction needs consistency, not soundness. The unrefutability direction needs the stronger Gödel hypothesis or Rosser's modification. Retained from N2-codex.md, entry self-reference-finite; this is the checker's source review.
- CONFIRMED | “Gödel's incompleteness theorems are about a *specific* limit of *specific* formal systems, not about the collapse of certainty, truth, or mathematics.” | https://api.pageplace.de/preview/DT0400.9781439876923_A40170168/preview-9781439876923_A40170168.pdf | body-specific-limit: Franzén p. 4: "The incompleteness theorem is a theorem about the consistency and completeness of formal systems." The page correctly distinguishes this technical result from unrestricted claims about knowledge or reality. Retained from N2-codex.md, entry body-specific-limit; this is the checker's source review.
- CONFIRMED | The examples illustrate why arithmetic strength and consistency matter; Presburger arithmetic and real closed fields are complete and decidable. | https://plato.stanford.edu/entries/goedel-incompleteness/; public/strata/godel-incompleteness/index.html | body-three-conditions: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry body-three-conditions; this is the checker's source review. The demonstration coverage is narrowed under X2/K3.
- CONFIRMED | “Has +, ×, and induction” / “rich enough to encode its own syntax.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-1-1: SEP identifies PA as first-order Peano arithmetic and lists its arithmetic language and induction. This is the standard effectively axiomatized system used throughout its incompleteness discussion. Retained from N2-codex.md, entry condition-1-1; this is the checker's source review.
- CONFIRMED | “Incomplete (and can’t prove its own consistency).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-1-2: SEP states that consistency "cannot be proved in F itself" and warns that "not just any, merely extensionally adequate provability predicate works". The page includes the standard-predicate qualification; read "modest amount" as sufficient arithmetic for the theorem being stated. Retained from N2-codex.md, entry condition-1-2; this is the checker's source review.
- CONFIRMED | “This is the home turf of the theorems.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-1-3: This is the page's description of its chosen example. PA meets the stated hypotheses; the source explicitly uses PA as the main arithmetical system. Retained from N2-codex.md, entry condition-1-3; this is the checker's source review.
- CONFIRMED | “Whole numbers with addition but no multiplication.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-2-1: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry condition-2-1; this is the checker's source review.
- CONFIRMED | “Consistent, complete, and decidable” / “a machine settles every statement (Presburger 1929).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-2-2: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry condition-2-2; this is the checker's source review.
- CONFIRMED | “Too weak to talk about itself, so the theorem doesn’t apply.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-2-3: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry condition-2-3; this is the checker's source review.
- CONFIRMED | “First-order theory of the reals” / “all of high-school algebra and Euclidean geometry.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-3-1: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry condition-3-1; this is the checker's source review.
- CONFIRMED | “Complete and decidable (Tarski 1951).” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-3-2: SEP calls addition-only arithmetic "complete (and decidable) (Presburger 1929)" and real closed fields "both complete and decidable". Its bibliography identifies the 1951 second edition of Tarski's decision method. The limitations concern arithmetic encoding, not merely having a multiplication symbol. Retained from N2-codex.md, entry condition-3-2; this is the checker's source review.
- CONFIRMED | “The reals can’t pin down the integers, so no self-encoding, so no incompleteness.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-3-3: Read in the explicitly selected language of real closed fields. The completeness and decidability result rules out interpreting the needed arithmetic there. It is not a claim that arbitrary expansions of the real field cannot define integers. Retained from N2-codex.md, entry condition-3-3; this is the checker's source review.
- CONFIRMED | “Proves everything, including its own consistency” / “so it is “complete” in the empty, useless sense.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-4-1: SEP defines consistency as excluding a sentence and its negation together, and says an inconsistent system has "every statement" derivable. This confirms explosion and incompleteness versus inconsistency, but does not imply soundness. Retained from N2-codex.md, entry condition-4-1; this is the checker's source review.
- CONFIRMED | “The theorems are about consistent systems; this is the degenerate case they exclude.” | https://plato.stanford.edu/entries/goedel-incompleteness/ | condition-4-2: SEP defines consistency as excluding a sentence and its negation together, and says an inconsistent system has "every statement" derivable. This confirms explosion and incompleteness versus inconsistency, but does not imply soundness. Retained from N2-codex.md, entry condition-4-2; this is the checker's source review.
- CONFIRMED | “It still must reach 0” | https://arxiv.org/pdf/1405.4484 | runtime-must-end: Rathjen p. 7: "Every Goodstein sequence terminates"; the proof uses "no infinitely descending ordinal sequences". The following paragraph attributes unprovability of the special, arithmetically expressible sequences to Kirby and Paris in 1982. This is the universal theorem, not failure of any particular computation. Retained from N2-codex.md, entry runtime-must-end; this is the checker's source review.
- CONFIRMED | “for 4 it reaches 0 only after a number of steps with over 120 million digits” | https://web.math.ucsb.edu/~agboola/teaching/2022/spring/8/notes/goodstein.pdf | runtime-four: Sladek p. 5 gives G(4) with exponent 402653211. Independently, floor(log10(3)+402653211*log10(2))+1 = 121210695 digits. The difference of one between the conventions does not affect this digit count. Retained from N2-codex.md, entry runtime-four; this is the checker's source review.
- CONFIRMED | “vastly more than the atoms in the observable universe” | https://www.norvig.com/atoms.html | runtime-atoms: Norvig estimates atoms at "10 to the 80th power". A step count with 121210695 decimal digits exceeds that estimate overwhelmingly. The parenthesis compares the step count, not the number 120 million itself. Retained from N2-codex.md, entry runtime-atoms; this is the checker's source review.
- CONFIRMED | “First incompleteness theorem (Gödel 19311; Rosser 19363)” | https://plato.stanford.edu/entries/goedel-incompleteness/ | godel-first-date: SEP states incompleteness for a "consistent formal system" with arithmetic and gives "Rosser’s modification of the first theorem (Rosser 1936)". Adding one independent sentence preserves consistency and effective axiomatization, so the theorem applies again; it does not exclude non-effective complete true arithmetic. Retained from N2-codex.md, entry godel-first-date; this is the checker's source review.
- CONFIRMED | “Second incompleteness theorem (Gödel 19311)” | https://plato.stanford.edu/entries/goedel-incompleteness/ | godel-second-date: SEP states that consistency "cannot be proved in F itself" and warns that "not just any, merely extensionally adequate provability predicate works". The page includes the standard-predicate qualification; read "modest amount" as sufficient arithmetic for the theorem being stated. Retained from N2-codex.md, entry godel-second-date; this is the checker's source review.
- CONFIRMED | “an ordinary number that explodes past 10^150 and then crashes to zero” | git show 60ea23c371:public/strata/godel-incompleteness/index.html; https://arxiv.org/pdf/1405.4484 | meta-growth-display: The mathematical sequence really grows above 10^150 at step 7, and the termination theorem implies eventual zero. The UI stops at step 11. This clause alone describes the mathematical sequence; the stronger watchability promise is charged to meta-goodstein rather than counted twice here. Retained from N2-codex.md, entry meta-growth-display; this is the checker's source review.
- CONFIRMED | “the second shown independent in 1977, the first in 1982.” | https://www.karlin.mff.cuni.cz/~krajicek/ph.pdf; https://arxiv.org/pdf/1405.4484 | paris-harrington-primary: The scanned primary chapter, OCRed only on pp. 1133-1134, is dated 1977 and says its combinatorial theorem "is not provable in Peano arithmetic." Rathjen supplies the other half of the sentence, Kirby-Paris 1982. Retained from N2-codex.md, entry paris-harrington-primary; this is the checker's source review.
- CONFIRMED | [prime-recipe] The recipe - k-th symbol rides the k-th prime | git show 60ea23c371:public/strata/godel-incompleteness/index.html | godel(): g *= BigInt(ps[i]) ** BigInt(CODE[syms[i]]), the k-th prime raised to the k-th symbol's code, as Gödel p. 179 "2^n1 . 3^n2 . ... . pk^nk". Retained from N2-claude.md, entry prime-recipe; this is the checker's source review.
- CONFIRMED | [decode-action] Hit decode and watch the factorisation hand the formula back, symbol for symbol. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | decode() factors by primes(64) and maps exponents back through SYM. Retained from N2-claude.md, entry decode-action; this is the checker's source review.
- CONFIRMED | [run-quine] Run this one and compare the output to the source, character for character. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | runQuine compares printed === quineSrc. Retained from N2-claude.md, entry run-quine; this is the checker's source review.
- CONFIRMED | [b8-1] The program never looks at itself from the outside. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | quine has no file access; verify.mjs also prints "ok quine source contains no file/read access". Retained from N2-claude.md, entry b8-1; this is the checker's source review.
- CONFIRMED | [goodstein-instrument] start at: 3 - finishes fast 4 - the long climb 16 - watch it explode ▶ step ⏩ run ⟲ reset step 0 · base 2 | git show 60ea23c371:public/strata/godel-incompleteness/index.html | buttons data-start="3", "4", "16" (lines 320-322). recreated with the pinned goodstein.mjs under the page caps (350 digits, 40000 steps): 3 reaches 0 at step 5; 4 is still 10 digits at step 40000; 16 passes 150 digits at step 7 and pauses at step 11 (409 digits). Retained from N2-claude.md, entry goodstein-instrument; this is the checker's source review.
- CONFIRMED | [b42-2] This page operates the two gears - arithmetisation and self-reference - and states the theorems exactly. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | self-description; true of the page. Retained from N2-claude.md, entry b42-2; this is the checker's source review.
- CONFIRMED | [b42-3] It does not build the full proof: writing out the arithmetical predicate Proof(m, n) (“m codes a proof of the formula coded by n”) and deriving the Gödel sentence inside a formal system is the work of a machine-checked development, not a browser toy. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | the page does not formalise Proof(m, n). Retained from N2-claude.md, entry b42-3; this is the checker's source review.
- CONFIRMED | [b42-4] What's shown is the mechanism and the precise claim; what's cited is the rest. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | self-description. Retained from N2-claude.md, entry b42-4; this is the checker's source review.
- CONFIRMED | [b43-2] The arithmetisation machine and the quine are live and reproducible; | git show 60ea23c371:public/strata/godel-incompleteness/index.html | live code; verifier recreated. Retained from N2-claude.md, entry b43-2; this is the checker's source review.
- CONFIRMED | [b43-3] The “mind is not a machine” reading is flagged as a contested philosophical argument, not settled - that is the one place we deliberately do not take a side. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | card 4 says "a contested philosophical one, not a theorem" (its substance: card-4-3). Retained from N2-claude.md, entry b43-3; this is the checker's source review.
- CONFIRMED | [placard-1] This layer's check opens this page in a real browser and drives it. | git show 60ea23c371:verify-godel-incompleteness.mjs | reads #bignum, #quineVerdict, #gsValue etc. with page.textContent in a browser. Retained from N2-claude.md, entry placard-1; this is the checker's source review.
- CONFIRMED | [meta-quine] a program that prints itself (the same self-reference, made operable) | git show 60ea23c371:public/strata/godel-incompleteness/index.html | as run-quine. Retained from N2-claude.md, entry meta-quine; this is the checker's source review.
- CONFIRMED | [body-exact-bigint] with exact-`BigInt` encoding and prime-factorisation decoding | git show 60ea23c371:public/strata/godel-incompleteness/index.html | godel() and factorExps() use BigInt. Retained from N2-claude.md, entry body-exact-bigint; this is the checker's source review.
- CONFIRMED | [runtime-decode] (round-trip exact) | git show 60ea23c371:public/strata/godel-incompleteness/index.html | decode button handler. Retained from N2-claude.md, entry runtime-decode; this is the checker's source review.
- CONFIRMED | [runtime-quine] ✓ output is identical to the source, all 129 characters. It printed itself. | git show 60ea23c371:public/strata/godel-incompleteness/index.html | recreated: the quine-data element is 129 characters (quine.js is the same plus a newline, 130 bytes). Retained from N2-claude.md, entry runtime-quine; this is the checker's source review.
- CONFIRMED | [runtime-completion] Done. The sequence from 3 reached 0 in 5 steps | git show 60ea23c371:public/strata/godel-incompleteness/index.html | recreated: 3 reaches 0 at step 5. Retained from N2-claude.md, entry runtime-completion; this is the checker's source review.
- CONFIRMED | [runtime-plot] the integer climbing | git show 60ea23c371:public/strata/godel-incompleteness/index.html | drawSpark label "log10(value) - the integer climbing". Retained from N2-claude.md, entry runtime-plot; this is the checker's source review.

## Findings

- [fixed] X1 (code-table-visibility): Replaced the button-table claim with the actual recipe-exponent location. MINOR, recorded without a page correction line.
- [fixed] X2 (conditions-demo-coverage): Narrowed both the page and markdown demonstration descriptions to arithmetic strength and consistency. MINOR, no page correction line.
- [fixed] X3 (gentzen-ordinal-date): Changed the exact ordinal result from 1936 to 1943; added and mirrored its Corrected line.
- [fixed] X4 (goodstein-four-step-count): Changed the displayed transition count to 3·2^402653211 − 3; added and mirrored its Corrected line.
- [fixed] X5 (goodstein-start-controls): Restricted both prose and runtime full-fall promises to start 3; added and mirrored its Corrected line.
- [fixed] X6 (consistency-implies-soundness): Replaced the soundness inference with the actual consistency restriction; added and mirrored its Corrected line.
- [fixed] X7 (physical-theory-exclusion): Said the hypotheses must be checked for the chosen formalization. MINOR, no page correction line.
- [fixed] X8 (paris-harrington-priority): Replaced unqualified first priority with a landmark natural statement of finite combinatorics independent of PA. Kept the title and 1977 publication details. MINOR, no page correction line.
- [fixed] X9 (paris-harrington-priority): Replaced unqualified first priority with a landmark natural statement of finite combinatorics independent of PA. Kept the title and 1977 publication details. MINOR, no page correction line.
- [fixed] X10 (encoding-interface-scope): Qualified the dek as encoding and decoding strings of up to twelve symbols from its palette. MINOR, no page correction line.
- [dated] X11 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [fixed] X12 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.
- [dated] X13 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [fixed] X14 (ordinal-coefficient-order): Fixed recursive ordinal rendering in both engines and the published copy, clarified tree wording, and added independent expected-notation checks. Added and mirrored its Corrected line.
- [fixed] X15 (goodstein-pause-reason): Made the pause message identify the actual exceeded limit, with browser checks for both branches; added and mirrored its Corrected line.
- [fixed] X16 (goodstein-start-controls): Restricted both prose and runtime full-fall promises to start 3; added and mirrored its Corrected line.
- [fixed] X17 (paris-harrington-priority): Replaced unqualified first priority with a landmark natural statement of finite combinatorics independent of PA. Kept the title and 1977 publication details. MINOR, no page correction line.
- [fixed] X18 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.
- [fixed] X19 (ordinal-coefficient-order): Fixed recursive ordinal rendering in both engines and the published copy, clarified tree wording, and added independent expected-notation checks. Added and mirrored its Corrected line.
- [fixed] K1 (quine-description-roles): Clarified the two printed roles in the page and notebook. MINOR, no page correction line.
- [fixed] K2 (diagonal-lemma-credit): Used the diagonal lemma in the page and notebook. The repair review also removed the remaining attribution from the Lawvere reference and research verifier comment. MINOR, no page correction line. Published checks are rebuilt at landing.
- [fixed] K3 (conditions-demo-coverage): Narrowed both the page and markdown demonstration descriptions to arithmetic strength and consistency. MINOR, no page correction line.
- [fixed] K4 (gentzen-ordinal-date): Changed the exact ordinal result from 1936 to 1943; added and mirrored its Corrected line.
- [fixed] K5 (goodstein-four-step-count): Changed the displayed transition count to 3·2^402653211 − 3; added and mirrored its Corrected line.
- [fixed] K6 (goodstein-start-controls): Restricted both prose and runtime full-fall promises to start 3; added and mirrored its Corrected line.
- [fixed] K7 (consistency-implies-soundness): Replaced the soundness inference with the actual consistency restriction; added and mirrored its Corrected line.
- [fixed] K9 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.
- [fixed] K10 (paris-harrington-priority): Replaced unqualified first priority with a landmark natural statement of finite combinatorics independent of PA. Kept the title and 1977 publication details. MINOR, no page correction line.
- [fixed] K11 (encoding-interface-scope): Qualified the dek as encoding and decoding strings of up to twelve symbols from its palette. MINOR, no page correction line.
- [dated] K12 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [fixed] K13 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.
- [dated] K14 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [dated] K15 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [fixed] K16 (goodstein-start-controls): Restricted both prose and runtime full-fall promises to start 3; added and mirrored its Corrected line.
- [fixed] K17 (paris-harrington-priority): Replaced unqualified first priority with a landmark natural statement of finite combinatorics independent of PA. Kept the title and 1977 publication details. MINOR, no page correction line.
- [fixed] K18 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.
- [dated] K19 (misuse-count-six): Updated misuse counts to seven in markdown, metadata, JSON-LD, the notebook and verifier, including its published copy. One shared Updated line dates the change. The independent six-formula sample count is unchanged.
- [fixed] K20 (goodstein-instance-unprovability): Made the universal quantifier explicit throughout the dek, metadata, explanation, misuse card and notebook; separated visible growth from the complete start-3 run. Added and mirrored one shared Corrected line.