What is a finite set?
Well, the standard definition is that a finite set is one whose cardinality is a whole number. More formally, the way this works is that we make this set ω, the whole numbers, consisting of 0, 1, 2, etc., and then we say that a set is finite if it's in bijection with some element of ω.
This... this is not so great. I mean, it works fine ordinarily, but the problem is that it relies on this external thing, ω, and sometimes we might be in a setting where we don't have ω. For instance, suppose you want to take ZF, remove the axiom of infinity, and instead add an axiom that states that all sets are finite. How would you do that? You couldn't do it using this definition of finiteness, because you can't talk about ω if you don't have the axiom of infinity! Indeed, having an ω to talk about would contradict the axiom you wanted to add, that all sets are finite.
So, a different definition is needed. Famously, there's Dedekind's notion of finiteness: A set is finite if it's not in bijection with any proper subset of itself. That's intrinsic -- no reference to any external ω. And this certainly is an important property that differentiates finite sets from infinite ones. But the problem is that while this is equivalent to finiteness in ZFC, without choice, it becomes weaker. In ZF without choice, it's consistent that there exist sets which are infinite, but Dedekind-finite[0]. So this can't be the essence of finiteness after all; just one more useful property. (Note that equivalence doesn't require the full strength of AC -- countable choice will do.)
Anyway so you go to the Wikipedia entry for "finite set" and you find that there are a number of these definitions that are equivalent in ZF. But most of these, while they may be useful and equivalent to finiteness, don't really seem like they are really what finiteness is about. Like, if you dropped some axioms and these became inequivalent, would you still use them? No.
The one that stands out is Kuratowski's definition. Say you have a set S. Take its power set. Take the smallest subset of its power set that: A. contains the empty set and all singletons, and B. is closed under taking unions of two sets. If S itself is in this set, then we say S is finite.
In other words, this is saying that S can be built up one element at a time. And that, really, is what finiteness means. The ordinary definition of finiteness is really saying this too, of course, because whole numbers are things that we build up one element at a time; it just has the problem that it's not intrinsic. And this is also why Dedekind-finiteness seems like the right definition at first: If a set isn't in bijection with any of its proper subsets, then you can remove one element at a time until you get the empty set, then put them back, thereby building it up one at a time. The problem is making that line of reasoning rigorous requires some form of choice.
So Kuratowski-finiteness is what I'd go with, then, in settings where you can't build ω. Although this leaves the question of what about settings where you can build ω, but there's not enough to make the two notions equivalent? Yikes. That sounds bad. Well, I'm not a set theorist or a logician, so, uh, for now I'm just going to hope I don't encounter such a thing. I assume people have actually thought about this before...
Actually, Kuratowski's definition has a problem too -- it relies on the notion of power set. But I think the axiom of power set is one of the ones that constructivists like to throw out and replace with weaker versions. So much for being good in that setting. Is the use of the power set really essential there, though? It's just there to provide the background; I wonder if there's some way to get around that...
Well, this is something I'm definitely not going to think about! In any case, Kuratowski's definition is pretty neat and useful to have available, even if it's not the One True Essence of Finiteness like I initially thought it was...
Edit Jan 6: Seems it's more predicativists than constructivists (yes, there's a large overlap) that object to that, and -- man, to hell with predicativity. I'm going to revert to my earlier position and say that in contexts I might possibly care about, this is the right definition.
-Harry
[0]Assuming consistency of ZF, of course.
Well, the standard definition is that a finite set is one whose cardinality is a whole number. More formally, the way this works is that we make this set ω, the whole numbers, consisting of 0, 1, 2, etc., and then we say that a set is finite if it's in bijection with some element of ω.
This... this is not so great. I mean, it works fine ordinarily, but the problem is that it relies on this external thing, ω, and sometimes we might be in a setting where we don't have ω. For instance, suppose you want to take ZF, remove the axiom of infinity, and instead add an axiom that states that all sets are finite. How would you do that? You couldn't do it using this definition of finiteness, because you can't talk about ω if you don't have the axiom of infinity! Indeed, having an ω to talk about would contradict the axiom you wanted to add, that all sets are finite.
So, a different definition is needed. Famously, there's Dedekind's notion of finiteness: A set is finite if it's not in bijection with any proper subset of itself. That's intrinsic -- no reference to any external ω. And this certainly is an important property that differentiates finite sets from infinite ones. But the problem is that while this is equivalent to finiteness in ZFC, without choice, it becomes weaker. In ZF without choice, it's consistent that there exist sets which are infinite, but Dedekind-finite[0]. So this can't be the essence of finiteness after all; just one more useful property. (Note that equivalence doesn't require the full strength of AC -- countable choice will do.)
Anyway so you go to the Wikipedia entry for "finite set" and you find that there are a number of these definitions that are equivalent in ZF. But most of these, while they may be useful and equivalent to finiteness, don't really seem like they are really what finiteness is about. Like, if you dropped some axioms and these became inequivalent, would you still use them? No.
The one that stands out is Kuratowski's definition. Say you have a set S. Take its power set. Take the smallest subset of its power set that: A. contains the empty set and all singletons, and B. is closed under taking unions of two sets. If S itself is in this set, then we say S is finite.
In other words, this is saying that S can be built up one element at a time. And that, really, is what finiteness means. The ordinary definition of finiteness is really saying this too, of course, because whole numbers are things that we build up one element at a time; it just has the problem that it's not intrinsic. And this is also why Dedekind-finiteness seems like the right definition at first: If a set isn't in bijection with any of its proper subsets, then you can remove one element at a time until you get the empty set, then put them back, thereby building it up one at a time. The problem is making that line of reasoning rigorous requires some form of choice.
So Kuratowski-finiteness is what I'd go with, then, in settings where you can't build ω. Although this leaves the question of what about settings where you can build ω, but there's not enough to make the two notions equivalent? Yikes. That sounds bad. Well, I'm not a set theorist or a logician, so, uh, for now I'm just going to hope I don't encounter such a thing. I assume people have actually thought about this before...
Actually, Kuratowski's definition has a problem too -- it relies on the notion of power set. But I think the axiom of power set is one of the ones that constructivists like to throw out and replace with weaker versions. So much for being good in that setting. Is the use of the power set really essential there, though? It's just there to provide the background; I wonder if there's some way to get around that...
Well, this is something I'm definitely not going to think about! In any case, Kuratowski's definition is pretty neat and useful to have available, even if it's not the One True Essence of Finiteness like I initially thought it was...
Edit Jan 6: Seems it's more predicativists than constructivists (yes, there's a large overlap) that object to that, and -- man, to hell with predicativity. I'm going to revert to my earlier position and say that in contexts I might possibly care about, this is the right definition.
-Harry
[0]Assuming consistency of ZF, of course.
