15

This is a followup question to Does foundation/regularity have any categorical/structural consequences, in ZF?

As shown in answers to that question, the axiom of foundation (AF, aka regularity) has consequences over ZF–AF that can be formulated purely in structural terms (i.e. using sets only in ways that respect isomorphism).

In particular, it implies the statement “Every set can be embedded into a set equipped with a well-founded extensional relation”, which Mike Shulman has called the axiom of well-founded materialisation; and (by the arguments in that question) this axiom should have the same structural consequences as foundation.

This statement is a very mathematically reasonable one. However, I don’t think I have ever seen this or anything similar appearing in practice in ordinary mathematics — only in logical investigations like this one, where it occurs specifically because of its relation to AF. So my question here is: Does the axiom of foundation have any consequences (over ZF–AF) that have appeared in ordinary mathematics?

Slightly more precisely:

  • By “consequence of foundation over ZF–AF”, I of course mean principally a statement that’s provable in ZF, but not in ZF–AF. But I’d also be interested in e.g. a proof in ZF that doesn’t go through in ZF–AF and can’t be trivially modified to do so.

  • By “ordinary mathematics”, I mean… this of course is subjective, and mostly I think “we know it when we see it”, and hope that most of us will find our judgement on it mostly agrees. But to articulate my own intent here a little: a sufficient (but not necessary) condition to would be that the statement has been considered in a field of mathematics other than logic; necessary conditions would be that it’s purely structural, and that it’s been considered outside work specifically investigating foundation (or related axioms) or modelling set theories that include foundation. To illustrate the non-necessity of the “outside logic” criterion — I would certainly be happy to consider consequences in e.g. general classical model theory.

See e.g. Where in ordinary math do we need unbounded separation and replacement? for a similar question, about different axioms, and relevant discussion of what should be considered “ordinary mathematics”.

Peter LeFanu Lumsdaine
  • 18,946
  • 3
    How would one give evidence that the answer is "there are no such consequences"? I suppose we could try to prove a meta-theorem. – Andrej Bauer May 30 '18 at 16:56
  • 3
    Would this be sufficiently "ordinary": That existence of a tree without a branch implies the existence of such a tree with a linear order on each rank? – Elliot Glazer May 30 '18 at 19:10
  • 1
    @Elliott: if you've seen that statement (or something roughly the same) considered in an "ordinary mathematical" context — i.e. with where the main motivations weren't studying the strength of axioms of set theory or similar — then yes, I would! But I really do mean "are there consequences that have been considered in ordinary maths?", not "can you find consequences that look like something that might be considered in ordinary maths?" (the answers to my previous question already do that quite well, I think). – Peter LeFanu Lumsdaine May 30 '18 at 20:38
  • 1
    @Andrej: agreed, a negative answer would be much harder to justify than a positive. The best I can imagine is some knowledgeable person saying “I thought about this a while ago, and did a large literature search, but didn't find anything.” The next best thing would be if this question gets a lot of views but no satisfactory answer… – Peter LeFanu Lumsdaine May 30 '18 at 20:41
  • 1
    A hopefully interesting nonexample: The statement “for every structure M and for every set X equipotent with a subset of (the domain of) M there is a structure N containing X which is isomorphic to M” is easily proved using AF in ZF, and even in Z. AF can be used to prove that for all sets A and X there is a set B equipotent with A and disjoint from X, from which the result follows. Just take B to be the set of all pairs {a,X} where a is an element in A. Of course, instead of using X, we could have avoided AF using any set Y not in the union of X, but this is less constructive. – Rodrigo Freire May 31 '18 at 03:16
  • 1
    You are asking a $\Sigma_1$ question, which is seemingly consistently false (and thus false in the true model of arithmetic). – Asaf Karagila May 31 '18 at 09:24
  • 1
    What about the theory of scattered linear orders? @AsafKaragila: Are there choiceless models that have counterexamples to Hausdorff's theorem on these? – Monroe Eskew May 31 '18 at 10:08
  • 1
    @Monro: Which theorem of Hausdorff, and note this is more a question about choice than about regularity. – Asaf Karagila May 31 '18 at 10:19
  • 1
    @AsafKaragila: I don’t follow your first comment. What $\Sigma_1$ statement from my question are you referring to? The difference between this and my linked previous question, in any case, is a historical/literature-based criterion, not a precise mathematical one; so I don’t quite see how a purely mathematical answer can answer it. – Peter LeFanu Lumsdaine May 31 '18 at 10:43
  • 1
    @MonroeEskew: Thankyou; that seems a very promising area to look in, which I hadn’t been aware of! – Peter LeFanu Lumsdaine May 31 '18 at 10:46
  • 2
    @Asaf, If you assume choice then everything that happens outside the well-founded part has a copy inside WF. So I guess that this means in the choice context, foundation can't affect "ordinary math." The theorem of Hausdorff is a classification of scattered linear orders. He defines an inductive hierarchy starting from singletons and shows that every linear order which does not contain a copy of $\mathbb Q$ appears in this list. – Monroe Eskew May 31 '18 at 11:03
  • 1
    @Monroe: Yes, I understand that. I have made similar remarks in recent related threads. I'm still not 100% sure of which theorem you mean. But my point is that since you're not specifically talking about ZFC in WF, but just ZF, I don't see how any of these things can be "reasonable answers". Yes, everything that can break, will break. Huzzah. So this is no longer a question about regularity, it is a question about choice. In that case, just frame it as a question about choice and move on. – Asaf Karagila May 31 '18 at 11:09

3 Answers3

12

I think Frucht's theorem, the statement "every group is isomorphic to the automorphism group of a graph", is a great example of what you're looking for; from the statement, it'd be hard to tell that any set theory is relevant in the proof.

Frucht's theorem is true in ZF (and ZFC-AF), but independent from ZF-AF. I'll sketch a proof below.

To construct a model of ZF-AF where Frucht's theorem fails, we start a permutation model of ZFA (ZF with atoms) where it fails. The basic Frankel model, where A is superamorphous, works fine (see Jech's "The Axiom of Choice" book if you haven't seen this model before).

To see it fails in the Frankel model, consider the free abelian group $G$ generated by the atoms. Suppose $G$ were the automorphism group of a graph $\Gamma$. Since $\Gamma$ is symmetric, it has a finite support, $E$, and every permutation of $A$ which fixes $E$ must fix $\Gamma$. This means every element of $\mathrm{Perm}(A\setminus E)$ corresponds to an element of $\mathrm{Aut}(\Gamma)$, which is $G$ by assumption. In particular, let $\pi$ the a transposition swapping two elements $a, b\in A\setminus E$. $\pi$ has order 2, so the corresponding element of $G$ has order $\leq$2, but $G$ is free abelian, so we must have $\pi$ acts trivally on $\Gamma$. However, $\pi$ acts non-trivially on $G$; it swaps the generators $g_a$ and $g_b$ corresponding to $a$ and $b$. $g_a$ and $g_b$ must correspond to distinct automorphisms $\gamma_a$ and $\gamma_b$ of $\Gamma$. If $v$ is a vertex in $\Gamma$, then $$\gamma_a(v)=\pi(\gamma_a(v))=\pi(\gamma_a)(\pi(v)) = \gamma_b(\pi(v)) = \gamma_b(\pi(v)) = \gamma_b(v)$$ So, $\gamma_a = \gamma_b$. Since $\gamma_a$ and $\gamma_b$ can't be distinct, $\mathrm{Aut}(\Gamma)$ can't be $G$.

Finally, to get a model of ZF-AF instead of ZFA (where atoms are all empty), you can replace each atom with a distinct Quine atom (a set so $x=\{x\}$). As long as you're careful to define free abelian group in a way that doesn't depend on $x$ not equaling the pair $\langle x,x\rangle$, there shouldn't be any difficulties.

As for why Frucht's theorem holds in ZF, it requires fairly trivial modifications to Sabidussi's ZFC proof.

Given a group $G$, begin with a colored, directed Cayley graph of $G$. This has automorphism group $G$, but if we forget the edge colors and directions, the graph may have extra automorphisms. We can indicate directions by attaching a stick of length 1 and 2 in the middle of every edge in the Cayley graph, resulting in an undirected colored graph with the correct automorphism group. If there are countably many colors, a similar trick works for colors, but in general, we will need distinct rigid graphs for each generator of $G$ to label each color. Under AC, it suffices to build a unique rigid graph for each ordinal; however, Sabidussi's paper actually builds a unique rigid graph for every set, by induction on rank. The idea is, roughly, that given a set in $S\in V_{\alpha+1}$, you begin with a complete graph on $V_\alpha$, and attach to each vertex it's corresponding, inductively defined graph. The resulting graph is now rigid. Then you attach more things to this graph to indicate elements or non-elements of $S$.

I have a better write-up of this argument (with sorely needed pictures) in my thesis, but until that's somewhere I can link conveniently, Sabidussi's paper is probably the best reference for actual induction details.

Brian Pinsky
  • 488
  • 3
  • 7
8

What about Scott's trick?

In more detail: here, I claim, is a proof-schema in ZF that belongs to "ordinary mathematics" but cannot be trivially modified to go through in ZF–AF.

Let $C$ be a locally-large category, by which I mean a proper class of objects, a proper class of morphisms, class-functions for domain, codomain, composition, and identities, satisfying the axioms of a category. (Since a proper class in ZF is specified by a logical formula, this is why the proof is a schema rather than a single one.) Let $W$ be a subclass of the morphisms of $C$. Then we can construct the localization $C[W^{-1}]$ as another locally-large category, as described here: we consider the (large) directed graph whose edges are the morphisms of $C$ and the morphisms of $W^{\rm op}$, generate the free (large) category on it, and then quotient by an appropriate equivalence relation.

The free large category on a large directed graph is unproblematic even in ZF–AF: its morphisms are finite lists of composable edges, and we can define a formula that specifies the proper class of finite sequences of elements of some other proper class. But there is no obvious way to form the quotient of a generic proper class by a proper-class equivalence relation in ZF–AF: the usual construction of the quotient of a set by an equivalence relation takes the elements of the quotient to be equivalence classes, but if the "equivalence classes" are proper classes then they cannot be elements of some other class. Scott's trick is to instead define the elements of the quotient to be the sub-sets of the equivalence proper-classes consisting of all their elements of minimal rank, which are sets since each $V_\kappa$ is a set. But without the axiom of foundation, this doesn't work since we can't assert that each equivalence proper-class contains any well-founded elements.

Mike Shulman
  • 65,064
  • 1
    Of course! Yes, this I agree this definitely hits the “ordinary mathematics” criterion, and while it’s not obvious whether the statement can fail in ZF–AF, it at least seems unlikely that any proof along these lines can work. For anyone who hasn’t seen it, I recommend the original source of Scott’s trick as a beautiful piece of mathematical writing — a 2-paragraph abstract, clearly setting out a powerful statement and its non-trivial proof. (Dana Scott, Definitions by abstraction in axiomatic set theory, Bulletin Amer. Math. Soc. 61 (1955), 442.) – Peter LeFanu Lumsdaine Jul 27 '18 at 07:58
  • 1
    Do you have a simple example of a locally large category? Googling that term only brought me to locally small categories... – Asaf Karagila Jul 28 '18 at 04:43
  • 1
    @AsafKaragila Well, every locally small category is also locally large... – Mike Shulman Jul 28 '18 at 17:16
  • 1
    Yes, but something less trivial? – Asaf Karagila Jul 28 '18 at 17:19
  • 1
    @AsafKaragila: Even assuming both the original category $C$ and the localisation $C[W^{-1}]$ are locally small, the construction of $C[W^{-1}]$ requires Scott’s trick in general, and in most natural examples: the equivalence classes of zigzags will be large, since objects can have many equivalent doppelgängers. So this is already the kind of quotient that requires Scott’s trick, or at least some trick beyond the standard “take the quotient to be the set/class of all equivalence classes”. – Peter LeFanu Lumsdaine Jul 28 '18 at 20:23
  • 1
    @AsafKaragila: On the other hand, for an example of a locally large category, you can take $\mathbf{B}\mathrm{On}$, the (delooping of the) monoid of ordinals under addition. But I don’t know a non-locally-small example where localisations come up naturally (maybe Mike does…) – Peter LeFanu Lumsdaine Jul 28 '18 at 20:25
  • 1
    Right, local largeness is not the real point, I only talked about that because it's the natural context for localization; in general localization doesn't preserve local smallness, although in many cases arising in practice there are other tricks that imply that it does. The point is that, as Peter says, even if the localization is locally small, its equivalence classes are proper classes, so constructing it requires some trick. – Mike Shulman Jul 29 '18 at 00:46
7

It has long been the informal view of set theorists that the Axiom of Foundation does not have consequences for "ordinary mathematics". For example, in Chapter III of his Set Theory: An Introduction to Independence Proofs (1980), K. Kunen tells us that we introduce the axiom to limit set theory to the sets that are actually employed to do mathematics. Similarly, in their mathematico-philosophical classic Foundations of Set Theory (1973, p. 87)), A. A. Fraenkel, Y. Bar-Hillel and A. Levy maintain "its omission will not incapacitate any field of mathematics". Of course mathematics has changed since these works were written, but I suspect the opinions expressed therein have not changed among contemporary set theorists with respect to what you informally call "ordinary mathematics".

Philip Ehrlich
  • 5,915
  • 1
    Thankyou for giving these relevant quotes! However, I have always understood these as having in mind the mainstream setting of ordinary mathematics, where choice is used without too many qualms; and as discussed in the linked previous question and its answers, the consequences of regularity in the presence of choice are quite restricted, in a way that makes them unlikely to affect ordinary mathematics. If you have seen similar quotes from people working in choiceless settings, especially if they suggest serious thought on this issue, then that would seem a stronger negative answer. – Peter LeFanu Lumsdaine May 31 '18 at 10:38