Re: The principle of unique choice

[Steve Vickers]



[On free choice sequences]

I’ve long had a very computational intuition regarding free choice sequences, but I find it hard to relate it to the discussion of how one understands sets v. propositions. Can anyone help me out to see a connection?

Computationally, sequences have to be understood differently depending on whether you are at the transmitting or receiving end.

At the transmitting end, the algorithm by which you generate the sequence is central. By contrast, at the receiving end the algorithm may be completely inaccessible. The sequence is more like one of Fourman’s messages from Mars.

This distinction is quite clear in Haskell, for instance, where the output from a function has an explicit algorithm - the function -, while the input, a formal parameter, can only be inspected element by element. In fact the Haskell would still work in principle if the sequence had a non-algorithmic source such as meteorological data. Hence at the receiving end you act as if the sequence is a free choice sequence, and to hypothesize that it is law-like has no practical use.

This contrast is formalized in the denotational semantics

  program |-> denotation

where the “denotation” is a point in a topological space and the topology formalizes the restriction on information that only open properties are accessible.

I suggest that, in its purest form, our understanding of lawless sequences is about what happens to a law (a program P) when you put semantic brackets round it ([[P]]).

(Note that this is also the distinction between sequences in Set and sequences in other toposes, in particular the generic sequence in the classifying topos.)

Many will be tempted to insert intermediate objects S and S’ as “sets of sequences”

  Programs -> S = Programs modulo behaviour

    -> S’ = global points of denotation space

    -> denotation space

(S’ becomes relevant once you recognize the denotation space as point-free.)

S and S’ are not available geometrically, but I wonder if they are implicitly playing roles in Giovanni’s discussion. They would be sets (in the broad of sense) of sequences, respectively law-like and lawless.

Here’s my real question. I’d like to think that that program-denotation distinction, in itself and without reference to “sets of sequences”, captures something of what Brouwer had in mind for choice sequences. Can that be right, or am I missing something?

Steve.

On 14 Aug 2026, at 11:21, Giovanni Sambin <gios...@gmail.com> wrote:



Dear Mark,

thank you for your comments. They allow me to explain my proposal a little better.

My impression is that there is no real contrast between us, but simply that we are approaching the
question from different perspectives.

You recall that Brouwer regards choice sequences as something that springs directly from mathematical intuition, from what he calls "selfunfolding".  It's far from me to propose a more accurate interpretation of what Brouwer meant, especially knowing that one of the greatest experts on Brouwer is in the audience.

I am very interested in reconstructing what Brouwer's intention, or intuition, actually was; but here my question is not "what did Brouwer mean?". It seems to me even more interesting to discover what is today the simplest explanation, both mathematically and philosophically, of an arbitrary real number, that is, of what Brouwer explains by means of his choice sequences.

Briefly, I claim that the role of choice sequences can be played by the geometric notion of an arbitrary path in a tree, and that this is possible only if one does not assume as valid the principle "propositions-as-sets" (and therefore neither AC nor AC!). It follows that the best solution is to adopt as a foundation a "weakened" type theory, in which one drops one of the assumptions typical of type theories: namely, the one according to which logic is one of the possible interpretations of type theory itself.

An arbitrary path is a sequence of singletons, which does not coincide with a sequence of elements, precisely because AC! does not hold. An arbitrary path is the extension to infinity of the notion of a finite list of elements (alias a node of the tree). The surprising result is that this notion is not obtained by means of a new conceptual assumption (the concept of an infinite list, that is, a generation by inductive rules that nonetheless proceeds to infinity), but by means of a new and richer mathematical theory: the introduction of positive topologies and the definition of an ideal point on a positive topology.

To accept as basic primitive concepts those of set (inductively generated) and of proposition, and then to define arbitrary paths as ideal points of a suitable positive topology, is conceptually very simple.
Mathematically, it rests on only two primitive notions, from which all the others are defined (such as subset and collection). The difference with respect to Brouwer lies in starting from a strong notion of pointfree topology, namely that of positive topology: the positivity relation allows one to define a very expressive notion of ideal point, which in the case of a tree yields exactly the arbitrary paths.
Philosophically, no unprovable assumption is needed (such as the convergence of the selfunfolding of each individual towards that of an idealised creating subject), but only a practical agreement on what we mean by inductive definition and by proposition, without appealing to static, predetermined notions, but ones clarified dynamically in each individual just enough to communicate without ambiguity with other individuals.

You write:

> In a lecture of 1951 Brouwer speaks, as usual, about his idea that "in modern or intuitionistic mathematics, as we shall see presently, a mathematical entity is not necessarily predeterminate, and may, in its state of free growth, at some time acquire a property which it did not possess before".

I fully agree with the spirit of this statement, in the sense that I too think that a mathematical entity can be determined only in time. It seems preferable to me, however, that this dynamic character be expressed by the notion of proposition (with no need to modify it, since props-as-sets is not assumed), rather than by the problematic notion of a choice sequence of elements of a set S, a notion that is not easy to distinguish from that of an operation, alias a function in the constructive sense, from N to S.

> Further on he explains "One of the reasons that led intuitionistic mathematics to this extension was the failure of classical mathematics to compose the continuum out of points without the help of logic." But in the margin of the manuscript he then adds a note to "reasons": "Incorrect, the  extension is an immediate consequence of the selfunfolding; so here only the utility of the extension is explained."

To say that the notion of choice sequence "is an immediate consequence of the selfunfolding" is precisely what, in my view, would require going beyond the foundation, and therefore having to add it as a further notion: it is not explained in terms of set and proposition, as I do, but requires the notion of selfunfolding (or equivalents, such as the creating subject), which in my opinion is not at all a clear mathematical notion.

I do hope that the matter is now a bit clearer.

Best wishes,
Giovanni

Il giorno lun 20 lug 2026 alle ore 15:48 Mark van Atten <vanatt...@gmail.com> ha scritto:

On Mon, 20 Jul 2026 at 14:14, Giovanni Sambin <gios...@gmail.com> wrote:

> Choice sequences, for Brouwer (and for Kreisel–Troelstra), are a foundational notion to be added.
> But they cannot be sequences in N → N, otherwise they are lawlike as in MLtt.
>
> In my approach, instead, no notion is added at all, and one modifies the base theory by removing AC and AC!. And this is achieved simply by not assuming props-as-sets.
>
> It has also happened other times in the history of mathematics that the solution consisted in removing rather than adding, for example in abstract algebra.


In a lecture of 1951 Brouwer speaks, as usual, about his idea that
"in modern or intuitionistic mathematics,
as we shall see presently, a mathematical entity is not necessarily
predeterminate, and may, in its state of free growth, at some time
acquire a property which it did not possess before".

Further on he explains "One of the reasons that led intuitionistic mathematics
to this extension was the failure of classical mathematics to compose
the continuum out of points without the help of logic."

But in the margin of the manuscript he then adds a note to "reasons":
"Incorrect, the extension is an immediate consequence
of the selfunfolding; so here only the utility of
the extension is explained."

On that view, choice sequence is not a foundational notion separate
from the others.

(For the quotes here, see the Appendix to the Cambridge Lectures,
pp.92 bottom - 93 top and footnote.)

Best wishes,
Mark.

--
You received this message because you are subscribed to a topic in the Google Groups "constructivenews" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/constructivenews/Zc1DD5hoel0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to constructivene...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/CAADExmtyePhJ2XJZSRrN5Yf00pP%3DHw%3D30iFKi%3Dm_4VBq1R5qwg%40mail.gmail.com.