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