Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?

Question

Here, Noah Schweber writes the following:

Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively obvious" without comment. This is true even when it looks like we're being rigorous: for example, when we formally define the real numbers in a real analysis class (by Cauchy sequences, Dedekind cuts, or however), we (usually) don't set forth a list of axioms of set theory which we're using to do this. The reason is, that the facts about sets which we need seem to be utterly tame: for example, that the intersection of two sets is again a set.

A similar view is expressed by Professor Andrej Bauer in his answer to the question about the justification of the use of the concept of set in model theory (here is the link, I can really recommend reading this answer). See also this answer. There he writes:

"Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets." This is what mathematicians say, but most cannot even tell you what ZFC is. Mathematicians work at a more intuitive and informal manner.

Now we know that in ordinary mathematics (including model theory), one uses informal set theory. But what about set theory itself?

So now I wonder: When set-theorists talk about models of ZFC, are they using an informal set theory as their meta-theory? Is the purpose of ZFC to be used by set-theorists as a framework in which they reason about sets or is the purpose of ZFC to give a object theory so that we can ge an exact definition of what a "set-theoretic universe" is (namely, it is a model of ZFC)?

Answer 1

The main fact is that a very weak meta-theory typically suffices, for theorems about models of set theory. Indeed, for almost all of the meta-mathematical results in set theory with which I am familiar, using only PA or considerably less in the meta-theory is more than sufficient.

Consider a typical forcing argument. Even though set theorists consider ZFC plus large cardinals, supercompact cardinals and extendible cardinals and more — very strong object theories — they need very little in the meta-theory to undertake the relative consistency proofs they have in mind. To show for example that the consistency of ZFC plus a supercompact cardinal implies the consistency of ZFC plus PFA, there is a forcing argument involved, the Baumgartner forcing. But the meta-theory does not need to undertake the forcing itself, but only to prove that forcing over an already-given model of ZFC plus a supercompact cardinal works as described. And that can be proved in a very weak theory such as PA or even much weaker.

So we don't really even use set theory in the meta-theory but just some weak arithmetic theory. I expect that the proof theorists can likely tell you much weaker theories than PA that suffice for the meta-theory of most set-theoretic meta-mathematical arguments.

Answer 2

You asked:

When set-theorists talk about models of ZFC, are they using an informal set theory as their meta-theory?

The short answer is yes. A set theorist is doing mathematics and hence is reasoning informally, just like any other mathematician.

It's important, at least when you're first wrapping your mind around these concepts, to distinguish between formal reasoning and informal reasoning that can be formalized. Formal reasoning consists of formal proofs in some formal system. Informal reasoning includes everything that you encounter in a human-readable mathematical text. Even when you read in a book a claim that "we work in ZFC" or "we work in PA", what you will find in the rest of the text is not a bunch of formal strings, but rather human-readable text written in some natural language like English. What is meant by claims that "the metatheory is PA" is that all the subsequent meta-theoretic reasoning can be formalized in the first-order language of arithmetic and appealing only to the axioms of PA.

Of course, the main reason for informal reasoning is that purely formal reasoning is, except in extremely simple cases, indigestible by human readers. Additionally, in many cases, it isn't particularly important that everything in the rest of the text can be formalized in a specific formal system; what we usually care about is that the reasoning is correct, and that, if necessary, it could be formalized in some well-known formal system. One advantage of leaving the reasoning informal is that the decision as to how exactly to formalize the argument is deferred until that question actually needs to be answered; if you like, it's a form of lazy evaluation.

Occasionally, people squirm when they hear talk about "correct reasoning" without any specification of a formal system. I'm not sure exactly why this discomfort arises. In any other area of mathematics, people don't seem to have any trouble recognizing mathematically correct (or incorrect) reasoning when they see it, even though no formal system is specified. It's only when the subject matter is set theory or logic that some people squirm. Perhaps it's because set theory and logic are perceived to be subjects that are supposed to provide absolute rigor to mathematics and eliminate the need for informal reasoning. It's true that the mathematical community's collective experience has shown that any correct mathematical argument can be formalized in one of a short list of formal systems, but ultimately, we have to rely on the ability of mathematicians to distinguish correct arguments from incorrect ones in order to ascertain which formal systems are appropriate foundations for mathematics and which are not. Furthermore, informal judgment needs to be applied to verify that a particular formalization accurately represents a given informal argument. In this sense, informal reasoning is not entirely eliminable, and one should not expect to be able to entirely dispense with one's ability to recognize correct informal mathematical argumentation.

Is the purpose of ZFC to be used by set-theorists as a framework in which they reason about sets or is the purpose of ZFC to give a object theory so that we can ge an exact definition of what a "set-theoretic universe" is (namely, it is a model of ZFC)?

Different purposes are possible. Set theorists may, for example, study ZFC as an interesting mathematical object in its own right, without caring about its role in the foundations of mathematics.

Of course, historically, ZFC has played an important role in the foundation of mathematics. It furnished an "existence proof": There exists a formal axiomatization of set theory such that all mathematical reasoning can be formalized in it. This "existence proof" then set the stage for later developments such as the "proof" that the consistency of mathematics cannot be proved mathematically—a development that was made possible only because ZFC was specified precisely enough that one could prove theorems about it. And as you suggest, ZFC is a candidate if you want to formalize your meta-theoretic reasoning (though as others have noted, it is typically massive overkill to do so).

So the answer to your question is that yes, ZFC can serve the purposes that you mention, though I would emphasize that those are not the only reasons that set theorists find it interesting.

Answer 3

I am writing this not only as an answer to your question, but also to some questions that were linked in your question. There seems to be a bunch of questions on MO that essentially ask the same thing: "Model theory is using concepts of set theory, set theory is using concepts of model theory. Is set theory, which is claimed to be the foundation of mathematics, based on circular reasoning?"

The short answer is no. I believe mathematicians who are not logicians and who confuse themselves with such questions simply want to see how tools in set theory and model theory are "built hierarchically". I am not claiming that all logicians perceive logic the way I am about to describe, but here is an approach:

I have an intuitive understanding of objects of first-order logic, i.e. quantifiers, variables, connectives etc. I also have an intuitive understanding of the concept of a set. I start listing down some axioms, namely the axioms of ZFC. Here I am using boldface letters to denote that these axioms are strings of symbols in real life. (This is going to be my metatheory.)

As I have an intuitive understanding of rules of first-order logic, I can start manipulating symbols and prove theorems. Recall that I had an intuitive understanding of the concept of a set and I chose my axioms to represent the picture I have in mind.

At some point, I realize that, using sets, I can formalize the intuitive notions I have. For example, I can choose certain sets to represent certain symbols and then other certain sets will represent certain strings and certain sets of strings. In this way, I can talk about $ZFC$ which is the set that represent the axioms of ZFC.

For example, I can define the (Tarskian) truth predicate as is defined in many model theory books. If you read this inductive definition, you will see that, for example, a sentence $\exists x \phi(x)$ is true in some structure $M$ if there exists $m \in M$ such that $\phi(m)$ is true in $M$. Here, the object $\exists$ is the set that I chose to represent my existential quantifiers whereas the object there exists is the symbol in real life that I use for existential quantifiers.

After a long and painful procedure, I can formalize all notions of model theory in ZFC. Then I can apply these tools to $ZFC$ to prove theorems of the form $Con(ZFC) \rightarrow Con(ZFC+CH)$ using axioms of ZFC.

All that being said, you do not have to choose your metatheory to be ZFC. As Joel pointed out, much weaker theories may suffice depending on what you want to prove.

You may already be aware of all of these. Perhaps you were only using the word "informal" to mean that axioms of ZFC are not formal objects as sets. The only reason I wrote this answer is that your use of the phrase "informal set theory as their meta theory" reminded me of the confusion that I quoted at the beginning and created the impression that there is something wrong with ZFC.

Answer 4

When we talk about models of a theory, say, $P$, I think $P$ is regarded as object to be studied, while ZFC is the theory we use to study $P$ but not the metatheory. Here metatheory should mean that which we take for granted in order to understand and do reasoning in ZFC (that is, the theory which syntactic ZFC theory must rest on), which most would agree Peano Arithmetic theory, or even Primitive Recursive Arithmetic is sufficient. Likely, when we talk about models of ZFC, that is, when $P$ happens to be ZFC, then we should think that ZFC serves both as object to be studied and the theory used for studying things, while it is still Peano Arithmetic that serves as metatheory.