# Understanding the role of Metatheories through an example

I've been studying for a course in set theory and I still have some problems in understading clearly the relation metatheory\theory. Being more specific, I'll present an example:

If we choose $$\mathrm{ZFC}$$ as our metatheory we can prove the completeness theorem for first order languages, right? But I have developed two different (?) interpretations about the nature of such "proof"

1. If we chooe $$\mathrm{ZFC}$$ as a metatheory that means that we are encoding our formal (first order) language (and theories) inside $$\mathrm{ZFC}$$, for example in $$\mathrm{V}_\lambda$$. Now formulae and formal proofs are elements of $$\mathrm{V}_\lambda$$ and $$\mathrm{ZFC}$$ can recognize and manipulate them. So the proof of completeness theorem will be a formal proof (inside $$\mathrm{ZFC}$$) so that: $$\mathrm{ZFC}\vdash \forall \ \ulcorner \mathrm{T}\urcorner( \mathrm{Con}(\ulcorner \mathrm{T}\urcorner)\longleftrightarrow \mathrm{Mod}(\ulcorner \mathrm{T}\urcorner) \neq \emptyset )$$
2. Choosing $$\mathrm{ZFC}$$ as a metatheory means that we simply take its axioms and work with them in the usual informal mathematical framework. So the proof of the completeness theorem will not be a formal (first order) proof as in the previous case, but a "standard" mathematical proof.

I'd lean towards the first one, although I sense that there is something missing. In this case Gödel's incompleteness theorems appears clearly to me to be mathematical results generating from taking certain theories simultaneously as both the object theory and the metatheory.

So, what is the issue here? Are both of them wrong? One of them is closer to being true?

Thanks

Your interpretation of "ZFC as the metatheory" is right (except we don't need the $$V_\lambda$$-bit), at least ideally: to a formalist,

• "Every consistent theory has a model"

is slang for

• "ZFC proves [Every consistent theory has a model]$$_{appropriately formulated}$$" (and moreover we either have such a formal proof in hand or we're confident that the natural language proof of the completeness theorem is a satisfactory blueprint for a formal ZFC-proof of [Every consistent theory has a model]$$_{appropriatelyformulated}$$).

Why did I say "at least ideally?" Well, there are two subtelties here about how this is actually practiced. The first is the bit about what happens if we don't right now have a formal ZFC-proof in hand: there's an element of subjectivity here, since two different people can reasonably disagree over whether a given natural language proof really is a satisfactory blueprint. The second is about the "appropriately formulated" bit: there's an implicit claim that the formal $$\{\in\}$$-sentence $$\chi$$ which we look at is in fact an appropriate formulation of the original natural-language mathematical claim. This is a really slippery thing to pin down precisely. However, I don't know of any actual situation where there's any doubt on this point (and ultimately the formalist would say that if there's serious doubt then the original claim was too vague to be meaningful).

(Note that these subtleties mean that your second interpretation isn't really wrong; rather, what's going on is that your second interpretation describes what we actually do while your first interpretation describes what (according to a formalist) we ought to do.)

In this case Gödel's incompleteness theorems appears clearly to me to be mathematical results generating from taking certain theories simultaneously as both the object theory and the metatheory.

This isn't right - Godel's theorem, appropriately approached, is not foundationally subtle at all. Namely, blackboxing the subtleties mentioned above, ZFC proves

$$(*)\quad$$ "For any computably axiomatizable theory $$T$$ interpreting Robinson arithmetic, if $$T$$ is consistent then $$T$$ is incomplete."

(In fact, galactically less than ZFC is needed, and $$(*)$$ can be improved.)

Note that Godel's theorem as phrased this way doesn't involve any object/meta-theory relationship: it's just a perfectly concrete mathematical claim, proved like any other such claim. Moreover, ZFC proves straightforwardly that $$(*)$$ applies to ZFC in the sense that ZFC proves "If ZFC is consistent then ZFC is incomplete." Note that hypothesis: ZFC isn't proving its own incompleteness, it's proving its own conditional incompleteness.

It may help to read about approaches to formally proving the incompleteness theorem (see e.g. here).

• Thank you for the interesting answer! Regarding the Incompleteness theorems, I wasn't saying that they are foundationally subtle. What I was saying is that it seems to me as they are results that "morally" comes from encoding a theory into itself, hence from using the same theory as object and meta theory in a formal way. I was just trying to give some meta-mathematical context to the theorem, which by itself does not need any meta-mathematics. Commented Apr 6, 2020 at 15:05
• Also, why is the $V_\lambda$-bit wrong? I suspected that it wasn't right, since every time I've seen a set-theoretic encoding of syntax was always in $V_\omega$, but I was moved by the (probably wrong) thought that maybe we could encode uncountable languages... Commented Apr 6, 2020 at 15:11
• @Lorenzo It's not really wrong, it's just unnecessary. We can talk about arbitrary-cardinality sets of sentences right off the bat, there's no need to work within some fixed $V_\lambda$. (In fact, we can even talk about proper classes of sentences as long as we're quite careful.) Commented Apr 6, 2020 at 17:12