Okay, so I'm reading Smullyan's book on Gödel's incompleteness theorems, and I've just about finished the part where he shows that Peano arithmetic is incomplete using Tarski's truth set (chapter IV).

My only issue is that I cannot see how this applies directly to any axiom system apart from that specific variant of P.A.. The proof relies heavily on the symbols used and seems a far cry from the (badly quoted) "Any system capable of expressing P.A. is incomplete".

Why does this proof of the incompleteness of a very particular axiom system have any bearing upon other systems which could subsume it? I can see how I could modify the proof to apply the theorem to ZFC, perhaps, but I see nothing general here. Is this some theorem of logic that has not been mentioned?

  • 1
    $\begingroup$ Words to live by: interpretation of one theory in another. More specifically to this point, recursive interpretation. $\endgroup$
    – Asaf Karagila
    Jul 19, 2015 at 15:31
  • $\begingroup$ You can find a simple computability-based proof and discussion of the generalized incompleteness theorem (subsuming Godel-Rosser) in this post, and a more technical version in this post. Both apply to any reasonable foundational system that mankind can ever use, so there is no escape even if one rejects classical logic, as long as one still can perform very basic finitist reasoning about finite strings. $\endgroup$
    – user21820
    Oct 2, 2018 at 13:45
  • $\begingroup$ Can we conclude that Smullyan's book is flawed since it fails to explain that the incompleteness theorems apply to any other theory? $\endgroup$ Dec 9, 2021 at 12:20

2 Answers 2


See Gödel's Incompleteness Theorems.

"Preliminary" formulation :

First incompleteness theorem : Any consistent formal system $F$ within which a "certain amount of elementary arithmetic" can be carried out is incomplete; i.e., there are statements of the language of $F$ which can neither be proved nor disproved in $F$.

Precise formulation :

Gödel's First Incompleteness Theorem : Assume $F$ is a formalized system which contains Robinson arithmetic $\mathsf Q$. Then a sentence $G_F$ of the language of $F$ can be mechanically constructed from $F$ such that:

If $F$ is consistent, then $F ⊬ G_F$.

If $F$ is $1$-consistent, then $F ⊬ ¬G_F$.

$\mathsf {ZFC}$ is precisely such a formalized system $F$ (i.e. "a formal system within which a 'certain amount of elementary arithmetic' can be carried out").

Gödel's original proof in his Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") does not use $\mathsf {ZFC}$ nor $\mathsf {PA}$.

His proof is relative to a "variant" of Principia Mathematica system; but his proof - in addition to esatblish the result now know as Gödel's Incompleteness Theorems - provides also a method applicable to many formal systems, provided that they satisfy some "initial conditions".

All the systems known as $\mathsf Q, \mathsf {PA}, \mathsf {ZFC}$ satisfy these conditions.

Relevant to your question, you can see :

It can be interesting to note that Melvin Fitting's thesis advisor was Raymond Smullyan.

  • $\begingroup$ So what kind of formulation is Smullyan giving? His version is literally just "The system P.A. is incomplete" [direct quote]. I've looked over the later theorems, which he claims are simply alternate proofs given weaker premises, and I've yet to see anything too similar to that which you've written. $\endgroup$
    – Nethesis
    Jul 19, 2015 at 15:13
  • 3
    $\begingroup$ Here "contains Robinson arithmetic Q" needs to be taken in the sense "admits an interpretation of Q", because theories like ZF, having different primitive notions from those of Q, do not literally contain Q. $\endgroup$ Jul 19, 2015 at 15:32
  • $\begingroup$ @AndreasBlass I've not seen Robinson arithmetic anywhere in the book I'm reading. I'm wondering what's going on. $\endgroup$
    – Nethesis
    Jul 19, 2015 at 15:40
  • $\begingroup$ I haven't read Smullyan's book, so I don't know what formalization he uses. The incompleteness proof for theories that "contain" Robinson's Q is available in many places, for instance Peter Hinman's book "Fundamentals of Mathematical Logic". Shoenfield's book "Mathematical Logic" uses a very similar theory that he calls N in place of Q, but it's the same idea. The original source for Q is, I believe, a book "Undecidable Theories" by Tarski, Mostowski, and Robinson. $\endgroup$ Jul 19, 2015 at 15:46
  • $\begingroup$ Robinson's system Q is a finite set of axioms that are all provable in PA (which means that Q is strictly weaker than PA). Q is strong enough to prove the incompleteness theorems. In fact, I believe Robinson discovered it by working out what axioms of PA were actually used in the proof. $\endgroup$
    – Rob Arthan
    Jul 19, 2015 at 15:47

The incompleteness theorems apply to any system that admits a relative interpretation of PA or Robinson's system Q. See How to prove that Gödel's Incompleteness Theorems apply to ZFC? for more information.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .