[FOM] New umbrella
P.B.Levy at cs.bham.ac.uk
Sun Nov 2 12:58:20 EST 2014
On 2 Nov 2014, at 17:05, fom-request at cs.nyu.edu wrote:
> Date: Sun, 2 Nov 2014 13:26:21 +0100
> From: Bas Spitters <b.a.w.spitters at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc: Freek Wiedijk <freek at cs.ru.nl>
> Subject: Re: [FOM] New umbrella? (Freek Wiedijk)
> <CAOoPQuTo1RoPwDQwQwwixVTX4ioTvnAuDQRVG+D=g2DFof72qg at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
> Dear Paul,
> Your paper seems somewhat imprecise on what "Set" is. I am guessing
> some (Boolean?) topos.
These papers generally need excluded middle, Axiom of Choice and Axiom
of Replacement, so I don't believe the results would apply to an
arbitrary boolean topos.
> Perhaps you need some universes?
We can make do with classes (since functor categories from large
categories aren't used), but life is easier with universes.
> I'd be surprised if you were actually using *cumulative* set theory.
You are right; these papers don't depend on Foundation.
A famous example: every endofunctor F on Set preserving injections is
isomorphic to one preserving inclusions. (Adamek)
This follows from either global choice or strong extensionality (the
statement that any two bisimilar sets are equal, implied by Foundation
and by Antifoundation).
Antifoundation, while we're on the subject, is so much fun. For
example, it implies that domain equations have unique identity-
structured bifree solutions.
Too bad there will be no place for fun in the serious mathematics of
the future. :-(
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
More information about the FOM