**Disclaimer**

Of course not, I'm aware of Gödel's second incompleteness theorem. Still there is something which does not persuade me, maybe it's just that I've taken my logic class too long ago. On the other hand, it may turn out I'm just confused. :-)

**Background**

I will be talking about models of set theory; these are on their own sets, so a confusion can arise, since the symbol $\in$, viewed as set belonging in the usual sense, may have a different meaning from the symbol $\in$ of the theory. So, to avoid confusion I will speak about levels.

On the first level is the set theory mathematicians use all day. This has axioms, but is not a theory in the usual sense of logic. Indeed, to speak about logic we already need sets (to define alphabets and so on). In this *naif* set theory we develop logic, in particular the notions of theory and model. We call this theory **Set1**.

On the second level is the *formalized* set theory; this is a theory in the sense of logic. We just copy the axioms of the *naif* set theory and take the (formal) theory which has these strings of symbols as axioms. We call this theory **Set2**.

Now Gödel's result tells us that if **Set2** is coherent, it cannot prove its own coherence. Well, here we need to be a bit more precise. The claim as stated is obvious, since **Set2** cannot prove anything about the sets in the first level. It does not even know that they exist.

So we repeat the process that carried from **Set1** to **Set2**: we define in **Set2** the usual notions of logic (alphabets, theories, models...) and use these to define another theory **Set3**.

A correct statement of Gödel's result is, **I think**, that

>if **Set2** is coherent, then it cannot prove the coherence of **Set3**.

**The problem**

Ok, so we have a clear statement which seems to be completely provable in **Set1**, and indeed it is. This doesn't tell us, however that

>if **Set1** is coherent, then it cannot prove the coherence of **Set2**.

So I'm left with the doubt that what one can do "from the outside" may be a bit more than what one can do in the formalized theory. Compare this with Gödel's first incompleteness theorem, where one has a statement which is true in **PA** (and we can prove it from the outside) but which is not provable in **PA**.

So the question is:

> is there any reason to believe that **Set1** cannot prove the coherence of **Set2**? Or I'm just confused and what I said does not make sense?

**Final comment**

In a certain sense, it is far from intuitive that set theory should have a model. Because models are required to be sets, and sets are so small...

Of course I know about universes, and how one can use them to "embed" the theory of classes inside set theory, so sets may be bigger than I think. But then again, existence of universes is independent from the usual axioms of set theory.