Eliminating countable choice in a general way (for instance in the aIVT)

[frank waaldijk]

This topic is a follow-up on the previous one which discusses the elimination of countable choice when proving the approximate intermediate value theorem (aIVT):

For all continuous real functions f, for all a,b in R, for all e>0:
If f(a) < 0 < f(b) then there is x in R such that |f(x)| < e

 
One should first see the beautiful new proof of aIVT (countable-choice-free) that Matt F. gave on MathOverflow (http://mathoverflow.net/a/255371/49). Here I hope to describe a more general way to eliminate countable choice, which works in other settings as well. I will use aIVT as a running example, and the usual bisection method for proving it. For clarity I will distinguish between equivalence classes and representatives, even though this is slightly more work.

You will recall that the bisection method as usually described, asks one to choose between two options at each iteration step. However, as I described in the previous topic, if one eliminates all choice in the construction of a, b and f (by making them recursive), and one picks a (recursive) representative a' and b' these iterative choices can be eliminated and replaced by a completely deterministic algorithm.

This is because the definition and evaluation of all iterations can then be made recursive in a', b'. 

Leaving recursion aside, there is a more general way to eliminate choice in the construction of a,b and f. [Actually I have been working on this for the past 5 years and it shows how really slow my mind works in foundational matters, that I didn't realize earlier in the previous topic how well that work can be applied here )-: ]

And that way involves looking at f as well. (Thank you Mike Shulman for asking for `functionality')

Now the easiest way to explain what I mean is to consider aIVT once again, but keep in mind that the procedure works in many many other settings [I think to  have proved that in NToP (Natural Topology, a BISH-version of intuitionistic topology) will comment and reference later].

The most important thing is to construct R not as Cauchy-sequences (equiv. classes if you will) but as shrinking rational intervals, using the standard apartness # which generates the reals. This is Brouwer's way, but I have adapted it to BISH in NToP. When we do so, we see that R arises as a #-quotient of Baire space (B).

Now the beauty of NToP is the following: continuous functions from B to B form the machinery to construct continuous real functions, and (in the presence of a Lindelöf-type axiom which is valid in CLASS, INT and RUSS) vice versa every real function can be represented by such a "#-morphism".

Thm. (valid in CLASS, INT, RUSS):
Every continuous function f from R to R can be represented by a morphism f' from (B,#) to (B,#)

The relevant property here of such a morphism f' is that it represents f in one fell stroke, thus eliminating the need for countably many choices when iterating.

Now to prove the above theorem we need the Lindelöf-type axiom BDD (Bar Decidable Descent: "every bar on B descends from a decidable bar"), and to prove BDD in INT or RUSS we use choice axioms stronger than countable choice.

But. We don't need the above theorem. If we just limit ourselves beforehand to real functions f which are given by a representative f' which is a #-morphism from (B,#) to (B,#), then everything works like clockwork.

Because (not surprisingly), any function that you dream of can be thus represented, -unless perhaps you are dreaming in a very cleverly constructed topos-, so addition etc. (well, all the recursive functions :-)) can be thus represented, AND composition of morphisms is uniquely defined (deterministically).

So we see that, if we define a continuous real function f to be a real morphism iff it has a representation as a #-morphism, then we can use the bisection method to prove (without using countable choice):

aIVT*:  For all real morphisms f, for all a,b in R, for all e>0:
If f(a) < 0 < f(b) then there is x in R such that |f(x)| < e

Proof: pick representatives a', b' in B, and f' which is a #-morphism representing f. Taking the mean of a,b (a/2+b/2) also has such a #-morphism-representative say m', and using a', b', f' and m' we can deterministically define a sequence x' in B which represents x in R for which f(x)<e.

Barring mistakes on my part (don't discount that possibility please...reluctant as I am to say so, past experience has taught me a lot of humility in that respect...), this method works for other settings as well, I believe.

Well...I'll be interested to hear from you.

Regards,
Frank

[Michael Shulman]

This is interesting, but if I understand correctly you aren't really
proving the same theorem, since you've restricted the class of
functions to those that have a particular kind of representation?

[frank waaldijk]

Yes, but you should take into account that in CLASS, INT and RUSS this restriction is no restriction at all (that is what the mentioned theorem is for).

In other words, in CLASS, INT and RUSS we can prove:

Every continuous real function is a real morphism.

So if you would like a really hard challenge: I will give €5 (sorry, I'm stingy and you never know if Matt reads this :-) ) to anyone who can give even an indication of a model/topos/what have you in which there is an concrete example of a continuous real function which cannot be represented by a #-morphism.

[frank waaldijk]

This is why in NToP the recommendation is to work with morphisms in BISH. Morphisms are much sharper defined objects, and one does not lose anything which exists in CLASS, INT or RUSS. Another plus side is that morphisms are (I believe) well suited for computational purposes (or at least to ensure a smooth transition from theory to computation).

[Michael Shulman]

That's an interesting challenge, but the only point I want to make is that because of this restriction it seems that the method you describe is not strictly "more general" than Matt's.

[Frank Waaldijk]

If you want to interpret "more general" in the most strict sense, then you are absolutely right. More than right, because in the case of aIVT Matt's proof is "marginally" more general than the NToP method.

I felt that I had already acknowledged this, as well as the beauty of Matt's proof.

In a slightly less strict sense, which is the default language that I use when discussing foundations on a meta-level, I believe the term "more general" describes the NToP method compared to Matt's proof rather accurately.

But I was obviously not clear enough, so let me try once more.

You have a class C(R,R) of "pointwise continuous real functions" for which Matt proves aIVT without using CAC, DC or uniform continuity, directly in BISH.

In C(R,R) we can pinpoint a subclass M(R,R) of real morphisms for which, using NToP, one can prove aIVT without using CAC, DC or uniform continuity, directly in BISH.

Now I'm telling you that this subclass M(R,R) actually coincides with C(R,R) in the three most important subtheories of BISH, namely CLASS, INT and RUSS.

Therefore the method NToP provides for finding x with |f(x)|<e ... really works for any conceivable function f in C(R,R) that you can come up with in BISH. I hope this helps you understand why I consider the NToP method only "marginally" less general than Matt's proof on the subject of aIVT.

But Matt's proof is very specific for aIVT. The NToP method to eliminate countable choice works

"for all" constructive proofs involving Polish spaces which rely on an iterative construction which involves evaluating #-morphism values derived from a finite number of input values and input #-morphisms.

If I said "continuous-function" I would once again be slightly inaccurate in the most strict sense. But to me, it makes far more sense to use the class of #-morphisms in BISH for Polish spaces (like I said, in its main three subtheories there is no difference between this subclass and the class of the continuous functions), because the #-morphisms have a very sharp constructive description. A #-morphism is uniquely determined by one single element of Baire space. That is the precise feature which allows for countable-choice-elimination.

Think of it: an entire continuous real function coded uniquely by just one single element of Baire space, in a way that also facilitates computing. And then consider having this machinery for all Polish spaces.

That is what I mean with "more general".

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

[Frank Waaldijk]

Sorry, "coded uniquely" is not correct, I meant "coded unambiguously". There are many #-morphisms describing the same continuous real function. "Coded uniquely" only holds for morphisms between Polish spaces which are say homeomorphic to a "closed subspace of Baire space", in other words which are subspreads of Baire space.

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

[Andrej Bauer]

> In C(R,R) we can pinpoint a subclass M(R,R) of real morphisms for which,
> using NToP, one can prove aIVT without using CAC, DC or uniform continuity,
> directly in BISH.

Oh, it works much better than that. It works in an elementary topos,
and in type theory, including homotopy type theory. In fact, I bet it
works in Abstract Stone Duality. It does not rely on any peculiarities
of BISH (such as the idea that equality is an equivalence relation).

> Now I'm telling you that this subclass M(R,R) actually coincides with C(R,R)
> in the three most important subtheories of BISH, namely CLASS, INT and RUSS.

True, but that's a rather impoverished view of the world of
constructive mathematics. Just three varieties to care about? How
about sheaves, and topological models, and other realizability models,
and type theory, and Abstract Stone Duality?

The method of representing functions by combinatorial objects (trees
of some sort, usually) is of course quite useful for many purposes,
but is too concrete, and therefore too limiting, to serve as a general
notion of continuous function. There is more to continuity than
representation by a combinatorial object.

With kind regards,

Andrej

[Frank Waaldijk]

I'm glad you think it works, Andrej!

How about sheaves, and topological models, and other realizability models,
and type theory, and Abstract Stone Duality?

 

The method of representing functions by combinatorial objects (trees
of some sort, usually) is of course quite useful for many purposes,
but is too concrete, and therefore too limiting, to serve as a general
notion of continuous function. There is more to continuity than
representation by a combinatorial object.

That is why my recommendation to use #-morphisms was limited to BISH.

As you know, I have been commenting on the idiosyncrasies of BISH for a long time. But, to be fair to BISH, let me say some meta-metamathematical things on a personal note.

Aside from INT and RUSS, I have never been impressed by the alternatives to  BISH (including my own, don't worry). The reason that INT and RUSS impress me is because they offer a sharply described comprehensive framework for doing any kind of mathematics that interests me (usually this is "low abstraction level" stuff, like the analysis, algebra, topology,... that is described in (under)graduate courses). And everything in INT and RUSS works simply, consistently, coherently, just like one would expect in math.

Moreover I do not need to belong to some group of specialists to study and understand INT and RUSS. Because there are standard textbooks which build up these theories from the ground up in a very clear and very very precise way.

No surprise then that INT and RUSS are rather stable. Meaning that one can really build from the ground up without having to worry too much about shifting foundations.

If at any time one of the varieties from the less impoverished constructive world that you mention can match the above (personal I know) criteria, please let me know. The chapter in the HoTT-book on constructive math to me is just a stub. I have yet to see a comprehensive treatise of formal topology in which it is painstakingly precisely shown that we can also do analysis and other math easily in formal topology. And in which all the axiomatics are detailed. And which also shows the advantage of formal topology over say Brouwer's methods. I have to say that ASD looks solid to me, but is over my head so far [this is really my failure I suppose], making it hard for me to evaluate.

Looking from my low-level perspective, I also think that anything in constructive mathematics ultimately stems from N. Countable infinity is already a difficult subject. Finite combinatorics is the only sure ground. That means that anything that is built in the richer constructive world ultimately has to come from and to function in something close to BISH.

For me personally, I will find worthwhile anything that is built in the richer constructive world if it demonstrably solves concrete issues in computing and a BISH-like environment.

I know you and many others are working on precisely such worthwhile issues, but allow me to repeat my plea for "advanced constructivism" to build a stable, easy-to-understand, foundationally precise and comprehensive platform in which also a low-abstraction-level person like myself can do math. And to take some time to write an accessible textbook for non-specialists.

So to you representing continuous functions by elements of Baire space may seem too restrictive, and you are probably right from a general perspective. But on my ground level it is already pretty sophisticated. And it works simply, exactly, precisely, in the stable theories CLASS, INT and RUSS (which can be viewed as a natural subtheory of INT).

Maybe some comparison can be made here that studying assembly language is low-level, but not completely irrelevant. And that for efficient, portable, smooth and verifiable programming, all details of the interaction between program, compiler and assembler need to be taken into account together, keeping in mind also that all codes should be readable and checkable for people who didn't write them.

But I know little about software development, so  perhaps this is not an apt comparison. [I do know that in NToP, many spaces have different representations as a natural space (many ways to build a #-quotient), and often one needs one representation in situation A and another in situation B. A nice feature of NToP is that the transition of one representation to another is again given by a #-morphism. That is the kind of low-level stuff that I'm interested in.] 

Best wishes, and glad to see your interest in this subject Andrej,

Frank

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

[Andrej Bauer]

I would suggest realizability as a comprehensive framework of the kind
you are looking for. It is concrete (it is safe to ignore the
category-theoretic incarnations of realizability if one is mostly
interested in just doing constructive math), it is a common
generalisation of all the varieties you mention, but it also offers a
more general picture. Jaap van Oosten wrote a book about it, I wrote
a PhD thesis specifically targeted at computable/constructive math,
and so did Peter Lietz, not to mention the work of Kleene, Vesley,
Troelstra and others that came before, although I will admit that a
textbook about constructive mathematics through realizability would be
very welcome.

In short, and speaking vaguely, for every model of computation A
(which we can think of as a general-purpose programming language, or a
partial combinatory algebra) there is a corresponding realizability
model R(A). Now, the instances arise as special cases:

1. INT is obtained when we take as A the Type 2 Turing machines. (To
be a bit more precise, we take *all* sequences are realizers, but only
computable ones as programs.)

2. RUSS is obtained when we take as A ordinary Turing machines.

3. CLASS is the trivial case when the model of computation consists of
a singleton.

This approach is relevant because in practice we do *not* use Turing
machines. We use programming languages, and they give realizability
models which are *different* from INT and CLASS. If you already think
of constructive mathematics as having something to do with computation
(that's not the only option!), and you want your theorems to actually
be applicable in practice, then general realizability is only a slight
generalisation of what you're used to doing that will give you
precisely that. Instead of relying on Turing machines, or some other
specific idea about representation of objects and computation with
them, assume nothing in particular, apart from a very general ability
to compute. The passage is perhaps comparable to that of passing from
analysis on Euclidean spaces R^n to analysis on complete metric
spaces.

With kind regards,

Andrej

[Frank Waaldijk]

Thank you Andrej for this answer!

I like realizability, and I read your thesis and Peter Lietz's (doesn't mean I am capable of doing things that way), and have familiarized myself somewhat with TTE because even to me it is clear that these approaches are quite valid on the ground level that I mentioned.

I do suspect that NToP will fit well in either of these settings, I'm not sure if NToP is really superfluous because I still have some (diminishing... :-) ) expectations that the apartness topology offers elegancy.

[Anyway, NToP is basically a "minor" adaptation of Brouwer's work based on a very beautiful idea of Wim Couwenberg. I'm just the patsy who got stuck with writing the book. Oh, and I also think that NToP can serve as a very natural way to formulate Brouwer's ideas in CLASS.]

So then, really, I will enjoy a textbook on constructive mathematics through realizability, if it is considerate enough to include readers having my limited knowledge. Perhaps you should not underestimate the impact that such a book could have, meaning it might well be worth anyone's time and effort to write such a book (becoming the patsy :-)).

Best wishes,

Frank

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

[Frank Waaldijk]

Michael, I truly apologize. On rereading the topic, I now see that I really hadn't explained at all why I thought the NToP method was "more general".

Please forgive me, I was under the impression that I had already spelled it out, when really to an uninitiated interested person the claim was obviously unclear. 

This is precisely what I would want to avoid, the only excuse I have is that this topic has been somewhat too much exertion for me, and that I saw your question late last night when I should have made the decision to go to bed instead of replying. 

So, instead of being rather strict as I implied, your question was actually very relevant. Sorry once again, best wishes Frank

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

On Sat, Nov 26, 2016 at 12:17 AM, Frank Waaldijk <fwaa...@gmail.com> wrote:

[Bhupinder Singh Anand]

On Saturday, November 26, 2016 5:24 PM, Frank Waaldijk wrote in construc...@googlegroups.com:

 

“… I will enjoy a textbook on constructive mathematics through realizability …”

 

Dear Frank,

 

The following paper---which implicitly addresses the role of realizability in differentiating between constructive and non-constructive mathematical reasoning---is due to appear in the December 2016 issue of 'Cognitive Systems Research':

 

'The Truth Assignments That Differentiate Human Reasoning From Mechanistic Reasoning: The Evidence-Based Argument for Lucas’ Goedelian Thesis'

 

Kind regards,

 

Bhup

 

CSR paper: https://foundationalperspectives.files.wordpress.com/2016/05/28_human_reasoning_v_mechanistic_reasoning_update.pdf