48

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

Community
  • 1
user98009
  • 489
  • 13
    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. – Carl Mummert Sep 03 '16 at 20:00
  • 9
    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. –  Sep 04 '16 at 13:26
  • 6
    @Hurkyl: true enough, but programmers are not going to tell you "I use machine code" when in fact they use PHP. – Andrej Bauer Sep 04 '16 at 19:50
  • 5
    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. – Andrej Bauer Sep 05 '16 at 07:52
  • I think it depends on the person. Without being a logician i find comforting knowing that i can work as a theorem prover generating axioms of set theory (from axiom schemas) and applying modus ponens, and reflecting about this process in a computable way, that is using something like PA ("combinatorics" and induction) when analyzing the proof process. This is usually sketchy, of course, but i like to "know" i could make it rigorous if necessary, even model it as a brain/mental process. Of course checking what (meta)theory axioms i actually use or need is interesting and sometimes difficult. – plm Aug 04 '23 at 23:00
  • Dear @CarlMummert, Thank you very much. I've often noticed that kind of vague comment from logicians -set theorists in particular. I can only understand that as due to emotional/motivational unease, because it would be much more helpful to readers to have clearly stated what is being used as metaaxioms (like axioms are usually carefully indicated). By the way what metatheory is necessary to produce the forcing proof of the consistency of $ZFC+\neg CH$ ? PA ? Less ? Any reference surveying this question, and perhaps lower-bounding the metatheory strength for some results ? – plm Aug 04 '23 at 23:18

4 Answers4

39

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.

Joel David Hamkins
  • 224,022
  • 22
    Just to second this, in my book Forcing for Mathematicians I explicitly use PA as the metatheory. – Nik Weaver Sep 03 '16 at 23:30
  • 15
    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. – Andreas Blass Sep 04 '16 at 04:44
  • 8
    @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${}^+$. – Nik Weaver Sep 04 '16 at 05:13
  • 2
    @Prof. Hamkins: What is the weakest arithmetic theory that would suffice for "the meta-theory of most set-theoretic meta-mathematical arguments"? – Thomas Benjamin Oct 01 '16 at 01:53
  • Well, that is a question for the reverse mathematics people. – Joel David Hamkins Oct 01 '16 at 13:54
  • @JoelDavidHamkins: That very well may be, but since you mentioned in your answer that "we don't really even use set theory in the metatheory but just some weak arithmetic theory", one might infer (rightly or wrongly) that you, yourself (for example) might use a weak arithmetic theory in your meta-theory of choice that is weaker than $PA$. What might that weaker arithmetic theory be? $Q$ (Robinson arithmetic)? $I$$\Delta_0$? $PRA$? (Just to name a few....) I am aware that (for example) there is a weak set theory equiconsistent(?) with $Q$, and there might be other weak set theories – Thomas Benjamin Nov 22 '16 at 12:15
  • (cont.) associated with arithmetic theories weaker than $Q$. If that's the case, then one should be able to replace the weak arithmetic theory with its associated set theory as the metatheory, and then the answer to the $OP'$ question asked in the title is "yes"--but a much weaker set theory. So I ask you, what is the weak arithmetic theory of choice you find you use as (in) your working meta-theory? – Thomas Benjamin Nov 22 '16 at 12:24
  • 5
    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. – Joel David Hamkins Nov 22 '16 at 12:50
  • @JoelDavidHamkins: Thanks for clearing that up. – Thomas Benjamin Nov 23 '16 at 01:30
  • 1
    @JoelDavidHamkins: Do you still endorse this viewpoint after your more recent work that we might call “studying the structure of the multiverse”? Last year I talked with Miha the following fact: Let M be a countable model of ZFC. There is a perfect set of pairwise non-amalgamable Cohen generic reals over M. Now I would say we’re actually using some set theory (ZC) to talk about models of ZFC. – Monroe Eskew Apr 28 '19 at 04:33
  • Thank you very much for the enlightening comments. Silly question: Can one prove stronger (un)provability results using a strong metatheory instead of a weak one ? In set theory we can prove that PA does not prove $0=1$, so the answer is yes, but what kind of (un)provability result is added when passing to a stronger theory ? Only consistency-type statements -i don't even know if there is such a thing as a "consistency-type statement" ? Any article on this topic ? – plm Aug 04 '23 at 23:53
25

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.

Timothy Chow
  • 78,129
  • 8
    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? – Andrej Bauer Sep 04 '16 at 20:01
  • 2
    @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. – Nik Weaver Sep 04 '16 at 20:17
  • Actually, if I recall correctly he more or less says this in the paper. – Nik Weaver Sep 04 '16 at 20:21
  • 4
    @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. – Timothy Chow Sep 04 '16 at 20:44
  • Sure, I'm just splitting historical hairs here. – Andrej Bauer Sep 05 '16 at 07:50
  • I know this is an old post, but I just came here via the "Related" links and have a very big objection. You wrote: "people don't seem to have any trouble recognizing mathematically correct (or incorrect) reasoning when they see it". Obviously this holds for basic mathematical reasoning, which I could define as "interpretable within ZC" (and some people don't even think AC is correct, but never mind that). However, this does not hold for any reasoning that invokes higher set theory. For example, Regularity is obviously incorrect, but that doesn't stop people from using it. [cont] – user21820 Apr 20 '21 at 05:47
  • [cont] The apparent first mathematician who came up with Regularity considered it false too, so anything using it should be stated as an assumption, or we could think of it as that we are just reasoning about well-founded models of ZC. But no, current consensus is to treat Reg as an axiom rather than assumption. Now of course you can argue that theorems of ZC+Reg are simply theorems about the well-founded sets, and thus we can recover correct mathematics regardless of whether Reg holds in general. But this does not apply to Replacement, whose soundness is a little dubious. [cont] – user21820 Apr 20 '21 at 05:55
  • [cont] The point is that mathematical reasoning that employs higher set-theoretic assumptions are not clearly recognizable as correct in any objective sense. ZFC is not merely a collation of assumptions that are felt to be true, but is actually a social construct that provides an elegant axiomatization of what set theorists want to use, which is also strictly more than what ordinary mathematicians want to use. – user21820 Apr 20 '21 at 06:03
  • @user21820 I don't see why you call this an "objection." My main point was that there is nothing mysterious about the term "correct reasoning." It seems to me that you tacitly agree. For you to reject (say) Regularity on the grounds that it is not correct, presupposes that you know what it means for something to be correct or not correct. I am not insisting that everyone agree on exactly what constitutes correct reasoning, only that the concept of correct reasoning makes sense. – Timothy Chow Apr 20 '21 at 09:17
  • Ah ok so there is some misunderstanding in both directions. I personally do not presuppose that Regularity is false, because when it comes to higher set theory there could be not just "true" and "false" but also "meaningless". I do agree with you that the concept of "correct reasoning" makes sense, and I think I misread you as claiming that there is a shared agreement on "correctness". But then the argument that people should not be uncomfortable with the term "correctness" is unjustified, since it is subjective. In contrast, "can be formalized in formal system S" is an objective claim. – user21820 Apr 20 '21 at 12:23
  • @user21820 Here we do perhaps have a slight disagreement, because I believe that "can be formalized in formal system S" is also subjective, just to a lesser degree than "the proof of Fermat's Last Theorem is correct" is. – Timothy Chow Apr 20 '21 at 13:25
  • I should be more precise. For any reasonable S, "S proves Q" is an arithmetical sentence simple enough that I believe it has an objective truth-value, and that is what I meant by "objective claim". Whether or not we are able to justify that claim might be subjective, sure. I don't know what exactly you mean by "the proof of FLT is correct", but I suppose I would agree with whatever you meant there. – user21820 Apr 20 '21 at 14:08
  • @user21820 Sure, I know what you're claiming. I'm just saying that I believe that even "S0 + S0 = SS0 is a theorem of PA" is somewhat subjective. It relies on some kind of understanding of symbols and rules which might differ slightly from one person to another. We can't look inside each other's internal conscious states. For practical purposes, that doesn't matter, but what I maintain is that there remains some degree of subjectivity. In particular I don't believe that strict formalism is philosophically privileged as "completely objective". – Timothy Chow Apr 20 '21 at 14:15
  • That's interesting... I'm not averse to that kind of extreme skepticism of real-world embedding of natural numbers, on which complete objectivity regarding provability must rest, but I wasn't aware that you were one of those skeptics. While I believe that there is no real-world embedding (see here), I usually put that issue one side when talking to people. =P – user21820 Apr 20 '21 at 15:03
14

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.

Burak
  • 4,135
  • 2
    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? – მამუკა ჯიბლაძე Sep 04 '16 at 09:47
  • 2
    @მამუკაჯიბლაძე: 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. – Burak Sep 04 '16 at 10:02
  • 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? – მამუკა ჯიბლაძე Sep 04 '16 at 10:09
  • 1
    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. – Burak Sep 04 '16 at 10:17
  • Aha. Do I understand correctly that when you say you represent symbols and string of symbols by sets, you mean sets in a very undemanding fragment of your ZFC, just enough to give meaning to encodings of symbols and their finite strings? – მამუკა ჯიბლაძე Sep 04 '16 at 10:40
  • 2
    @მამუკაჯიბლაძე: 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. – Burak Sep 04 '16 at 10:49
  • Thanks, now I understand. Except I still do not understand what your metatheory is. – მამუკა ჯიბლაძე Sep 04 '16 at 10:58
0

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.

Censi LI
  • 403