Now, where did the weirdness come from here. Well, to me it seems clear that really it came from the fact that the reals can be built out of a bunch of shifted rational numbers, right? But everyone agrees about that.
I do not think everyone agrees about that! I think that people who reject AoC would say “sure, any real number can be a shifted rational, but not all of them, there’s just no reasonable procedure which does this for the entire set at once.”
Yeah that’s probably right. But then there’s introducing this weird distinction between “I can do it for any x” and “I can do it for all x.”
It quickly becomes pretty philosophical at that point, about whether you think there’s a distinction there or not. I guess my claim in this post is more like “working mathematicians in fields outside of foundations have collectively agreed on an answer to this philosophical puzzle, and that answer is actually quite defensible.”
If you write me a function of type (a→⊥)→⊥, I can point out the place in its source code where you included a value of type a, but I can’t write a function of type ((a→⊥)→⊥)→a.
I think I must’ve not paid enough attention in type theory class to get this? Is this an excluded middle thing? (if it’s a joke that I’m ruining by asking this feel free to let me know)
Look, there’s an integer! It’s right there, “4”. Apparently Int is inhabited.
bar :: ((a→⊥)→⊥)→a bar fo = ???
There’s nothing in particular to be done with fo… if we had something of type a→⊥ to give fo, we would be open for business, but we don’t know enough about a to make this any easier than coming up with a value of type ⊥, which is a non-starter.
I am giving an example of something I can do “for any x” but not “for all x”. In the first case, the x is given in a fully constructed, reified form, and I can look at its internals to build a bespoke response. In the second case, I would have to give a general procedure that can work with all x while interacting with the x only by means of its external interface.
Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.
I do not think everyone agrees about that! I think that people who reject AoC would say “sure, any real number can be a shifted rational, but not all of them, there’s just no reasonable procedure which does this for the entire set at once.”
Yeah that’s probably right. But then there’s introducing this weird distinction between “I can do it for any x” and “I can do it for all x.”
It quickly becomes pretty philosophical at that point, about whether you think there’s a distinction there or not. I guess my claim in this post is more like “working mathematicians in fields outside of foundations have collectively agreed on an answer to this philosophical puzzle, and that answer is actually quite defensible.”
If you write me a function of type (a→⊥)→⊥, I can point out the place in its source code where you included a value of type a, but I can’t write a function of type ((a→⊥)→⊥)→a.
I think I must’ve not paid enough attention in type theory class to get this? Is this an excluded middle thing? (if it’s a joke that I’m ruining by asking this feel free to let me know)
foo :: (Int→⊥)→⊥
foo f = f 4
Look, there’s an integer! It’s right there, “4”. Apparently Int is inhabited.
bar :: ((a→⊥)→⊥)→a
bar fo = ???
There’s nothing in particular to be done with fo… if we had something of type a→⊥ to give fo, we would be open for business, but we don’t know enough about a to make this any easier than coming up with a value of type ⊥, which is a non-starter.
Sorry, I think explaining without using type theory what you are trying to say may help me understand better?
EDIT: like, in particular, insofar as its relevant to the axiom of choice.
I am giving an example of something I can do “for any x” but not “for all x”. In the first case, the x is given in a fully constructed, reified form, and I can look at its internals to build a bespoke response. In the second case, I would have to give a general procedure that can work with all x while interacting with the x only by means of its external interface.
Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.
I can come-up-with-math-to-model any problem, but I can’t come-up-with-math-to-model all problems, by diagonalization.
Well put! I guess if I can define a function from problems to math-to-model-it, then for every problem I can pick out the right math-to-model-it?
Or, indeed, perhaps not? ;)