Understanding the role of Metatheories through an example

Question

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

Answer 1

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).