FOM: Re: talk radio style

[Colin Mclarty]

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.

Colin