[FOM] Re: Constructive analysis
spitters at cs.kun.nl
Thu Sep 12 05:21:06 EDT 2002
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.
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.
More information about the FOM