*Post by Alan Smaill**Post by Julio Di Egidio*You 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 Smaill*Suppose 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.