As I understand it, Godel's completeness theorem essentially says that if a sentence $\phi$ can be proven in a first order theory $\Gamma$, then $\phi$ is satisfied in all models $\mathcal{U}$ of $\Gamma$.

The first incompleteness theorem can be understood to mean that there are some sentences $\phi$ that cannot be proven in $\Gamma$ and this is because there are models of $\Gamma$ in which $\phi$ is satisfied and other models in which $\phi$ is not satisfied.

The second incompleteness theorem then states that one such sentence is $Con(\Gamma)$, the statement that "$\Gamma$ is consistent".

I've been trying to understand what this theorem means in terms of the models of the theory.

Proving $\Gamma$ is consistent is equivalent (I think!) to showing that there exists a model $\mathcal{U}$ of $\Gamma$. My question is essentially:

Is the second incompleteness theorem true because in some models $\mathcal{U}$ of the theory you cannot construct a submodel $\mathcal{V}$ obeying the axioms of $\Gamma$ and hence in those models you cannot prove consistency. Then, since in this particular model you can't prove consistency, it follows from the completeness theorem that you can't prove consistency directly from the axioms of $\Gamma$.

Even if this reasoning is completely wrong, I'm essentially just looking for a model-theoretic explanation of the second incompleteness theroem.

  • $\begingroup$ Note that even if $\Gamma$ is consistent, it could still prove $\neg \mathcal{C}on(\Gamma)$, so the situation is different from the usual undecidable sentences. Also, the second incompleteness theorem assumes as hypothesis (among others) that $\Gamma$ is indeed consistent, so while you will have at least one model where $\mathcal{C}on(\Gamma)$ does not hold, your theory is still consistent though, it's just that this particular model is not "aware" of it. $\endgroup$
    – godelian
    Feb 10, 2014 at 12:43
  • $\begingroup$ I'm not completely sure if I know what model-theoretic explanation you are looking for, but let me just say, assume $\Gamma$ is consistent, since $Con(\Gamma)$ is not provable from $\Gamma$, there is a model of $\Gamma$ such that $\neg Con(\Gamma)$ is true, namely, in this model you could even show that ``$\Gamma$ proves $\exists v (v\neq v)$'' $\endgroup$
    – Jing Zhang
    Feb 10, 2014 at 12:44
  • 7
    $\begingroup$ @DarMM your first sentence states the soundness theorem for first-order logic, not the completeness theorem. The completeness theorem is the converse of the soundness theorem. $\endgroup$ Feb 10, 2014 at 12:47
  • $\begingroup$ Thank you all. Godelian, that's basically the kind of idea I was looking for, i.e. the model not being "aware" of its own consistency. Similar to how you can have countable models of the reals and naturals in countable models of ZFC, but yet (due to the necessary bijections being missing from the model) the model isn't aware they are the same size. Zhang, that's very interesting. Benedict, you are right of course, thank you. $\endgroup$
    – DarMM
    Feb 10, 2014 at 13:45
  • $\begingroup$ The first incompleteness theorem imposes very important restrictions on $\Gamma$: it must be computably axiomatizable and it must interpret a sufficient fragment of arithmetic. $\endgroup$ Feb 12, 2014 at 0:11

3 Answers 3


Your explication is essentially correct if the theory you are dealing with is strong enough so that it can manipulate (infinite) models as objects of the theory, and prove the completeness theorem. This is true for typical set theories (but not for typical arithmetical theories). You might be interested in Jech’s proof of Gödel’s theorem: http://www.math.psu.edu/jech/preprints/goedel.pdf .

  • $\begingroup$ Thank you Emil, your comments and the paper have cleared things up for me. $\endgroup$
    – DarMM
    Feb 10, 2014 at 13:52

No. Gödel's completeness theorem says that if a sentence ϕ is satisfied in all models of the first-order theory Γ, then it can be formally proven in Γ. The first sentence of your question merely expresses that a given formal calculus is sound.

Gödel's first incompleteness theorem should not be thought of in terms of models. It states the existence of a sentence that is not deducible (nor its negation) in any "reasonable" first-order calculus for number theory.

Completeness and incompleteness mean very different things here.

  • $\begingroup$ Perhaps I have understood things incorrectly, but I got the impression from discussing it with logicians that the reason Godel's first incompleteness theorem is true is because for those sentences which cannot be deduced (nor their negation) are undeducible because there exists models of the axioms where the sentence is true and other models where its negation is true. $\endgroup$
    – DarMM
    Feb 12, 2014 at 21:20
  • 1
    $\begingroup$ I would say that the "reason" it's true is found in the proof itself, namely in the possibility of coding the syntax of the formal system within itself. The proof is entirely syntactic. Note that the undecidable sentence is actually true provided the formal system is consistent. $\endgroup$ Feb 13, 2014 at 21:49
  • $\begingroup$ Thank you Lawrence, I can see now that I hadn't fully understood this (to use loose language) syntactic/semantic distinction and was attempting to understand purely syntactic facts semantically. $\endgroup$
    – DarMM
    Feb 14, 2014 at 8:42
  • $\begingroup$ @Lawrence Paulson: What does it mean and why "the undecidable sentence is actually true"? $\endgroup$ Mar 28, 2015 at 3:54
  • $\begingroup$ @IsaacGorelic, the undecidable sentence (call it G) uses a fixed point argument to refer to itself. G states that that G is not provable within the formal calculus. And as G is indeed not provable, it is true. All this rests on our assumption that the calculus is consistent. We cannot hope to prove consistency, so in a sense, the truth of G is unknowable. $\endgroup$ Mar 29, 2015 at 16:28

Assume $\Gamma$ is strong enough to talk about models and prove the completeness and incompleteness theorems. In this case, $\Gamma+\neg Con(\Gamma)$ is consistent provided that $\Gamma$ itself is consistent. Then, no model of $\Gamma+\neg Con(\Gamma)$ agrees that there is a model of $\Gamma$ as it would believe $\neg Con(\Gamma)$. This is an example of what you are describing.

However, that particular model believing that there are no models of $\Gamma$ inside it does not actually imply there are no such models from outside perspective. It may just not recognize some structures as models of $\Gamma$ because its notion of natural numbers and proofs do not coincide with the real world!

For the case of ZFC, you should check this beautiful argument explained by Joel Hamkins multiple times on MO!


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.