**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 sets on their own, 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 consistent, it cannot prove its own consistence. 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 consistent, then it cannot prove the consistence 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 consistent, then it cannot prove the consistence 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 for natural numbers (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 consistence of **Set2**? Or I'm just confused and what I said does not make sense?

Of course one could just argue that **Set1**, not being formalized, is not amenable to mathematical investigation; the best model we have is **Set2**, so we should trust that we can always "shift our theorems one level". But this argument does not convince me: indeed Gödel's first incompleteness theorem shows that we have situations where the theorem in the formalized theory are strictly less then what we can see from the outside.

**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 not provable from the usual axioms of set theory.