[FOM] Re: Constructive analysis

[Bas Spitters]

On Wednesday 11 September 2002 13:02, Andrej Bauer wrote:
> Bas' equation
>                       TTE ~ BISH + CC + MP + FT
>
> should be amended with two axioms that get used all the time:
>
>                  TTE ~ BISH + CC + MP + FT + NC + SE
>
> Here NC is "number choice" or "countable choice"

Bishop is not entirely clear about choice. It seems that dependent choice (DC) 
is all that he used. I assumed that DC is included in BISH (and so do Bridges 
and Richman in their Varieties book).
DC is slightly stronger then NC, but as far as I know the philosophical 
reasons for assuming NC also motivate DC.

> The second axiom, SE, is the axiom of not-not stable equality, i.e.,
> for any set A, and all x, y in A,
>
>                      (not (not (x = y)) ==> x = y

This follows from Markov's principle (MP) if the apartness is Sigma01, which 
is usually the case in analysis. So SE does not seem to be needed.

> (By the way, what is "continuous choice"? Perhaps Bass meant
> "countable choice"?)

Continuous choice is a term used by Bridges/Richman for:
1. Any function from N^N to N is continuous and
2 If P subset N^NxN, and for each a in N^N there is n in N such that 
	(a,n) in P, then there is a function f:N^N->N such that (a,f(a)) in P, 
	for all a in N^N.

Hence a combination of the continuity principle and a choice axiom.

> The exact relationship between TTE and "BISH + CC + MP + FT + NC + SE"
> can be explained in terms of realizability, as follows.

Thanks for the nice explanation.

Bas Spitters

-------------------------------------------------------
Department of Computer Science, University of Nijmegen.
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
e-mail: spitters at cs.kun.nl  Phone: +31-24-3652610.