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?



What "metatheory" did early set theory/logic researchers use to prove semantic results?
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.


