If math allowed mutable state, we could reduce the axiom of choice to excluded middle:
def axiom_of_choice(family): cache = {} def choice_fn(index): if index not in cache: cache[index] = family(index) return cache[index] return choice_fn
This relies on excluded middle because the ability to check whether an index is in the cache and if so look it up requires the ability to compare indices by equality.
(Sampling from family(index) is legit. The axiom of choice asserts that dependent products commute with propositional truncation. Propositional truncation does not destroy the computational content of the realizers of the family, it just quotients the realizers to be equal for when it comes to determining the well-definedness of functions. Since we use a cache, the resulting choice_fn still respects equality.
This isn’t valid type theory of course, since type theory has models that don’t permit this stuff and requires propositional truncation to be explicit.)
I think of this as a sort of converse of Diaconescu’s theorem.
This isn’t actually how the effective topos gets countable choice. Instead I believe the effective topos relies on the fact that realizers of functions out of have to be deterministic because elements of don’t admit multiple representations.
I assume family here is a function that accepts an index and returns a nonempty set? But then it seems that for the first encountered index the choice function will just return a set rather than an element from it, no? Or am I misreading something?
family is a function that witnesses the “nonemptiness” (really, mere inhabitedness) by returning an element of the propositional truncation of the set. So more formally, axiom_of_choice has type (Πi: I. ||F(i)||) → ||Πi: I. F(i)||. The “choice” comes from the fact that family (due to the propositional truncation) is allowed to return different F(i)’s from identical i’s, whereas choice_fn is required to choose a canonical F(i) for each i . (The intermediate results are untyped because this is a realizer, not a typed term in a type theory.)
😅 This explanation is, I assume, not very helpful to anyone who doesn’t already know what’s going on. But basically in type theory, propositions correspond to (propositionally truncated) types, and proofs correspond to programs/terms with the types in question, so in proving the nonemptiness of the sets, you automatically end up with a witness function that picks out elements—except the witness function may be “nondeterministic” (that’s where the propositional truncation comes in), which is what requires choice to fix.
The propositional truncation is important to understand. There is a version of type theory’s logic that doesn’t include propositional truncation, but in it the axiom of choice is trivial to prove and not really of any use. Unfortunately the intuitive way to explain propositional truncation gives catastrophically wrong intuition for my use-case, as explained here: https://mathstodon.xyz/@MartinEscardo/111014413939196037
I am not an expert, but I think solutions like this have a potential of hitting an infinite recursion, if evaluating some expression inside the code somehow indirectly invokes the axiom of choice, for example if you construct an object specifically for that purpose.
My understanding of the axiom of choice, and the axioms in general, is that instead of merely describing how things work, they are describing what things are are talking about (by describing how they work). There are multiple concepts (in the Platonic realm) you could plausibly mean when you use the word “set”.
The axiom of choice says “I only mean those models that have the property that for any set of sets, there is a selection that works like this, and the selection itself is included in the model of ‘sets’”. There are models that follow the remaining axioms and have the property, and also models that follow the remaining axioms and don’t have the property.
I guess to add, the thing about constructive math (which avoids excluded middle and unrestricted choice) is that it permits models where everything is computational. What I hope I’ve shown is that in some such models, the obstacle to choice really just boils down to excluded middle. (Probably—again it’s really difficult to combine mutable state with other stuff in pure math.)
I am not an expert, but I think solutions like this have a potential of hitting an infinite recursion, if evaluating some expression inside the code somehow indirectly invokes the axiom of choice, for example if you construct an object specifically for that purpose.
I don’t think you run into this problem.
My understanding of the axiom of choice, and the axioms in general, is that instead of merely describing how things work, they are describing what things are are talking about (by describing how they work). There are multiple concepts (in the Platonic realm) you could plausibly mean when you use the word “set”.
The axiom of choice says “I only mean those models that have the property that for any set of sets, there is a selection that works like this, and the selection itself is included in the model of ‘sets’”. There are models that follow the remaining axioms and have the property, and also models that follow the remaining axioms and don’t have the property.
Yes, there are two places where that shows up in my comment. First, “if math allowed mutable state” is a condition on the concepts one might be referring to, as usually those concepts don’t allow mutable state. (In fact combining sets and mutable state is probably the hardest part, because e.g. what does it mean to take a subset {x \in S | phi(x) } if phi might mutate some state as a side-effect?) Secondly, my “proof” reduces the axiom of choice to excluded middle, and excluded middle is again a feature that you might or might not have in your mathematical universe.
If math allowed mutable state, we could reduce the axiom of choice to excluded middle:
This relies on excluded middle because the ability to check whether an index is in the cache and if so look it up requires the ability to compare indices by equality.
(Sampling from family(index) is legit. The axiom of choice asserts that dependent products commute with propositional truncation. Propositional truncation does not destroy the computational content of the realizers of the family, it just quotients the realizers to be equal for when it comes to determining the well-definedness of functions. Since we use a cache, the resulting choice_fn still respects equality.
This isn’t valid type theory of course, since type theory has models that don’t permit this stuff and requires propositional truncation to be explicit.)
I think of this as a sort of converse of Diaconescu’s theorem.
This isn’t actually how the effective topos gets countable choice. Instead I believe the effective topos relies on the fact that realizers of functions out of
I assume
familyhere is a function that accepts an index and returns a nonempty set? But then it seems that for the first encountered index the choice function will just return a set rather than an element from it, no? Or am I misreading something?familyis a function that witnesses the “nonemptiness” (really, mere inhabitedness) by returning an element of the propositional truncation of the set. So more formally,axiom_of_choicehas type(Πi: I. ||F(i)||) → ||Πi: I. F(i)||. The “choice” comes from the fact thatfamily(due to the propositional truncation) is allowed to return differentF(i)’s from identicali’s, whereaschoice_fnis required to choose a canonicalF(i)for eachi. (The intermediate results are untyped because this is a realizer, not a typed term in a type theory.)😅 This explanation is, I assume, not very helpful to anyone who doesn’t already know what’s going on. But basically in type theory, propositions correspond to (propositionally truncated) types, and proofs correspond to programs/terms with the types in question, so in proving the nonemptiness of the sets, you automatically end up with a witness function that picks out elements—except the witness function may be “nondeterministic” (that’s where the propositional truncation comes in), which is what requires choice to fix.
The propositional truncation is important to understand. There is a version of type theory’s logic that doesn’t include propositional truncation, but in it the axiom of choice is trivial to prove and not really of any use. Unfortunately the intuitive way to explain propositional truncation gives catastrophically wrong intuition for my use-case, as explained here: https://mathstodon.xyz/@MartinEscardo/111014413939196037
I am not an expert, but I think solutions like this have a potential of hitting an infinite recursion, if evaluating some expression inside the code somehow indirectly invokes the axiom of choice, for example if you construct an object specifically for that purpose.
My understanding of the axiom of choice, and the axioms in general, is that instead of merely describing how things work, they are describing what things are are talking about (by describing how they work). There are multiple concepts (in the Platonic realm) you could plausibly mean when you use the word “set”.
The axiom of choice says “I only mean those models that have the property that for any set of sets, there is a selection that works like this, and the selection itself is included in the model of ‘sets’”. There are models that follow the remaining axioms and have the property, and also models that follow the remaining axioms and don’t have the property.
I guess to add, the thing about constructive math (which avoids excluded middle and unrestricted choice) is that it permits models where everything is computational. What I hope I’ve shown is that in some such models, the obstacle to choice really just boils down to excluded middle. (Probably—again it’s really difficult to combine mutable state with other stuff in pure math.)
I don’t think you run into this problem.
Yes, there are two places where that shows up in my comment. First, “if math allowed mutable state” is a condition on the concepts one might be referring to, as usually those concepts don’t allow mutable state. (In fact combining sets and mutable state is probably the hardest part, because e.g. what does it mean to take a subset {x \in S | phi(x) } if phi might mutate some state as a side-effect?) Secondly, my “proof” reduces the axiom of choice to excluded middle, and excluded middle is again a feature that you might or might not have in your mathematical universe.