The axiom of foundation seems pretty ad hoc to me. It’s there to patch Russell’s paradox. I see no reason not to expect further paradoxes.
We arrived at the axiom of infinity from a finite amount of experience, which seems troubling to me.
This is an extremely finite, weird statement.
It’s a very cool construction, but it’s a finite one that we can verify by hand or with computer assistance. Of the things that ZF claims exist, some of them have this “verifiability” property and some don’t. At the very least don’t you agree that’s a crucial distinction, and that we ought to be strictly less skeptical of constructible, computable, verifiable things than of things like uncountable ordinals?
Also, there’s another respect in which foundation doesn’t impact Russell issues at all. Whether one accepts foundation, anti-foundation or no mention of foundation, one can still get very Russellish issues if one is allowed to form the set A of all well-founded sets. Simply ask if A is well-founded or not. This should demonstrate that morally speaking, foundation concerns are only marginally connected to Russell concerns.
To make the obvious comment, this is all unnecessary as Russell’s paradox goes through from unrestricted comprehension (or set of all sets + ordinary restricted comprehension) without any talking about any sort of well-foundedness...
But that’s a neat one, I hadn’t thought of that one before. However I have to wonder if it works without DC.
Edit: I feel silly, this doesn’t use dependent choice at all. OK, so the answer to that is “yes”. However it does require enough structure to be able to talk about infinite sequences, unless there’s some other way of defining well-foundedness.
There are (at least) three ways to define well-foundedness, roughly:
one which requires impredicative (second-order) reasoning;
one which requires nonconstructive reasoning (excluded middle);
one which requires infinitary reasoning (with dependent choice, and also excluded middle actually).
They may all be found at the nLab article on the subject; this article promotes the first definition (since we use constructive mathematics there much more often than predicative mathematics), but I think that the middle one (Lemma 2 in the article) is actually the most common. However, the last definition (which you are using, Lemma 1 in the article) is usually the easiest for paradoxes (and DC and EM aren’t needed for the paradoxes either, since they’re used only in proofs that go the other way).
One thing bothering me—is there any way to define a well-founded set without using infinitary reasoning? It’s easy enough to say that all sets are well-founded without it, by just stating that ∈ is well-founded—I mean, that’s what the standard axiom of foundation does, though with the classical definition—but in contexts where that doesn’t hold, you need to be able to distinguish a well-founded set from an ill-founded one. Obvious thing to do would be to take the transitive closure of the set and ask if ∈ is well-founded on that, but what bugs me is that constructing the transitive closure requires infinitary reasoning as well. Is there something I’m missing here?
I know one way; it cannot be stated in ZFC↺ (ZFC without foundation), but it can be stated in MK↺ (the Morse–Kelley class theory version): a set is well-founded iff it belongs to every transitive class of sets (that is every class K such that x ∈ K whenever x ⊆ K); it is immediate that we may prove properties of these sets by induction on membership, and a set is well-founded if all of its elements are, so this is a correct definition. However, it requires quantification over all classes (not just sets) to state.
Sure foundation is by far the most ad-hoc axiom. But it is also one of the one’s that is easiest to see doesn’t generally matter. For pretty much any natural theorem if a proof uses foundation then there’s a version of the theorem without it. Since not-well founded sets don’t fit most of out intuition for sets as things like boxes that’s not an issue. None of the serious apparent paradoxical properties go away if you remove foundation.
It’s a very cool construction, but it’s a finite one that we can verify by hand or with computer assistance. Of the things that ZF claims exist, some of them have this “verifiability” property and some don’t. At the very least don’t you agree that’s a crucial distinction, and that we ought to be strictly less skeptical of constructible, computable, verifiable things than of things like uncountable ordinals?
Yes, certainly but by how much? If our intuition can go this drastically wrong on small finite objects why should I trust my intuition on objects that are even further removed from my everyday experience? I mean it isn’t like I need 30 or 40 sided dice to pull this off. In fact you can actually make much smaller than 6 sided dice that are non-transitive. Working out the minimum number of sides (assuming that each die in the set doesn’t need to have the same number of sides) is a nice exercise that helps one understand what is going on.
You’re right, I see that it’s the “restriction” of restricted comprehension that actually does the work in avoiding Russell’s paradox, not foundation. Nevertheless, the story is the same: we had an ambitious set-theoretic foundation for mathematics, Russell found a simple and fatal flaw in it, and we should not simply trust that there will be no further problems after patching this one.
If our intuition can go this drastically wrong on small finite objects why should I trust my intuition on objects that are even further removed from my everyday experience?
This is hardly an argument for accepting that infinite sets exist! There may be a counterintuitive contradiction that one can arrive at from ZF, just as Russell’s paradox is a counterintuitive contradiction arrived at from 19th century foundations, and just as all kinds of counterintuitive but non-contradictory behavior is possible in the finite, constructive realm.
I am proposing that we remove the axiom of infinity from foundations, not that we go further and add its negation. (Though I see that there has been work done on the negation of the foundation axiom! And dubious speculation about its role in consciousness.)
Also one other remark: Foundation isn’t there to repair any Russel issues. You can get as a theorem that Russell’s set doesn’t exist using the other axioms because you obtain a contradiction. Foundation is more that some people have an intuition that sets shouldn’t be able to contain themselves and that together with not wanting sets that smell like Russell’s set caused it to be thrown in.
I’m really tempted to be obnoxious and present an axiomatic system with a primitive called a “paradox” and then just point out what happens one adds the axiom that there are no paradoxes. This is likely a sign that I should go to bed so I can TA in the morning.
The axiom of foundation seems pretty ad hoc to me. It’s there to patch Russell’s paradox. I see no reason not to expect further paradoxes.
We arrived at the axiom of infinity from a finite amount of experience, which seems troubling to me.
It’s a very cool construction, but it’s a finite one that we can verify by hand or with computer assistance. Of the things that ZF claims exist, some of them have this “verifiability” property and some don’t. At the very least don’t you agree that’s a crucial distinction, and that we ought to be strictly less skeptical of constructible, computable, verifiable things than of things like uncountable ordinals?
Also, there’s another respect in which foundation doesn’t impact Russell issues at all. Whether one accepts foundation, anti-foundation or no mention of foundation, one can still get very Russellish issues if one is allowed to form the set A of all well-founded sets. Simply ask if A is well-founded or not. This should demonstrate that morally speaking, foundation concerns are only marginally connected to Russell concerns.
To make the obvious comment, this is all unnecessary as Russell’s paradox goes through from unrestricted comprehension (or set of all sets + ordinary restricted comprehension) without any talking about any sort of well-foundedness...
But that’s a neat one, I hadn’t thought of that one before. However I have to wonder if it works without DC.
Edit: Answer is yes, it does, see below.
Sorry. what do you mean by DC?
Dependent choice.
Edit: I feel silly, this doesn’t use dependent choice at all. OK, so the answer to that is “yes”. However it does require enough structure to be able to talk about infinite sequences, unless there’s some other way of defining well-foundedness.
There are (at least) three ways to define well-foundedness, roughly:
one which requires impredicative (second-order) reasoning;
one which requires nonconstructive reasoning (excluded middle);
one which requires infinitary reasoning (with dependent choice, and also excluded middle actually).
They may all be found at the nLab article on the subject; this article promotes the first definition (since we use constructive mathematics there much more often than predicative mathematics), but I think that the middle one (Lemma 2 in the article) is actually the most common. However, the last definition (which you are using, Lemma 1 in the article) is usually the easiest for paradoxes (and DC and EM aren’t needed for the paradoxes either, since they’re used only in proofs that go the other way).
One thing bothering me—is there any way to define a well-founded set without using infinitary reasoning? It’s easy enough to say that all sets are well-founded without it, by just stating that ∈ is well-founded—I mean, that’s what the standard axiom of foundation does, though with the classical definition—but in contexts where that doesn’t hold, you need to be able to distinguish a well-founded set from an ill-founded one. Obvious thing to do would be to take the transitive closure of the set and ask if ∈ is well-founded on that, but what bugs me is that constructing the transitive closure requires infinitary reasoning as well. Is there something I’m missing here?
I know one way; it cannot be stated in ZFC↺ (ZFC without foundation), but it can be stated in MK↺ (the Morse–Kelley class theory version): a set is well-founded iff it belongs to every transitive class of sets (that is every class K such that x ∈ K whenever x ⊆ K); it is immediate that we may prove properties of these sets by induction on membership, and a set is well-founded if all of its elements are, so this is a correct definition. However, it requires quantification over all classes (not just sets) to state.
Sure foundation is by far the most ad-hoc axiom. But it is also one of the one’s that is easiest to see doesn’t generally matter. For pretty much any natural theorem if a proof uses foundation then there’s a version of the theorem without it. Since not-well founded sets don’t fit most of out intuition for sets as things like boxes that’s not an issue. None of the serious apparent paradoxical properties go away if you remove foundation.
Yes, certainly but by how much? If our intuition can go this drastically wrong on small finite objects why should I trust my intuition on objects that are even further removed from my everyday experience? I mean it isn’t like I need 30 or 40 sided dice to pull this off. In fact you can actually make much smaller than 6 sided dice that are non-transitive. Working out the minimum number of sides (assuming that each die in the set doesn’t need to have the same number of sides) is a nice exercise that helps one understand what is going on.
You’re right, I see that it’s the “restriction” of restricted comprehension that actually does the work in avoiding Russell’s paradox, not foundation. Nevertheless, the story is the same: we had an ambitious set-theoretic foundation for mathematics, Russell found a simple and fatal flaw in it, and we should not simply trust that there will be no further problems after patching this one.
This is hardly an argument for accepting that infinite sets exist! There may be a counterintuitive contradiction that one can arrive at from ZF, just as Russell’s paradox is a counterintuitive contradiction arrived at from 19th century foundations, and just as all kinds of counterintuitive but non-contradictory behavior is possible in the finite, constructive realm.
I am proposing that we remove the axiom of infinity from foundations, not that we go further and add its negation. (Though I see that there has been work done on the negation of the foundation axiom! And dubious speculation about its role in consciousness.)
Also one other remark: Foundation isn’t there to repair any Russel issues. You can get as a theorem that Russell’s set doesn’t exist using the other axioms because you obtain a contradiction. Foundation is more that some people have an intuition that sets shouldn’t be able to contain themselves and that together with not wanting sets that smell like Russell’s set caused it to be thrown in.
And of course more generally, for those not familiar, you can never get rid of paradoxes by adding axioms!
I’m really tempted to be obnoxious and present an axiomatic system with a primitive called a “paradox” and then just point out what happens one adds the axiom that there are no paradoxes. This is likely a sign that I should go to bed so I can TA in the morning.
How about by legislating? Has that been tried?