FOM: Re: talk radio style
cxm7 at po.cwru.edu
Sun Jan 18 10:28:15 EST 1998
Reply to message from simpson at math.psu.edu of Sat, 17 Jan
>Steve Awodey writes:
> > The further questions Steve is asking, regarding the use of
> > excluded middle and choice in developing analysis in a topos, are
> > not essentially different in topos theory than in the context of
> > higher-order logic. In particular, there's nothing new to be said.
>Huh? McLarty said that excluded middle and choice are not needed for
>analysis in a topos. According to McLarty, all that is needed is the
>natural number object.
Choice and excluded middle are not *needed*, they are
*available* as further assumptions if you want them. I have said
this all along, and Awodey is saying it here.
Your own work often distinguishes between assumptions needed
to prove a given theorem, and further assumptions available to
strengthen the effect of the theorem. Don't drop your standards of
rigor when you discuss topos theory.
>[ Technical question: I'm confused about the mismatch between Cauchy
>and Dedekind reals. McLarty said this can happen in a topos with
>natural number object. Can it happen in higher-order logic? ]
Are you familiar with Intuitionistic ZF? It happens there.
This answers your question about higher order logic.
More information about the FOM