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.
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.