Post by Alan SmaillPost by Julio Di EgidioYou still do not answer the question: sure,
there are even unicorns out there, but how's that
relevant to the theory, in this case, ZF-Inf and to
the mathematics we can do with it? Namely, can any
putatively infinite sets enter an argument in ZF-Inf
in any useful way at all?
I have no idea how useful ZF-Inf is as a theory,
I'm not aware of anyone exploring what can be done.
Whether the following is useful is a matter of taste,
I suppose.
One thing that we don't need either Inf or ~Inf for
is deriving the familiar form of induction
( P(0) & Ax:( P(x) -> P(Sx) ) -> Ay: P(y)
where we refer only to finite ordinals.
Suppose that
0 := {}
Sx := (x U {x})
Nx :=
(x = 0 \/ Ey e x: Sy = x )
& Az e x: ( z = 0 \/ Ev e x: Sv = z )
Nx == "x is a finite ordinal"
A finite ordinal either has an immediate predecessor
or is 0.
With the axiom of foundation, ordinals are well-ordered.
If there is a counter-example to P(x), there is a first
counter-example to P(x).
If P(x) -> P(Sx), then the first counter-example
doesn't have an immediate predecessor. If P(0), then
it isn't 0, either. If both, there is no first
counter-example.
Therefore (for finite ordinals),
( P(0) & Ax:( P(x) -> P(Sx) ) -> Ay: P(y)
[...]
Post by Alan SmaillSuppose there is an infinite set. Now use replacement to
show that there is a set such that zero is an element of it
and the successor of every element of it is an element of it.
Contradiction with ~Inf, so there is no infinite set.
(Jim Burns has been outlining the main part of the proof.)
It's really very simple. It's just that we only rarely
use the axiom schema of replacement, so it seems odd.
If we can describe the elements of some class (which is
possibly a set) and that class is _not larger than_ some
set, then the axiom of replacement says that class is
also a set.
In this case, if there is an infinite set B, there is a
minimal infinite set B'. The axiom of infinity asserts
the existence of some set which can be as small as the
minimal infinite set B'. We describe the elements
{}, {{}}, {{},{{}}}, ...
and we show that there are not more of them than the
elements of B'. Therefore, they form a set.
"What? Any description at all can form a set?" one may ask.
It's the restriction in size that prevents all that freedom
from erupting into things like the "set" of all sets not
containing themselves. So I'm told, anyway.
I'm not sure how one would go about supporting that
claim with more than "So I'm told", but ZFC does seem
to be successful out here in the real world.