Timeline for Axiom of Computable Choice versus Axiom of Choice
Current License: CC BY-SA 2.5
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 27, 2010 at 5:58 | comment | added | Carl Mummert | Diaconescu's theorem only uses sets that are classically subsets of {0,1}. So the limited types cannot be the only factor making AC constructive in the context of arithmetic. Trying to formalize the proof of Diaconescu's theorem from Wikipedia in HA, instead of forming sets U and V, we have to make a function G with G(0) = χ_U and G(1) = χ_V. It appears this is not always possible. Even if it is, we can apply AC_{00} (!) with G as a parameter. In the choice function f(x), f(0) and f(1) may differ even if G(0) and G(1) are extensionally the same. In IZF, if U = V then f(U) has to equal f(V). | |
| May 27, 2010 at 5:26 | comment | added | Carl Mummert | I have always read Bishop's statements as saying that, but there may be some other writings I have not seen in which he clarifies his opinion. Since Bishop's book doesn't choose any particular formalism, it's possible to interpret it in many formal systems, and I'm biased because the first interpretation I learned for it was HA^\omega. I will have to use a separate comment to respond about something about AC. | |
| May 27, 2010 at 0:47 | comment | added | Andrej Bauer | @Carl: Thanks for mentioning higher-order arithmetic. But I was not "glossing over" it, I simply did not mention it. Are you saying that according to Bishop's understanding of mathematics, choice at higher arithmetical types is valid (in an absolute sense)? I would say the consistency of choice with higher-order arithmetic is an accident caused by the fact that only very special sets, namely $\mathbb{N}$, $\mathbb{N}^\mathbb{N}$, $\mathbb{N}^{\mathbb{N}^\mathbb{N}}$, ..., are available in the theory. | |
| May 26, 2010 at 15:00 | comment | added | Carl Mummert | I think you are glossing over the difference between choice in topos theory and choice in theories of higher-order arithmetic such as HA^\omega. In the latter context, the full choice scheme for higher-order arithmetic in all finite types is constructively valid. I don't think that qualifies as "countable and dependent choice". This complete acceptance of choice is inherent in Bishop's quote, "a choice is implied by the very meaning of existence". There is no difference between AC_{0,0} and AC_{15,19} from that perspective. | |
| May 23, 2010 at 20:15 | comment | added | Joel David Hamkins | +1. Thanks, Andrej, I thought you would show up with some constructivist ideas. | |
| May 23, 2010 at 19:44 | comment | added | Halfdan Faber | Andrej, Thank you for the elaboration. Also a great answer to a not so good question. | |
| May 23, 2010 at 18:32 | history | answered | Andrej Bauer | CC BY-SA 2.5 |