21

In the thread Set theories without "junk" theorems?, Blass describes the theory T in which mathematicians generally reason as follows:

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

Question: If set theorists just want to do set theory and not worry about foundations (and encodings of mathematical objects as sets), do they also work in the theory T? Or are they always regarding every object as a set?

Also, do I understand it correctly that it's hard to actually formalize the syntax of the theory T, because of the many types and connotations of natural language involved? But then, what's "first-order" about T, if T is communicated through natural language?

Community
  • 1
user100315
  • 221
  • You should add a reflexive transitive closure to your theory T, otherwise it won't work. This part of my research. If you have a first order many sorted logic, you need sometjng that "loops". – Lucas K. Oct 26 '16 at 21:27
  • 9
    No, but they usually have some while discussing GCH (worst math joke ever?) – guest Oct 27 '16 at 00:46
  • 4
    Another joke -- yes they work in T, the modal logic with axiom $\Box A\rightarrow A $, since forcing implies truth... – Bjørn Kjos-Hanssen Oct 27 '16 at 07:45
  • If set theorists just want to do set theory and not worry about foundations My impression is that there is essentially no research done by set theorists that is not about foundations. Am I wrong? –  Oct 27 '16 at 15:38
  • 2
    I'd say very little of what set theorists do is actually about foundations, unless you understand "foundations" in a very broad sense (for example, when a set theorist proves that certain open problem from another area of mathematics is undecidable in $\mathsf{ZFC}$, that doesn't count as "foundations" to me)... – David Fernandez-Breton Oct 27 '16 at 17:23
  • 2
    @DavidFernandezBreton Really? My view is that such a result would be a very welcome result in foundations. What counts as foundations for you, if not that? – Joel David Hamkins Oct 27 '16 at 21:22
  • 2
    @JoelDavidHamkins , for me "foundations" denotes more the purely "philosophical" reflection about whether, for example, $\mathsf{ZFC}$ is an appropriate system to work as the foundations of math, or whether our definition of "natural number" agrees with some pre-existent intuitive notion of number, and so on. The moment you prove a theorem about something like abelian groups (even if such a theorem is an independence result), you're no longer doing foundations of math: you're doing math. (this is just part 1 of the comment) – David Fernandez-Breton Oct 28 '16 at 14:00
  • 1
    (part 2 of the comment above) It is still the case, of course, that something like an independence result in abelian group theory might shed light in a particular foundational issue, and so it might be relevant for the foundations, but the result itself is math, not foundations of math. – David Fernandez-Breton Oct 28 '16 at 14:02
  • 1
    (separate comment) In any case, going back to @BenCrowell's question, even if you want to include independence results as a subset of "foundations", there's still lots of other stuff that set theorists do. For example, proving a Ramsey-theoretic result in $\mathsf{ZFC}$ is something that a set theorist might do, and I find it really hard to classify a statement of this sort as "foundations", it seems to be more "pure combinatorics" (although infinitary rather than finitary). – David Fernandez-Breton Oct 28 '16 at 14:05
  • @DavidFernandezBreton It seems that you use the word much more narrowly than most people working in foundations. It seems that for some reason you want the intersection of foundations and mathematics to be empty, whereas a more nuanced view recognizes that many mathematical results, including many independence results, have a foundational significance. See also my answer here: http://mathoverflow.net/questions/172838/metan-th-mathematics/172848#172848, arguing that there is no crisp distinction between mathematics and meta-mathematics (or foundations). – Joel David Hamkins Oct 28 '16 at 21:14
  • Since Prof. Blass states that $T$ is "many-sorted", would it be fair to say that its logic would be V$\ddot a$$\ddot a$n$\ddot a$nen's "Sort Logic" (see his paper, "Sort Logic and Foundations of Mathematics", found under title on the Web)? I'm asking because if this is so, sort logic seems to provide a type of rationale for accepting the existence of large cardinals (e.g. "The LST(L$\ddot o$wenheim-Skolem-Tarski)-number for the [logic] $\Delta_2$ is the first supercompact cardinal [Thm. 3.5 in the aforementioned paper]", meaning, "LST($\Delta_2$) exists if and only if supercompact cardinals – Thomas Benjamin Oct 31 '16 at 08:50
  • (cont.) exist [ Thm. 5 of Magidor's and V$\ddot a$$\ddot a$n$\ddot a$nen's paper, "On L$\ddot o$wenheim-Skolem-Tarski numbers for extensions of first-order logic"]), the rationale being that the LST-number (for example) needs to exist in order for certain (desired?) properties of models to exist. – Thomas Benjamin Oct 31 '16 at 09:23
  • @JoelDavidHamkins after reading the answer that you linked to, I get the impression that our views are not so different from each other. You're basically saying that the boundaries between "foundations" and "math" can't be well-defined, because a lot of foundations really look like ordinary math. I seem to be saying above that, if we wanted to draw a sharp boundary between "foundations" and "math", the end result would be that the "foundations" part is a meagre set (because in a comeagre set, the foundations seem to be indistinguishable from the math itself). – David Fernandez-Breton Oct 31 '16 at 13:52
  • Well, I'm not sure I agree with that, since the main point of my answer there was that it is not sensible to "draw a sharp boundary" between foundations and mathematics, because they interact and overlap so much. In any case, most ZFC independence results are definitely part of foundations, and this is not a meager set. – Joel David Hamkins Oct 31 '16 at 15:59

2 Answers2

16

Caveat number 1: strictly speaking, no one actually works in the theory $T$, just as no one actually works in the theory $\mathsf{ZFC}$. Mathematicians work by means of carefully used natural language and not within a formal system. Formal systems are formulated as approximations that try to model what mathematicians actually do while at work. Now to address the question, with the above caveat in mind, are we always regarding every object as a set? Not necessarily always, just sometimes. The point is that $\mathsf{ZFC}$ and $T$ are bi-interpretable, so you can switch between both viewpoints at will without that changing the stuff that you can prove (and even better: both $T$ and $\mathsf{ZFC}$ are just approximations to what we actually do, so we can just do math as usual, and not worry about these nuances, and whatever it is that we're doing can in theory be translated to the formal system of your choice).

David Fernandez-Breton
  • 884
  • 2
    This sounds exactly right to me. I work in a system which I have never attempted to completely formalise, but on the other hand after the one serious course I did in logic and set theory I know that if I wanted I could break everything down to ZFC, and indeed there are a gang of people who are currently typing in theorem after theorem into Coq and hence are formally doing just this. On the other hand I know for sure that I don't care whether or not Q "is" in R, or whether Q is equivalence classes of pairs (a,b) of integers with b non-zero etc etc, and that these questions are "not math". – znt Oct 26 '16 at 22:17
  • 4
    A small detail: the people who are typing things into Coq are not using ZFC, they are using type theory. As for you not caring whether $\mathbb{Q}$ is a subset of $\mathbb{R}$, at some level you're right that you shouldn't have to care, but on another you're running the danger of an inconsistency. They used to not care whether every function can be written as a power series, they just did it. So, if you really do not want to care, you should change your preferred foundation from ZFC to one that actually lets you not care about this sort of thing. That would be Univalent Foundations. – Andrej Bauer Oct 27 '16 at 06:43
  • ZFC is consistent, so znt still doesn't need to care. – arsmath Oct 27 '16 at 11:03
  • 7
    @AndrejBauer Why do you think ZFC requires you to care about whether $\mathbb{Q}\subset\mathbb{R}$? It seems to me that ZFC is fully compatible with a structuralist perspective about such things. My impression is that set theorists generally are as structuralist about such matters as other kinds of mathematicians. – Joel David Hamkins Oct 27 '16 at 12:14
  • All standard constructions (by cuts, by metric completion, etc.) of $\mathbb{R}$ from $\mathbb{Q}$ result in $\mathbb{Q} \not\subseteq \mathbb{R}$. Therefore, if we are serious about using ZFC, whenever anybody writes $1/2 \in \mathbb{R}$ the answer is false. If we are serious about ZFC, then we should define a map $e : \mathbb{Q} \to \mathbb{R}$ and always write $e(1/2)$ when we construe $1/2$ as a real. This may seem like an irrelevant detail, but is not when you speak to computers. – Andrej Bauer Oct 27 '16 at 14:22
  • Informal mathematics operates with phrases such as "we identify $\mathbb{Q}$ with the obvious subset of $\mathbb{R}$" on the basis of which we are allowed to pretend that $1/2 \in \mathbb{Q}$ as well as $1/2 \in \mathbb{R}$. This piece of informal mathematics directly violates ZFC and it cannot be rescued easily. It is dishonest to claim that we can encode this particular piece of informal mathematics in formal ZFC. It is far from obvious that it can be done, and in fact it cannot be done. Ttraditional type theory suffers from the same problem, Univalent foundations come closer to solving it. – Andrej Bauer Oct 27 '16 at 14:29
  • 8
    I am serious about ZFC, and if I am in a structuralist mood about $\mathbb{R}$, then my theorems will state: in every complete ordered field, blah blah blah; or every complete separable dense linear order, etc., depending on what $\mathbb{R}$ means to you. There is no need to have a particular copy of $\mathbb{R}$ identified as the official reals, and this is what structuralism amounts to. The particular constructions are used to show existence only, and it is a trivial matter to build instances showing that $\mathbb{Q}\subset\mathbb{R}$ is possible, if you want it. – Joel David Hamkins Oct 27 '16 at 14:34
  • 9
    Usually, though, the structuralism goes without saying, and so one asserts a theorem about $\mathbb{R}$, with the understanding that it doesn't matter which copy of $\mathbb{R}$ you use. (In some very rare cases, it may matter---for example, if one is paying attention to interaction with the cumulative hiearchy---and in those cases one will say a little more about the requirements of the situation.) This happens also in category theory, for example, where one may want to use a copy of $\mathbb{R}$ that is available in the current universe that has been fixed, rather than arising above it. – Joel David Hamkins Oct 27 '16 at 14:42
  • 1
    Let's drive your point a bit further: it is in fact necessary that you take the structuralist position and state your theorems so that they apply to all copies of "complete ordered fields" that exist in ZFC. This is precisely what prevents "accidental theorems" which hold because of the particularities of some specific encoding. But by doing so we robbed ZFC of being the foundation! It has been relegated to some background theory whose only purpose is to guarantee consistency and the occasional existence. The relevant foundation is some form of structuralism and it completely obscures ZFC. – Andrej Bauer Oct 27 '16 at 19:38
  • 3
    I don't agree with that---rather, my view is that the structuralist viewpoint is simply undertaken within ZFC itself. We become structuralist in preferring statements of the form, "All copies of $\mathbb{R}$ have such-and-such relation to their rational numbers etc.". But there seems to be no issue about formalizing such statements in ZFC. – Joel David Hamkins Oct 27 '16 at 20:19
  • 5
    I view the structuralist part of the foundation as the easy part, in that it can be implemented in a high level language, simply by preferring certains kinds of theorems. Meanwhile, the value of ZFC as a foundation is the simplicity and clarity of the most fundamental existence assumptions, free of the meta-theory and mass of defined terms that often seem to complicate alternative foundations. In my opinion, this is why set-theory has led to such a successful and clarifying meta-foundational program, via forcing and large cardinals. – Joel David Hamkins Oct 27 '16 at 20:45
  • You can identify both the rationals and the reals as a subset of the surreal numbers, in which case $\mathbb Q \subset \mathbb R$. – Christopher King Feb 20 '24 at 19:51
12

You address your question to set theorists, and so let me answer as a set theorist that, yes, when I think purely as a set theorist, then indeed the idea that every object is a set just goes without saying — it is a basic elementary part of the ZFC conceptual framework. One needn't ever even remark on this in an argument made to other set theorists.

For example, the cumulative $V_\alpha$ hierarchy provides an extremely rich structural background for the set-theoretic universe, which is especially informative and helpful in the analysis of various set-theoretic axioms, especially the large cardinal axioms that reach very high into this hierarchy. The picture of all objects existing as sets in the cumulative hierarchy is basically pervasive in set-theoretic arguments, and is definitely a fundamental part of the set-theoretic understanding of the mathematical universe. One may freely carry out an argument by $\in$-induction, for example, concluding that every object $x$ has a certain property, although really what one has proved is that every well-founded set has the property. In this sense, I would say that when set theorists are operating as set theorists amongst set theorists, they are not usually operating in the theory T described by Andreas, but rather in something much closer to ZFC, in a language expanded by concepts that have been defined in set theory. (As David mentioned, esentially no mathematician, including set theorists, works in a purely formal system.)

Meanwhile, however, this doesn't mean that set-theorists don't make use of type-theoretic concepts. For example, set theorists have diverse concepts of what counts as a real number, and one can commonly find various real-number concepts used in set theory, including: an element of Cantor space $r\in 2^\omega$; a subset of the natural numbers $r\subseteq\omega$; an element of Baire space $r\in \omega^\omega$; and so on. Often the algebraic field-theoretic structure of the reals is less important or relevant to set-theoretic concerns, and set theorists typically care about real numbers as: a package containing countably much information. In many set-theoretic contexts, it doesn't matter which particular real-number concept one is using, and in this sense talk about the reals reduces essentially to the use of a real-number type.

Finally, however, when set theorists communicate with other mathematicians, then of course they are naturally able to communicate in something much closer to the theory $T$ that you mentioned.

user21820
  • 2,733
Joel David Hamkins
  • 224,022
  • 2
    I'd say that the set theorist's theory $T$ has a sort for classes because classes arise as mathematical concepts in set-theoretic arguments. – Andrej Bauer Oct 27 '16 at 06:46
  • 1
    To add a concrete example: one workhorse method which relies fundamentally on the “everything is built out of sets” framework is the presentation of forcing using names (or Boolean-valued sets, etc.). One can do forcing-type arguments in a more $T$-like setting, using sheaves; but I’ve never seen that approach taken in mainstream set theory. – Peter LeFanu Lumsdaine Oct 27 '16 at 09:28
  • 1
    @AndrejBauer Yes, set theorists do often work in theories with a sort for classes, and this is completely explicit, for example, in Gödel-Bernays set theory and in Kelley-Morse set theory. In this sense, the class sort is not really a part of the informal theory $T$, but present explicitly in the formal theories GBC and KM and the various intermediate theories such as ETR. Set theorists are usually quite explicit about their background theory regarding classes, and one could replace ZFC in my answer with GBC or KM in the two-sorted second-order language of set theory. – Joel David Hamkins Oct 27 '16 at 11:44
  • Joel, What is ETR? – Bob Solovay Nov 02 '16 at 01:54
  • ETR is the theory of Elementary Transfinite Recursion. This extends GBC set theory with an axiom that asserts of every well-founded class relation and recursion rule that there is a solution of the recursion. Vika Gitman and I have proved that this is exactly equivalent over GBC to the principle of open determinacy for class games, and you can see our paper at: http://jdh.hamkins.org/open-determinacy-for-class-games/ (click through to the arxiv for pdf). – Joel David Hamkins Nov 02 '16 at 02:12
  • Sorry, I should have said that we proved ETR is equivalent to clopen determinacy for class games. This is something analogous to Steel's dissertation result that clopen determinacy for games on $\omega$ is equivalent in reverse mathematics to $\text{ATR}_0$. The intriguing thing is that he also gets open determinacy in that context, but for proper class games over GBC, it turns out that open determinacy is strictly stronger. – Joel David Hamkins Nov 03 '16 at 16:23
  • 4
    Regarding the edit by user218210, I think my original ${}^\omega 2$ and ${}^\omega\omega$ is standard notation for the function spaces. The right-side exponentation $2^\omega$ and $\omega^\omega$ can be ambiguous because they might also refer to the cardinal or ordinal, instead of the space of sequences. But I didn't roll it back... – Joel David Hamkins Apr 21 '21 at 10:07
  • Please roll it back if you prefer your original! I knew that the more common notation is ambiguous, but I thought it was completely disambiguated by your surrounding phrasing. =) – user21820 May 24 '22 at 17:31