[FOM] Replacement

[Harvey Friedman]

On 8/15/07 2:41 AM, "Jan Pax" <pax0 at seznam.cz> wrote:

> 
>>  Not a good mathematical example, as Forster called for. Along these lines,
>>  one might prefer
>>  
>>  there is a limit ordinal with a limit ordinal below.
>>  
> 
> And thus Borel Determinacy is unprovable in ZFC without replacement as this
> needs V_omega_1.

What does "and thus" mean here? I don't see any relationship between what
you write here and the three lines that you quote from me.

E.g., common formulations of Borel Determinacy in ordinary mathematics do
not involve use of Von Neumann ordinals. Just least sigama algebra, etc. The
"needs V_omega_1" refers to consistency strength (or interpretability), and
also to a particular line of formal systems.

On the other hand, what you wrote is related to my posting about

> "Every symmetric Borel set in the plane contains or is disjoint from the
> graph of a Borel function"
> 
> can be proved in ZFC but not in ZFC\Replacement.

also formulated with "least sigma algebra". The above is closely related to
Borel determinacy, and is immediately understood and appreciated by any
mathematician who is slightly comfortable with Borel sets.

I should mention that there is another way of dealing with ordinals which
predates the von Neumann ordinals. That is, well orderings, where one uses
the equivalence relation of "being isomorphic". You can prove lots about
well orderings and isomorphism without any replacement, and this is by far
more comfortable for most mathematicians.

From: Andrej Bauer <Andrej.Bauer at fmf.uni-lj.si>

>Isn't replacement required for construction of initial algebras (and
>final coalgebras) of functors? For example, given a functor F:Set->Set,
>one often considers the colimit of the diagram

>   0 --> F0 --> F(F0) --> F(F(F0)) --> ...

>The colimit is constructed as a quotient of the disjoint sum of the
>family {0, F0, F(F0), F(F(F0)), ...}. But how do we form this family if
>not by replacement?

>This is certainly "ordinary math" as such constructions are used in
>topology, algebra and theoretical computer science, at least.

This is certainly not ordinary mathematics, although some ordinary
mathematicians might sometimes choose to cast things this way for
expositional purposes. I.e., you can choose to set things up with heavy
doses of generality and abstraction, and make use of unusual axioms. You can
take this kind of thing further by using Grothendieck universes if you want.

This kind of thing will certainly not satisfy the kind of people Forster is
talking to when he wrote:

> I know there are lots of people who dislike the axiom scheme of
> replacement.  They say things like ``it has no consequence for
> ordinary mathematics'' and the like.  Unfortunately i have none
> of them handy at the moment, so i have to ask:  do any of them
> think that the axiom scheme is actually *false*?  Or do they
> merely think that it shouldn't be a core axiom?

Harvey Friedman