Godel's Second Incompleteness theorem and Models 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.
 A: 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 .
A: 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.
A: 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!
