>> | You do occasionally see infinite ordinals in mainstream mathematics,
>> | and even in theoretical computer science.
>> Apropos of the above points, how often are such uses really essential,
>> i.e. not once again locutions which can simply be eliminated in favour
>> of assertions about certain mappings between wosets?
Actually, I think that almost all mainstream uses of von Neumann ordinals
can be eliminated in favor of mappings between well-ordered sets.
That's fine for logicians,
but then your metatheory had better be very clever at hiding
these locutions, or you'll never sell it to the mathematicians.
When mathematicians form a transfinite sequence:
S_0 ... S_83 ... S_omega ....
they don't really care exactly how you constructed the numbers
0 ... 83 ... omega ....
but they do want to think of them as fixed objects,
and they do not want to have to preface each construction by:
Let W be a well-ordered set of large enough size to carry out the
following argument ... Let 0_W denotes the first element of W, let
omega_W denotes the first non-0_W element of W with no predecessor ....
In general, logicians may be willing to go to great lengths
to see what can be done in a weak theory, but you'll never sell
this to mathematicians if it means doing extra work.
Here's another example, which does not use infinite ordinals.
The following construction is common in algebra:
Let F be a field, and now form the sequence of field extensions,
F_0 = F , F_1 , F_2, ...
where for each natural number n, F_{n+1} adds a root of some polynomial.
Now, take the union of all the F_n.
If you define the field extensions in the usual way, then you can't prove
that the union exists in Zermelo set theory; you need the Replacement Axiom.
It's true that if you're clever, you can locute around this and prove
all the basic algebra theorems in Zermelo, but it will be a hard sell
to get the algebraists to buy into doing it this way.
>> For example, I recently wanted to prove in HOL that for any infinite set A,
>> there is a bijection A x A <-> A. ............
>> (Of course the cutest proof is to apply the upward Lowenheim-Skolem theorem
>> to a first order theory of surjective pairing, the assertion being easy for
>> the special case of the natural numbers. In a higher order formalism
>> no metatheory is required to do this as the syntax and interpretation of
>> first order sentences is expressible in the object logic.)
Interesting idea. Does this really work in HOL?
It would seem to me that even given the syntax and semantics of first-order
sentences, the upward Lowenheim-Skolem theorem is not a completely
trivial result. The proofs I know use as a lemma the fact that A and A x A
(and the set of all finite sequences from A) have the same cardinality.
Ken