Skip to main content
3 of 4
added 8 characters in body
Mike Battaglia
  • 4.9k
  • 19
  • 44

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, and 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 hadn't even gained 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 directly see how they treated semantics?
Mike Battaglia
  • 4.9k
  • 19
  • 44