# What "metatheory" did early set theory/logic researchers use to prove semantic results?

Things like the first-order completeness theorem and the Löwenheim-Skolem theorem are considered foundational in mathematical logic.

The modern approach seems to be, usually, to interpret a "model" specifically as a set in some other (typically first-order) "set metatheory." So when we talk about a model of PA, for instance, we typically mean that we are formalizing it as a subtheory of something like first-order ZFC. Models of ZFC can be formalized in stronger set theories, such as those obtained by adding large cardinals, etc.

But when Godel proved that a first-order sentence has a finite proof if and only if it holds in every "model" -- what was he talking about? Likewise, how can we understand the Löwenheim-Skolem theorem if models didn't even exist at the time?

It is clear that these researchers were not talking about using first-order ZFC as a metatheory, as that theory didn't even gain popularity until after Cohen's work on forcing in the 60s. Likewise, NBG set theory had not yet been formalized. And yet, they were obviously talking about something. Did they have a different notion of semantics than the modern set-theoretic one?

In closing, two questions:

1. In general, how did early researchers (let's say pre-Cohen) formalize semantic concepts such as these?
2. Have any of these original works been translated into English, just to see directly how they treated semantics?
• This is tangential and doesn't answer the main question, but I wanted to remark the discussion of models of ZFC can be fully done in ZFC itself - we won't be able to prove that they exist, but we can still formulate results like "if ZFC is consistent it has a countable model". Apr 15, 2018 at 22:03

I don’t know the history well enough for a full answer, but here is a partial answer, on the mathematical aspects. When you write:

It is clear that these researchers were not talking about using first-order ZFC as a metatheory […] And yet they were obviously talking about something. Did they have a different notion of semantics than the modern set-theoretic one?

and

The modern approach seems to be, usually, to interpret a "model" specifically as a set in some other (typically first-order) "set metatheory."

you seem to be following a somewhat common misconception: that one can’t do set-based semantics without having some set theory in mind as a metatheory.

But this isn’t the case! The fundamental definition of a (Tarskian) model is just as a set with certain extra structure — just like a group, or a ring, or similar. Not “a set in ZFC”, or “a set in NBG”, but just a set, which we can then reason about using whatever techniques and principles we use for mathematical reasoning in general.

Of course, in that reasoning, we’re likely to follow some established principles, like those justified by ZFC or NBG or some other specific theory. (Historically, such foundational theories were developed exactly to try to codify/justify the principles generally used and accepted.) And logicians are, for a variety of reasons, more likely than other mathematicians to be explicit about what principles they’re following in a particular piece of work. But fundamentally, you don’t need an explicit set-theoretic metatheory to study set-based semantics, any more than you need one to study groups or rings or Riemann surfaces.

As I said, I’m not especially well-read historically, but from the papers I’ve read from that period, my impression is mostly that most researchers in the period were using the modern (Tarskian) notion of semantics, and that some authors wrote explicitly about what sort of metatheory they were using, while others didn’t. But the lack of an explicit metatheory is not any failure of rigour or clarity in their notion of models — it’s normal mathematical practice, certainly of the time and at least arguably of today as well.

• I get the thinking that we don't need the entire machinery of set theory just to talk about a "set of objects." Or, at the least, we could maybe treat it like we're using a tiny, minimalist fragment of set theory. The problem is, you get these heavyweight set-theoretic notions thrown around: for instance, when we talk about the "cardinality" of a model, as in the case of the Löwenheim-Skolem theorem. What is a "cardinal?" I don't know exactly how much set theory is needed to formalize the notion of a "cardinal," but it would seem that we've already gotten to a non-trivial amount. Apr 15, 2018 at 23:34
• I agree with (and upvoted) this answer, but I'd phrase one part of it a bit differently. I'd say that Skolem, Gödel, and other early mathematical logicians worked in a metatheory, namely ordinary mathematics. They discused models in the same "meta"theory in which others discussed analytic functions or Galois groups. Note that "meta" isn't a special property of a theory, it just means that it's not necessarily the same as the object theory under discussion, so it "meta-ness" doesn't show up (and therefore isn't mentioned) in areas that don't discuss object theories. Apr 16, 2018 at 0:58
• @MikeBattaglia: If I remember right, Cantor introduces cardinality (which he called Potenz, i.e. power) by saying two sets have the same power if they can be put in 1-to-1 correspondence. So in modern terms, he’s implicitly defining cardinalities as the quotient of the class of sets by the “equipotence” relation; and in a modern treatment, general class quotients constructed by Scott’s trick do indeed take a bit of machinery. But historically, it’s not about a set theory or a fragment of one in the modern sense; it’s that he was admitting such quotients as a principle of reasoning. Apr 16, 2018 at 7:54

Peter LeFanu Lumsdaine has correctly remarked that one need not specify a precise set-theoretic metatheory in order to prove something like the completeness theorem. This remark is borne out if we look at, for example, Gödel's original papers.

Gödel's collected works have been published by Oxford University Press, and English translations are included. Regarding the completeness theorem, which was first published in "Über die Vollständigkeit des Loikkalküls," he makes the following remarks:

In conclusion, let me make a remark about the means of proof used in what follows. Concerning them, no restriction whatsoever has been made. In particular, essential use is made of the principle of the excluded middle for infinite collections (the nondenumerable infinite, however, is not used in the main proof).

He then goes into a rather extended defense of his decision to use the law of the excluded middle in his proof. Note in particular that he does not give a careful definition of the "metatheory" in which he is working.

In his famous 1931 paper on the incompleteness theorem, Gödel starts off by mentioning both Principia Mathematica (PM) and Zermelo–Fraenkel set theory, but soon narrows his focus to PM. He does mention that all the syntactic concepts that he uses in his proof are expressible within the system PM, but he does not belabor this point. After the main argument, he remarks that the proof is intuitionistically valid. Again, there is no precise description of the "metatheory" in which he is working.

• It is worth noting that in footnote 4 Gödel says : "To be more precise, we should say "valid in every domain of individuals", which, according to well-known theorems [alluding to Skolem-Löwenheim resusts], means the same as "valid in the denumerable domain of individuals"." Apr 16, 2018 at 11:29
• Also, in the fundamental proof, he says : "it follows by familiar arguments" alluding apparently to König's infinity lemma (1926). Apr 16, 2018 at 11:31

To address the main question about Gödel's original proof of the completeness theorem, which as Timothy Chow explains can be found in Gödel's Collected Works, he is using the notion of “Erfüllungssystem”, which means something like "satisfactory system". It is a structure intended to satisfy a formula $\phi$ that is not refutable (i.e., such that $\neg \phi$ is not provable), whose underlying set is the natural numbers. He then extends his theorem for countable theories proving the compactness theorem.

The structure is built as what we would now call a filtered colimit of a countable chain of finite structures. This is done through the use of König's lemma, by first building a finitely branching tree of finite structures with the property that the there are structures at any finite level and the satisfaction in a given structure at level $n$ restricts to the satisfaction at the immediate predecessor. Then there is a cofinal branch through which he builds the model of $\phi$ on the structure given by the natural numbers.

It is worth mentioning that as an immediate consequence of his proof he gets the downward Löwenheim-Skolem theorem, since he builds a model on the structure whose underlying set is the natural numbers for any countable set of satisfiable formulas. Löwenheim's original "proof" had actually some flaws which later Skolem fixed.

• Yes. In the language of reverse mathematics, Gödel's completeness theorem for countable theories is provable in WKL$_0$. See also mathoverflow.net/questions/24874/… Apr 16, 2018 at 14:51
• Thanks, this actually helped a lot. So his underlying set is the natural numbers. Is this a similar approach to what he did with PA for his incompleteness theorem then? Intuitively, the Godel numbering system is sort of like him creating a "model" of PA within PA itself, except he's encoding things as numbers instead of sets. Regardless, the main concepts seem to still apply, so perhaps that is what he is doing here. Apr 18, 2018 at 1:43
• @MikeBattaglia In the incompleteness theorems he's encoding the metatheory within PA itself. Apr 18, 2018 at 11:50

As Andreas Blass pointed out, the meta-theory can be ordinary mathematics, at least in theory. In practice, without an explicit meta-theory, authority figures decide what is allowed, and what not. Tarski (like Cantor before him) learned this lesson the hard way, as can be read in accounts of Tarski's theorem about choice from 1924:

... when he tried to publish the theorem in Comptes Rendus de l'Académie des Sciences Paris, Fréchet and Lebesgue refused to present it. Fréchet wrote that an implication between two well known propositions is not a new result. Lebesgue wrote that an implication between two false propositions is of no interest.

It is no surprise that the modern notion of model and meta-theory are due to Tarski (and his colleague Robert Vaught) from 1956. But Tarksi already presented a "non-modern" notion of meta-theory in 1933, see the SEP entry on Tarski's Truth Definitions.

The issue is a little bit complex, but here is my own summary of the difference between those two notions for a start:

If I understood it correctly, for the 1933 version, the model (i.e. the algebraic structure about which we talk) is part of the meta-language and not mentioned separately. The assignment of objects to variables on the other hand is what can satisfy a given formula. A formula is (defined to be) true if it is satisfied by all possible assignments of objects to variables.

The 1956 version is treated less explicitly in the linked SEP entry, but it is hinted at that the model is no longer an implicit part of the meta-language, but an explicit object from set-theory. A model can satisfy a given formula (or sentence), similar to how an "assignment of objects to variables" could satisfy a given formula for the 1933 version. But the text also hints that the 1956 now relies stronger on an underlying set-theory, while the 1933 explicitly tried to minimize "the set-theoretic requirements of the truth definition".