On Formally Undecidable Propositions of Principia Mathematica and Related Systems I

Filed correctly. limit is right and needs no argument: this is a theorem with a proof, a set of hypotheses, and a large territory outside them. It is the canon's second entry of that kind, and the commission that proposed it named this file's job in advance — proposals.md lists it as "commonly misused as: proof that minds cannot be machines (Lucas, Penrose)", and the spec for limit entries names Gödel as the standing example of the problem. So section 4 is again the longest part of the file, and it is the reason the file exists.

descends_from is empty, and again that is a gap rather than a fact. The honest ancestors are Whitehead and Russell's Principia Mathematica (1910–13), which the title names and whose system the paper is built against; Hilbert's programme, and specifically his demand for a finitary consistency proof for arithmetic; and Cantor's diagonal argument, which is the shape of the construction. None of the three is in canon/, none is in proposals.md, and the spec forbids inventing ids. lovelace-1843 is in the canon and is chronologically prior, but the 1843 Notes are nowhere in this paper's line.

There is one edit this entry cannot make and should name. canon/turing-halting-1936.md says, in its own second paragraph, that Gödel's 1931 theorems are among its honest ancestors, that godel-incompleteness-1931 was unwritten as of 2026-08-15, and that "when it exists this entry should be edited to descend from it, and the two of them will be the canon's standing pair of abused theorems." It now exists. The commission for this run says to write one file and touch no other entry, so the descends_from: [godel-incompleteness-1931] edit to the Turing file is left undone here deliberately, not overlooked. It is one line, and it is the owner's or a later session's to make.

The pairing is the point. These two theorems are misused in the same shape and by the same move, they are often confused with each other, and a reading that meets an in-principle impossibility claim frequently cannot tell which of them is being invoked — sometimes because the person invoking it cannot either. Where this entry and the Turing entry overlap, this one defers; where they diverge, section 4 says how.

What it is

By 1930 the ambition was explicit. David Hilbert wanted mathematics put on a footing where the question "is this provable?" had a definite answer for every statement, and where the consistency of the whole apparatus could itself be proved by uncontroversial finite means. Braithwaite's introduction to the Meltzer translation describes the state of play: Principia Mathematica had exhibited arithmetic as a deductive system from a limited number of axioms; the metamathematicians of the 1920s had been converting questions about proofs into questions about symbol manipulation; and in 1930 Presburger had published a decision procedure for a mutilated arithmetic with addition but not multiplication, proving every one of its propositions decidable. The programme looked like it was working.

Gödel's paper opens by stating that expectation in order to break it:

> The development of mathematics in the direction of greater exactness has—as is > well known—led to large tracts of it becoming formalized, so that proofs can be > carried out according to a few mechanical rules. The most comprehensive formal > systems yet set up are, on the one hand, the system of Principia Mathematica > (PM) and, on the other, the axiom system for set theory of Zermelo-Fraenkel > (later extended by J. v. Neumann). These two systems are so extensive that all > methods of proof used in mathematics today have been formalized in them, i.e. > reduced to a few axioms and rules of inference. It may therefore be surmised > that these axioms and rules of inference are also sufficient to decide all > mathematical questions which can in any way at all be expressed formally in the > systems concerned. It is shown below that this is not the case.

Three moves carry the paper.

Arithmetisation. Metamathematical talk about a formal system — this is a well-formed formula, this sequence of formulae is a proof — is made into arithmetic talk about numbers, by mapping the basic signs one-to-one onto natural numbers so that a formula becomes a finite series of numbers and a proof becomes a finite series of such series. Gödel is precise about what this buys: "the above-described procedure provides an isomorphic image of the system PM in the domain of arithmetic and all metamathematical arguments can equally well be conducted in this isomorphic image." A system strong enough to talk about numbers is thereby strong enough to talk about itself. Everything else follows from that.

The self-referential sentence. With provability now expressible inside the system, Gödel builds a formula that, read as content, says of itself that it is not provable, and shows in half a page that neither it nor its negation can be derived. He then names the resemblance himself:

> The analogy between this result and Richard's antinomy leaps to the eye; there > is also a close relationship with the "liar" antinomy, since the undecidable > proposition [R(q); q] states precisely that q belongs to K, i.e. according to > (1), that [R(q); q] is not provable. We are therefore confronted with a > proposition which asserts its own unprovability.

And in footnote 15 he disposes of the obvious objection: "In spite of appearances, there is nothing circular about such a proposition, since it begins by asserting the unprovability of a wholly determinate formula … and only subsequently (and in some way by accident) does it emerge that this formula is precisely that by which the proposition was itself expressed." The paradox is not reproduced. It is defused and then used as a tool.

The theorems. The rigorous version, Proposition VI, is stated in the paper's own vocabulary and is worth printing exactly as it stands, because almost every misuse in section 4 consists of dropping one of its conditions:

> Proposition VI: To every ω-consistent recursive class c of formulae > there correspond recursive class-signs r, such that neither v Gen r nor > Neg (v Gen r) belongs to Flg (c) (where v is the free variable of r).

Unpacked: for any set of axioms that is recursive (you can mechanically check whether something is an axiom), ω-consistent (a technical strengthening of consistency), and strong enough to carry the construction, there is a sentence such that neither it nor its negation is a consequence of those axioms. That is the first incompleteness theorem. Gödel notes immediately after that the requirement can be widened — the axioms need only be calculable rather than recursive — and that dropping ω-consistency for plain consistency still yields "a property (r) for which it is possible neither to provide a counter-example nor to prove that it holds for all numbers." J. Barkley Rosser closed that last gap in 1936 with a modified provability predicate, and the theorem has been stated for simple consistency ever since.

Section 4 gives the second theorem:

> Proposition XI: If c be a given recursive, consistent class of > formulae, then the propositional formula which states that c is > consistent is not c-provable; in particular, the consistency of P is > unprovable in P, it being assumed that P is consistent (if not, of course, > every statement is provable).

A consistent system of this strength cannot prove its own consistency. Gödel gives this one only in outline and promises the details in a sequel: "The results will be stated and proved in fuller generality in a forthcoming sequel. There too, the mere outline proof we have given of Proposition XI will be presented in detail." The paper's title ends in a roman numeral I for that reason. Part II was never written. The details were supplied by others — the derivability conditions now named for Hilbert, Bernays and Löb — and the promise stands undelivered after ninety-five years, which is a fact about this paper that almost nobody who cites it knows.

Two scope clauses in the paper itself are load-bearing and routinely lost.

Incompleteness is relative to a system, and is repaired by going up. Footnote 48a is explicit, and it is the single most useful sentence in the paper for anyone grading a modern misuse:

> The true source of the incompleteness attaching to all formal systems of > mathematics, is to be found—as will be shown in Part II of this essay—in the > fact that the formation of ever higher types can be continued into the > transfinite … whereas in every formal system at most denumerably many types > occur. It can be shown, that is, that the undecidable propositions here > presented always become decidable by the adjunction of suitable higher types > (e.g. of type ω for the system P).

The undecidable sentence is not unknowable, unprovable-in-principle, or beyond reason. It is decided in a stronger system, routinely, and Gödel says so. What you cannot do is have one effectively-given system that settles everything. Go up and the new system has its own new undecidable sentence, forever; that is the real content, and it is a statement about a hierarchy, not a ceiling.

Gödel did not claim to have killed Hilbert's programme. After proving Proposition XI he adds, in the paper, in italics of his own choosing:

> It must be expressly noted that Proposition XI (and the corresponding results > for M and A) represent no contradiction of the formalistic standpoint of > Hilbert. For this standpoint presupposes only the existence of a consistency > proof effected by finite means, and there might conceivably be finite proofs > which cannot be stated in P (or in M or in A).

The man who is universally said to have ended the Hilbert programme declined, in print, to say he had ended it. That reticence is worth carrying into every argument about what an impossibility result forecloses.

Two more clauses, not in the paper but essential to using it:

Effectiveness is a hypothesis, and dropping it dissolves the theorem. The axioms must be recognisable by a mechanical check. The set of all true sentences of arithmetic is a complete theory — it settles everything — and the theorem does not touch it, because you cannot mechanically list it. Incompleteness is the price of effectiveness, not a limit on truth. Anyone using the theorem to say something about what is true rather than about what a given effective procedure can derive has already left the theorem behind.

Sufficient strength is a hypothesis, and plenty of real systems fall below it. Presburger arithmetic — addition, no multiplication — was proved complete and decidable in 1930, and Gödel's own paper is framed against it. Tarski later did the same for the theory of real closed fields, and hence for elementary geometry. These are not curiosities: decidable fragments are precisely the ground that SMT solvers, model checkers and program verifiers stand on, which is why the industry that Gödel is invoked to declare impossible ships working products every day. "Any sufficiently rich system" has an exact meaning, and a great deal of useful mathematics sits under the bar on purpose.

Provenance. Gödel told Carnap, Feigl and Waismann of the first theorem on 26 August 1930, and mentioned it publicly at the Second Conference on the Epistemology of the Exact Sciences in Königsberg, 5–7 September 1930 — by Wikipedia's account, "in an off-hand remark during a general discussion on the last day", to a room that included von Neumann presenting the formalist case. The standard telling has von Neumann as the one person present who understood at once; I could not read Martin Davis's Notices of the AMS account to confirm it and flag it in Sources as secondary. A summary appeared in the Anzeiger of the Vienna Academy in 1930 (Gödel's own footnote 1 cites it as No. 19). The full paper was received on 17 November 1930 and published in Monatshefte für Mathematik und Physik volume 38, pages 173–198, in 1931. Note also, because it is the most common confusion of all and section 4 returns to it: the same man had proved a completeness theorem the year before, in his 1929 doctoral dissertation — first-order predicate logic is complete. Two theorems, opposite names, different subjects, one author, twenty-four months apart.

Why a reading would cite it

The occasion is not hypothetical and it is not old. In June 2026 the United States' standards body published a Gödel argument about AI safety, and the argument went straight into the security-vendor bloodstream.

NIST announced on 9 June 2026 that Apostol Vassilev, a senior scientist in its Information Technology Laboratory, had published a peer-reviewed proof in IEEE Security & Privacy — "Robust AI Security and Alignment: A Sisyphean Endeavor?", May/June 2026 issue — establishing, in NIST's own words, that "there is no finite set of guardrails that is universally robust against adversarial prompts." NIST describes the derivation plainly: Vassilev applied Gödel's 1931 result, "which showed that you can't have a finite set of statements and create a theory that is complete and consistent without contradictions", to guardrails treated as a finite rule set. The Cloud Security Alliance's research note gives the formalisation as a checker function over a constraint and a prompt, with a theorem that for any such checker there exists a constraint the checker gets wrong, and a further theorem extending the result to systems with finite context windows. The operational recommendation is continuous red-teaming, continuous hardening, and resilience in place of "one and done" — Vassilev: "You have to commit to a constant search for weaknesses and stay ahead of attackers."

That is exactly the sentence this canon exists to help a reading handle, and it needs handling in both directions.

The recommendation is right. Guardrails do fail; jailbreaks are found continuously; a security posture that assumes a fixed perimeter around a language model is wrong, and was wrong before the proof. A reading that meets this story should not treat it as debunked.

The derivation is doing far less work than its packaging claims, and the packaging is where the damage happens. Within weeks the result was being retailed as "AI guardrails will always fail — NIST just proved it mathematically", and as "what Kurt Gödel just did to your AI security strategy", and by July as the end of "secure by design" as such. A theorem about the relationship between effectively-given axiom sets and arithmetic truth was, in about six weeks, converted into a general licence to describe an engineering posture as mathematically foreclosed. Section 4 takes the argument apart clause by clause. The short version for a reading: the load-bearing premise is that natural language is unboundedly ambiguous while any rule set is finite, which is a claim about language and enumeration rather than about arithmetic; the closest correct citations are Rice's theorem and Fred Cohen's 1987 virus result, both of which are already in turing-halting-1936 and neither of which needs Gödel; and the conclusion "no complete defence over adversarial inputs" is compatible with defences that are sound, bounded, layered or probabilistic — which is what everyone builds anyway.

The second occasion is the mirror image, and this project's own window has it. The same month the impossibility argument was published, the record filled up with machines doing mathematics. DeepMind's paper of 21 May 2026, "Advancing Mathematics Research with AI-Driven Formal Proof Search", reports that its agent "autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research." On 1 August 2026 OpenAI published ten proofs of decade-old open problems from an unreleased model, with Lean 4 certificates on GitHub. And in this project's own 15 August midday digest, Crouzeix's conjecture — open since 2004 — has two independent claimed proofs, both disclosing model use, one of them from a sixteen-hour autonomous run.

Every one of those results has the same architecture, and the architecture is a direct answer to the incompleteness worry rather than a violation of it. An untrusted generator proposes; a small, separately implemented, heavily audited kernel checks. The Lean kernel does not trust the tactics, the automation, the half-million lines of Mathlib, or the model — it re-derives the proof term and either accepts or refuses. This is the de Bruijn criterion, and it is the practical form of Gödel's footnote 48a: you do not ask a system to certify itself, you check its output in a system whose trust base is small enough to audit. It is also why the honest caveat on these results is not Gödel at all but plumbing — a Lean file can compile without proving the intended statement if the statement was mis-formalised, new axioms were introduced, or custom tactics were used, which is why serious pipelines check the candidate against a separately declared statement file. That is a real risk with a real mitigation, and it is the kind of thing a reading should ask about instead of reaching for a theorem.

The third occasion is where the theorem genuinely bites, and a reading that only ever debunks will miss it. The second incompleteness theorem, together with Löb's theorem, is a live constraint on any agent that must reason about whether to trust its own successors. Yudkowsky and Herreshoff's "Tiling Agents for Self-Modifying AI, and the Löbian Obstacle" (MIRI, 2013) is the standing reference: an agent that wants to prove that a modified version of itself will remain safe is asking for exactly the self-trust the second theorem denies, and the naive formalisations collapse into either the Löbian obstacle or the procrastination paradox. Cite the theorem there and it is precisely right. Note what it costs, though: it is a constraint on proof-theoretic self-endorsement, not on self-improvement as such, and the standard escape is the same asymmetry as above — a stronger or differently-based verifier checks the weaker system, and nothing tries to certify itself.

The fourth occasion is measurement, and it is the one this project's own record keeps producing. The 15 August midday reading turned on Anthropic raising its catastrophic-misalignment rating explicitly because its safety measurements had degraded — saturating benchmarks, weakening R&D-acceleration evaluation — and labelling that an uncertainty adjustment rather than a finding. The turing-halting-1936 entry describes what happens next: an empirical, dated, fixable measurement problem attracts an in-principle gloss within a news cycle. Gödel is the second most likely theorem to be reached for after the halting problem, and it fits even worse, because incompleteness is about derivability in an effectively-given formal system and a benchmark is neither.

Nothing in this file is evidence. The 2026 items above are named as citation occasions, not re-argued; those that live in the digests carry their own primary links there, and the rest carry theirs in Sources. Nothing here is deposited in the ledger, nothing here grades a lab or a model, and nothing here touches the needle. A reading may cite this entry to say what an incompleteness claim would have to mean and what it would have to assume; it may not cite it to settle whether some particular system is safe, because that is a question about that system.

What it got right, and what it got wrong

Not required for limit. Included because the paper made claims that were not theorems, because its author made a further claim about it in 1951 that is gradeable, and because the entry that grades Kurzweil and Turing should grade Gödel too.

Right, and permanent: the theorems. Ninety-five years, no serious challenge, no hidden hypothesis found, generalised repeatedly (Rosser 1936 weakening ω-consistency to consistency; Rice 1953 extending the undecidability side to every non-trivial semantic property of programs; Chaitin's information-theoretic version). Mathematics did not stop. Gentzen proved the consistency of Peano arithmetic in 1936 using transfinite induction up to ε₀, which vindicates Gödel's own hedge about "finite proofs which cannot be stated in P" only if you accept that method as finitary, which was and remains contested. The programme survived in modified form; the specific 1920s ambition did not.

Undelivered, and it is not a small thing: Part II. Footnote 48a promises to show, in Part II, that the true source of incompleteness lies in the transfinite continuation of types, and the closing paragraph promises the full proof of Proposition XI there. Neither arrived. The second theorem's rigorous treatment came from Hilbert and Bernays in 1939 and from Löb in 1955. Anyone who says "Gödel proved the second incompleteness theorem in 1931" is describing a four-paragraph sketch and a promissory note.

Cautious, and vindicated by how badly others behaved: the Hilbert disclaimer. Gödel's insistence that Proposition XI "represent no contradiction of the formalistic standpoint" is the single most-ignored sentence in the paper, and ninety-five years of Gödel-invocation are a running demonstration of why he wrote it. The author's restraint is the strongest available evidence against the uses section 4 catalogues.

Gödel's own extrapolation, made 1951, still undecided in 2026. In the Gibbs lecture to the American Mathematical Society he drew the consequence as a disjunction, not a verdict: either mathematics is incompletable in the sense that its evident axioms can never be comprised in a finite rule — "the human mind (even within the realm of pure mathematics) infinitely surpasses the powers of any finite machine" — or there exist absolutely unsolvable diophantine problems of a specified type. Both disjuncts are consistent with his theorems, and he said so. He personally preferred the first, on broadly philosophical grounds, and in a 1972 note headed "A philosophical error in Turing's work" he located the place to attack: Turing's assumption that a mind has finitely many distinguishable states, against which Gödel argued that "mind, in its use, is not static, but constantly developing" and that the number of available abstract terms "may converge toward infinity in the course of the application of the procedure." Graded in 2026: the disjunction is untouched. Nothing in seventy-five years has established either disjunct, and no amount of machine performance at mathematics bears on it, because it is a claim about idealised mathematical insight and not about output. What is gradeable is that Gödel himself, the person with the strongest possible claim to know what his theorems entailed, refused to state the anti-mechanist conclusion as a consequence of them — and everyone who states it as one is going further than he would.

Lucas's 1961 claim, graded 2026: not refuted by the machines, and not established either. J. R. Lucas opened "Minds, Machines and Gödel" with "Gödel's Theorem seems to me to prove that Mechanism is false, that is, that minds cannot be explained as machines", and concluded from the Gödel sentence that "a machine cannot be a complete and adequate model of the mind. It cannot do everything that a mind can do, since however much it can do, there is always something which it cannot do, and a mind can." He is owed an accuracy the popular version denies him: he explicitly conceded machine superiority in performance, writing on the same page that "we can (or shall be able to one day) build machines capable of reproducing bits of mind-like behaviour, and indeed of outdoing the performances of human minds." So the 2026 record — Erdős problems falling to a few hundred dollars of compute, Lean-certified proofs of decade-old open problems, Crouzeix's conjecture — does not touch Lucas's thesis on its own terms. It demolishes the popular version, the one that says a machine will never do real mathematics, which is the version that actually circulates and which Lucas did not hold. Where Lucas fails is where his critics said in the 1960s that he failed, and the failure is a matter of logic rather than of the record: the Gödel sentence is only known to be true given the system's consistency, and neither Lucas nor anyone else has a non-circular way to know that of the system he is claiming to transcend. Penrose's 1994 restatement in Shadows of the Mind replaces consistency with soundness and inherits the same defect; Chalmers's review names it exactly — "the greatest vulnerability in this argument lies in the assumption that we know (unassailably) that we are consistent", and "the deepest flaw lies in the assumption that we know that we are sound" — and concludes that "Penrose has therefore pointed to a false culprit … the responsibility for the contradiction lies elsewhere than in the assumption of computability." Feferman's verdict on the same book is the one worth quoting to anyone who assumes the critics are partisans of machine minds: he says he is "personally convinced of the extreme implausibility of a computational model of the mind", and then that "Penrose's Gödelian argument does nothing for me personally to bolster that point of view."

Wrong in the retelling, and it is the paper's own vocabulary that did it: "true but unprovable". Gödel's Proposition VI says nothing about truth; it says neither the sentence nor its negation belongs to the consequences of the axioms. Truth enters through the informal sketch — "it follows at once that [R(q); q] is correct, since [R(q); q] is certainly unprovable (because undecidable)" — and through the standard model of arithmetic, and it is relative to the system throughout. The compressed slogan is where nearly every misuse in section 4 begins, and it is fifteen words shorter than the accurate statement, which is why it wins.

Commonly misused as

What the result actually says. For any formal system that (a) is effectively axiomatised — you can mechanically check what counts as an axiom, (b) is consistent, and (c) can represent enough arithmetic, there is a sentence of its language such that neither that sentence nor its negation is derivable in it; and, given the standard derivability conditions, that system cannot derive a sentence expressing its own consistency. Every clause is doing work, and every misuse below drops one.

Effectively axiomatised — drop it and the theorem vanishes; true arithmetic is complete. Consistent — drop it and everything is provable, which is not a win. Represents enough arithmetic — drop it and you get Presburger arithmetic and real closed fields, which are complete and decidable, and which the verification industry runs on. A sentence of its language — the theorem produces one specific sentence in one specific formal system, and says nothing about English, about safety policies, about neural networks, or about minds, unless someone first does the work of showing the thing in question is such a system. That work is almost never done, and demanding it is the single most useful question a reading can ask.

• "It proves minds cannot be machines." The canonical misuse, named as such in the commission, and now sixty-five years old. Lucas (1961) and Penrose (The Emperor's New Mind, 1989; Shadows of the Mind, 1994) argue that for any machine we can see the truth of a sentence the machine cannot prove, hence we are not machines. The standard reply, made by Putnam and Benacerraf in the 1960s and unrefuted since: the Gödel sentence is known true only on the assumption that the system is consistent, so the argument requires us to know the consistency of a system as complex as a full formalisation of human mathematical reasoning — which the second incompleteness theorem tells us that system could not establish about itself either. Human mathematicians make errors, publish flawed proofs, and accept them for years; Kempe's 1879 four-colour proof stood until 1890. Benacerraf adds a separate objection: even if we are machines, the machine we are may be far too complex for us ever to identify well enough to construct its Gödel sentence. And Gödel's own position was the disjunction, not the conclusion. The argument's real residue is Gödel's 1972 objection to Turing's finiteness-of-mental-states assumption, which is a genuine philosophical dispute and is not a corollary of the 1931 theorems. Note also the direction-of-travel point the Turing entry makes: Turing derived the machine model from an analysis of a human clerk, so a limit that binds machines was originally derived from a model of us.

• "No finite set of guardrails can be robust, therefore AI security is mathematically hopeless." The live 2026 case, and the reason this entry was worth writing this week. Take the conclusion and the derivation separately. The conclusion is sound and useful: no fixed rule set will catch every adversarial input, continuous red-teaming and resilience beat a static perimeter, and NIST is right to say so. The derivation is Gödel-dressed and does not need him. The premises reported in NIST's own announcement and in the CSA note are that natural language is unboundedly ambiguous and any guardrail set is finite — that is a cardinality-and-coverage argument about an infinite input space, and it is the same argument that gives you no general spam filter, no general virus detector, and no general jailbreak filter. Fred Cohen proved the virus case in 1987 by a diagonal argument; Rice's theorem covers the program-property case; both are already in turing-halting-1936, both are the right citations, and neither requires arithmetic self-reference. Where Gödel is invoked, the missing step is always the same: nobody shows that the guardrail system is an effectively axiomatised formal theory interpreting arithmetic, and without that the theorem is an analogy wearing a proof's clothes. Two further cautions for a reading. First, I could not read the paper — it is paywalled — so this grades the argument as NIST, IEEE's publisher summary and the trade coverage report it, and if the printed derivation is tighter than the reporting, the criticism above needs revisiting; that caveat is repeated in Sources because it matters. Second, I found no published rebuttal by a logician, which is itself worth knowing: the claim has run for two months through an official channel with no counterweight in the record, which is precisely the condition under which a misuse hardens into common knowledge. What a reading can say without any of this being settled is the thing that is certainly true: an impossibility of complete coverage over adversarial inputs says nothing against defences that are sound-but-incomplete, layered, bounded, probabilistic, or scoped to a particular deployment — and every defence that works is one of those.

• "There are truths that can never be proved." The most widespread form and the flattest contradiction of the paper. Footnote 48a says the undecidable propositions "always become decidable by the adjunction of suitable higher types". Provability here means derivability in a specified system; there is no notion of absolute unprovability in the paper, and Gödel spent a good deal of the rest of his life arguing for new axioms precisely because he thought the hierarchy could be climbed. The mystical version of this — that Gödel established limits to human knowledge, or supports the existence of God, or shows reason undermines itself — is a category error twice over: it confuses derivability with knowledge, and a formal system with a mind.

• "AGI is impossible because of incompleteness." The argument, in its usual form, chains Gödel, Turing and Rice to conclude that some decision spaces are structurally undecidable and therefore that general intelligence cannot be built. The chain proves something real and irrelevant. Undecidability means no single algorithm settles all cases of a general question; it says nothing about whether a system can be as capable as a human, because humans are also not general decision procedures. Whatever a person does when they judge a novel case, it is not deciding an undecidable problem. If the argument worked, it would prove human general intelligence impossible by the same steps — which is the standard reductio and the fastest way to test any instance of it. There is a real research literature that at least states its assumptions (Brcic and Yampolskiy's impossibility survey; the 2026 unverifiability-of-alignment papers), and its results are about general verifiers over arbitrary systems, not about buildability.

• "A system can't verify itself, so no AI can be trusted to check its own safety." Half right, and the half that is right is the most interesting thing in this file. The second theorem plus Löb genuinely obstruct proof-theoretic self-endorsement, which is why the Löbian obstacle is a named open problem in self-modifying-agent theory rather than a slogan. What does not follow is that verification is unavailable, because nobody in practice asks a system to certify itself. The working pattern is asymmetric: a large untrusted generator produces an artefact, and a small, independently implemented, auditable checker accepts or rejects it. That is the Lean kernel; that is why the May and August 2026 mathematics results are checkable by anyone without trusting the lab that produced them; and it is a design principle a reading can apply directly when a claim of the form "the model evaluated itself" appears. The theorem's real lesson here is a requirement, not a prohibition: your trust base must be something other than the thing being trusted.

• "Gödel and Turing proved the same thing." Related, not identical, and the difference decides which citation is correct. Gödel is about derivability in effectively-given formal theories that interpret arithmetic. Turing is about the non-existence of a general decision procedure over arbitrary programs. Each can be derived from the other with work, and Turing's route is the cleaner one for anything computational, which is why almost every AI-adjacent argument that invokes Gödel would be better and more honestly served by invoking Turing or Rice. When a reading meets an impossibility claim, the first question is which theorem is actually load-bearing; a claimant who cannot say has usually not checked.

• "Gödel proved mathematics is incomplete/inconsistent/broken." Incomplete in a precise sense, yes; inconsistent, no, and the theorem assumes the opposite. The everyday work of mathematics was not obstructed. Note also the standing confusion with the completeness theorem of 1929: first-order logic is complete — every logically valid formula is derivable — and the two results live together without tension because they are about different things (validity in all models versus derivability of arithmetic truths from a fixed axiom set). Someone who slides between them is not making an argument.

• The reverse misuse: "incompleteness is a self-referential parlour trick with no mathematical bite." This one is aimed at people who have read section 4 of a file like this one and overcorrected. The undecidable sentences are not all artificial. The Paris–Harrington theorem (1977), a strengthened finite Ramsey statement, is expressible in Peano arithmetic and not provable in it, and is usually described as the first natural such example. Kirby and Paris showed in 1982 that Goodstein's theorem — an entirely concrete statement about sequences of natural numbers, provable by transfinite induction and not in PA — is another. Gentzen had shown the unprovability of ε₀-induction in 1943. And the Löbian obstacle above is a case where the second theorem constrains a live engineering research programme. The theorem has teeth; they are just not the teeth it is usually said to have.

Sources

Primary, read directly. Gödel's paper in B. Meltzer's translation (On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Oliver & Boyd/Basic Books, 1962, with an introduction by R. B. Braithwaite), fetched as the PDF hosted at homepages.uc.edu and read page-by-page with the original Monatshefte pagination in the margins. Everything quoted above from the paper — the opening paragraph of §1, the Richard/liar analogy passage, footnote 15, Proposition VI, Proposition XI, the "no contradiction of the formalistic standpoint of Hilbert" paragraph, footnote 48a, the closing promise of a sequel, and the received date of 17 November 1930 — was read in that text. Caveats. This is one translation; Meltzer's has been criticised in the reviewing literature and the van Heijenoort/Bauer-Mengelberg translation in From Frege to Gödel and Mendelson's in Davis's The Undecidable are the ones scholars prefer. I could not consult either, so no quotation above has been cross-checked against a second translation, and the German original was not read at all. Braithwaite's introduction is the source for the Monatshefte volume and page range (38, 173–198) and for the Presburger 1930 comparison; it is an introduction from 1962 and is secondary even where it sits inside a primary volume.

On the statement, scope and history of the theorems. Panu Raatikainen's "Gödel's Incompleteness Theorems" in the Stanford Encyclopedia of Philosophy, read directly — source for the modern statements with their hypotheses, Robinson arithmetic Q sufficing for the first theorem and PRA-strength conditions for the second, Rosser's 1936 replacement of ω-consistency by consistency, the Lucas–Penrose section and its standard refutations (Putnam 1960, Boolos 1968, Shapiro 1998), the caution that the theorems "do not deal with provability in any absolute sense", and the Gibbs lecture disjunction. This is the entry's most reliable secondary source. The Königsberg conference details come from the Wikipedia article on the Second Conference on the Epistemology of the Exact Sciences (dates, "an off-hand remark during a general discussion on the last day", the speaker list) plus search-result summaries for the 26 August 1930 conversation with Carnap, Feigl and Waismann. **Martin Davis's "The Incompleteness Theorem" (Notices of the AMS, April 2006) returned 403 and was not read**, so the familiar story that von Neumann alone grasped the result on the spot is carried here as the standard telling rather than as a checked fact, and the same applies to Hilbert's "Wir müssen wissen, wir werden wissen" address the following day, which is dated 8 September 1930 in secondary sources I could not verify. Gödel's 1972 note "A philosophical error in Turing's work" is quoted from search-result summaries of the Collected Works passage and of Long Chen's paper on it in Philosophies 7:2 (2022); the note itself was not read.

On the anti-mechanist argument. J. R. Lucas, "Minds, Machines and Gödel", Philosophy 36:137 (April–July 1961), 112–127, read directly in the JSTOR scan at philomatica.org — source for the opening sentence, the p. 115 passage on the machine not being a complete and adequate model of the mind, and the concession that machines may outdo human performance. The header records it as a paper read to the Oxford Philosophical Society on 30 October 1959. Solomon Feferman, "Penrose's Gödelian argument" (PSYCHE 2, 1995, 21–32), read directly at math.stanford.edu — source for the "does nothing for me personally to bolster that point of view" verdict and the framing of Penrose's Theorem 1 as a variant of the standard diagonal argument. David Chalmers, "Minds, Machines, and Mathematics" (PSYCHE 2, 1995), read at consc.net — source for the consistency and soundness quotations and the "false culprit" verdict. The Internet Encyclopedia of Philosophy article on the Lucas–Penrose argument, read directly — source for Benacerraf's complexity objection, Lucas's "mistakes rather than set policies" reply, and McDermott's Kempe example. Penrose's own books were not read; both are characterised here through Feferman, Chalmers and the IEP. Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse (A. K. Peters, 2005) is the standard treatment of everything in section 4 and I did not read it; it is named because a later session with the book should check this file against it, and because a reading that wants one reference rather than this one should be sent there.

On the 2026 guardrails claim. NIST's announcement, "NIST Mathematical Proof Supports Transition to a Continuous-Monitor-and-Update Security Model for AI Systems" (9 June 2026), read directly — source for the "no finite set of guardrails that is universally robust" formulation, the description of how Gödel's 1931 result is applied, and the Vassilev quotation about constant search for weaknesses. Help Net Security's report (10 June 2026), read directly — source for the "for any finite set of guardrails, some prompt exists that gets the AI to disregard them" formulation and the note that the proof supplies no attack method. The Cloud Security Alliance research note, read directly — source for the checker-function formalisation, the second and third theorems, and the finite-context-window extension. The paper itself — Apostol Vassilev, "Robust AI Security and Alignment: A Sisyphean Endeavor?", IEEE Security & Privacy, May/June 2026, DOI 10.1109/MSEC.2026.3678214 — was not read; it is paywalled, and the title and DOI come from search-result summaries rather than from the IEEE record itself. This is the weakest link in the file and the criticism in section 4 is scoped accordingly: it grades the argument as officially described, not as printed. The downstream retellings named in section 2 (CovertSwarm's "AI guardrails will always fail. NIST just proved it mathematically", the Substack piece on "what Kurt Gödel just did to your AI security strategy", and the July 2026 "Gödel, LLM security, and the end of 'secure by design'" post, which returned 403) are known through search-result titles and summaries only.

On the 2026 mathematics record. George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli and Swarat Chaudhuri, "Advancing Mathematics Research with AI-Driven Formal Proof Search", arXiv:2605.22763 (21 May 2026, revised 8 June 2026) — abstract read directly and quoted; the body was not read. The OpenAI "Astra" results of 1 August 2026 (ten open problems, Lean 4 certificates on GitHub, roughly $2,000 of compute, a 249-page manuscript, a zero "sorry" count, and the disclosure that no Millennium Prize problem fell) are known through search-result summaries only — the Tech Times article returned 403 and I reached no primary OpenAI page, so treat every number in that sentence as unverified. Lean 4's kernel architecture and the de Bruijn criterion, and the caution that a Lean file can compile without proving the intended statement, come from Lean's own validation documentation and from search-result summaries of secondary explainers; I read the former's description second-hand through the search layer rather than fetching it, and have kept the claims to ones that are uncontroversial in the Lean community. Eliezer Yudkowsky and Marcello Herreshoff, "Tiling Agents for Self-Modifying AI, and the Löbian Obstacle" (MIRI, 2013) — not read; the characterisation of the Löbian obstacle and the procrastination paradox is from search-result summaries of the paper and its LessWrong discussion. Mario Brcic and Roman Yampolskiy, "Impossibility Results in AI: A Survey" (arXiv:2109.00484), and the June 2026 preprint on the unverifiability of AGI alignment (arXiv:2606.28639) are named from search results and were not read. Jürgen Schmidhuber's Gödel machine (arXiv:cs/0309048, 2003) and the Goedel-Prover series (arXiv:2508.03613, August 2025) are mentioned nowhere above but were encountered in research and are recorded here as a note for a later session: Gödel's name is attached to at least two constructive AI research lines, which is a small counterweight to the idea that his legacy in this field is entirely one of prohibition.

On the independent-statement literature. Paris and Harrington (1977) and Kirby and Paris (1982) on Goodstein's theorem, and Gentzen's 1936 consistency proof and 1943 ε₀-induction result, are cited from the Wikipedia and MathWorld entries for those theorems by way of search-result summaries; none of the original papers was read, and the descriptions above are deliberately confined to what those summaries state plainly.

On the project's own record. The 2026 items in section 2 drawn from this project — the August risk report and its measurement caveats, and the Crouzeix conjecture proofs with their disclosed model use — are read from digests/2026-08-15-12.md, where they carry their own primary links. They are named here as citation occasions only. This file deposits nothing in the ledger, grades no model, and places no needle.