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

  • 11
    $\begingroup$ Set theorists are often very careful not to specify the metatheory that they work in. For example, Kunen writes "The metatheory consists of what is really true." (1980, p.7, his emphasis) as part of a longer explanation. Try to figure out what axiomatic theory that is! His goal is to avoid having to pin himself down - he wants the reader to be able to insert their own metatheory on top of his exposition. $\endgroup$ Sep 3 '16 at 20:00
  • 9
    $\begingroup$ Regarding the second quote, I'm tempted to reply that most programmers accept that computers run machine code, but most couldn't tell you what machine code is. $\endgroup$
    – user13113
    Sep 4 '16 at 13:26
  • 4
    $\begingroup$ @Hurkyl: true enough, but programmers are not going to tell you "I use machine code" when in fact they use PHP. $\endgroup$ Sep 4 '16 at 19:50
  • 5
    $\begingroup$ Is this question about worries that "we use set theory to study set theory"? We use the English language to study the English language, we use our brains to think about our brains, so a priori there does not seem to be a problem. $\endgroup$ Sep 5 '16 at 7:52

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.

  • 19
    $\begingroup$ Just to second this, in my book Forcing for Mathematicians I explicitly use PA as the metatheory. $\endgroup$
    – Nik Weaver
    Sep 3 '16 at 23:30
  • 12
    $\begingroup$ Although weak theories suffice to prove the relative consistency results that are often proved by talking about models of set theory, they don't let you talk about models of set theory directly. The OP's wording of the question, "when set theorists talk about models of ZFC, are they using an informal set theory as their meta-theory?" suggests that (s)he is interested in our direct talk about models of ZFC rather than in the finitary (or almost finitary) arguments that could replace this direct talk for the purpose of relative consistency results. $\endgroup$ Sep 4 '16 at 4:44
  • 7
    $\begingroup$ @AndreasBlass: indeed, the approach I use in my book is to define a system ZFC${}^+$ (roughly, ZFC + "there is a countable model of ZFC") in which one can reason about models of ZFC. Then we prove in PA that if ZFC${}^+$ proves there is a model of ZFC + $\phi$ then Con(ZFC) $\Rightarrow$ Con(ZFC + $\phi$). So the relative consistency results are proven in the metatheory, in PA, but the bulk of the argumentation takes place in the auxiliary system ZFC${}^+$. $\endgroup$
    – Nik Weaver
    Sep 4 '16 at 5:13
  • 1
    $\begingroup$ @Prof. Hamkins: What is the weakest arithmetic theory that would suffice for "the meta-theory of most set-theoretic meta-mathematical arguments"? $\endgroup$ Oct 1 '16 at 1:53
  • 5
    $\begingroup$ Oh, while I recognize that a weak meta-theory suffices for all the usual arguments, my own practice is not particularly focussed on a weak meta-theory. I feel free to assume whatever it might take in the meta-theory to push an argument through. My fuller view is that the theory/meta-theory dichotomy is a little misguided, and what we really have is a hierarchy of theories, each of which provides a meta-theoretic context for the theories that it can speak about. In semantic terms, every universe in the multiverse provides a set-theoretic background for the theories available there. $\endgroup$ Nov 22 '16 at 12:50

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.

  • 7
    $\begingroup$ A very nice answer, but I think the historical bit about ZFC making it possible to show that consistency of mathematics cannot be proved mathematically, that's not right. Gödel specifically refers to Russell and Whitehead's type theory. So it was type theory which set the stage for Gödel's incompleteness theorems. Does Gödel also mention set theory in his paper? $\endgroup$ Sep 4 '16 at 20:01
  • 2
    $\begingroup$ @AndrejBauer: The full title of Godel's incompleteness paper is "On formally undecidable propositions of Principia Mathematica and related systems I". I read that he planned to write a "part II" which would address set theory, but because of the massive rapid acceptance of the first paper he decided it was unnecessary. $\endgroup$
    – Nik Weaver
    Sep 4 '16 at 20:17
  • $\begingroup$ Actually, if I recall correctly he more or less says this in the paper. $\endgroup$
    – Nik Weaver
    Sep 4 '16 at 20:21
  • 4
    $\begingroup$ @AndrejBauer : I chose vague phrasing intentionally. The statement that "the consistency of mathematics cannot be proved mathematically" is not exactly the same as Goedel's 2nd incompleteness theorem. First of all, "the consistency of mathematics cannot be proved mathematically" is not a purely mathematical claim, but even setting that aside, I think that it is Goedel's 2nd theorem as applied to ZFC that underlies most people's belief that the consistency of mathematics cannot be proved mathematically, rather than Goedel's 2nd theorem as applied to Principia Mathematica. $\endgroup$ Sep 4 '16 at 20:44
  • $\begingroup$ Sure, I'm just splitting historical hairs here. $\endgroup$ Sep 5 '16 at 7:50

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.

  • 2
    $\begingroup$ Sorry several things confuse me. What do you mean by strings of symbols in real life being a metatheory? What do you mean by certain sets representing certain symbols? In particular, in what sense is the object $\exists$ a set? $\endgroup$ Sep 4 '16 at 9:47
  • 2
    $\begingroup$ @მამუკაჯიბლაძე: I don't follow your comment. Perhaps I should explain my point using PA. After formalizing PA within PA using Gödel numbering, for every $\varphi$ in the language of PA, you have two different objects: $\varphi$ and the Gödel number $\varphi$, which is a natural number. One of them is a mathematical object, the other is not. $\endgroup$
    – Burak
    Sep 4 '16 at 10:02
  • $\begingroup$ Thanks, this is a helpful analogy. Still, I don't understand what exactly your metatheory is, and how exactly you represent symbols by sets. In fact, I also do not understand which sets do you have in mind as representers of symbols - some sort of naïve sets, or sets from the already built version of ZFC or what? $\endgroup$ Sep 4 '16 at 10:09
  • 1
    $\begingroup$ Here is an example of what I have in mind: We can construct natural numbers as sets in ZFC. Then I can set the number $0$ to represent $=$, the number $1$ to represent the quantifier $\exists$, the number $2$ to represent the variable $x$, the numbers $3$ and $4$ to represent the paranthesis $($ and $)$. Then the finite sequence $(1,2,3,2,0,2,4)$ represents the sentence $\exists x (x=x)$. Notice that the finite sequence $(1,2,3,2,0,2,4)$ itself is a set. Of course, this is not the only way of doing this. Honestly, I have never tried to formalize ZFC within ZFC in full detail. $\endgroup$
    – Burak
    Sep 4 '16 at 10:17
  • 2
    $\begingroup$ @მამუკაჯიბლაძე: Yes. You can do all this encoding probably in a very weak theory of arithmetic. We don't really need any sets. The reason I insisted using ZFC is the confusion I quoted at the beginning, namely thinking that model theory using set theory precludes us from applying model theoretic techniques to set theory. I believe the whole point of this answer can be summarized as follows: Without any circular reasoning, one can build tools of mathematical logic in certain set theories and then apply these tools to (the formalized versions of) the very same set theories. $\endgroup$
    – Burak
    Sep 4 '16 at 10:49

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.