Hmm, I’m trying to follow your argument, but I can’t immediately think of what double-negated axiom of choice would look like.
Like type-theoretically, to me, axiom of choice looks something like:
aoc:(Πx:A.||Bx||)→(||Πx:A.Bx||)
… where ||−|| is propositional truncation (which computationally you can think of as allowing functions to be nondeterministic; so axiom of choice states that if you have a nondeterministic function, you can nondeterministically pick a deterministic function). Where would we be putting the double-negation to translate it from classical to constructive? Usually implications/functions are unaffected by DNE translation, so the only option I can think of would be to DNE the propositional truncations, but dunno that this is the appropriate choice.
More generally, part of the beauty in the double-negation translation is that all of classical logic is valid under it. So if Alice makes some classical proof, then Bob can just translate that proof with double negations, and then the translated argument will be valid to Bob IFF it was valid to Alice.
(I think this is less feasible in the other direction? Like provability may be one model of constructive logic, sort of (I think you are more thinking about realizability? which is sort of complicated), but it is not the only one and not a universal one. But from the perspective of classical logic, plopping in double negations makes no difference, so any argument Bob makes is an argument that Alice would still accept.)
As I mentioned here, if Alice understands your point about the power of the double-negation formulation, she would be applying a different translation of Bob’s statements from the one I assumed in the post, so she would be escaping the problem. IE:
part of the beauty in the double-negation translation is that all of classical logic is valid under it.
is basically a reminder to Alice that the translation back from double-negation form is trivial in her own view (since it is classically equivalent), and all of Bob’s intuitionistic moves are also classically valid, so she only has to squint at Bob’s weird axioms, everything else should be understantable.
But I think things will still get weird if Bob makes meta-logical arguments (ie Bob’s arguments are not just proofs in Bob’s logic), which seems quite probable.
But I think things will still get weird if Bob makes meta-logical arguments (ie Bob’s arguments are not just proofs in Bob’s logic), which seems quite probable.
But in that case Bob’s meta-logic might be compatible with Alice’s meta-logic. For instance usually I see practical constructive mathematicians work in a neutral or classical meta-logic. If Alice and Bob share a meta-logic, then they can easily talk about the models of the object logic in the shared meta-logic.
Hmm, I’m trying to follow your argument, but I can’t immediately think of what double-negated axiom of choice would look like.
Like type-theoretically, to me, axiom of choice looks something like:
aoc:(Πx:A.||Bx||)→(||Πx:A.Bx||)
… where ||−|| is propositional truncation (which computationally you can think of as allowing functions to be nondeterministic; so axiom of choice states that if you have a nondeterministic function, you can nondeterministically pick a deterministic function). Where would we be putting the double-negation to translate it from classical to constructive? Usually implications/functions are unaffected by DNE translation, so the only option I can think of would be to DNE the propositional truncations, but dunno that this is the appropriate choice.
More generally, part of the beauty in the double-negation translation is that all of classical logic is valid under it. So if Alice makes some classical proof, then Bob can just translate that proof with double negations, and then the translated argument will be valid to Bob IFF it was valid to Alice.
(I think this is less feasible in the other direction? Like provability may be one model of constructive logic, sort of (I think you are more thinking about realizability? which is sort of complicated), but it is not the only one and not a universal one. But from the perspective of classical logic, plopping in double negations makes no difference, so any argument Bob makes is an argument that Alice would still accept.)
More on axiom of choice: https://math.stackexchange.com/a/4782176/315043
As I mentioned here, if Alice understands your point about the power of the double-negation formulation, she would be applying a different translation of Bob’s statements from the one I assumed in the post, so she would be escaping the problem. IE:
is basically a reminder to Alice that the translation back from double-negation form is trivial in her own view (since it is classically equivalent), and all of Bob’s intuitionistic moves are also classically valid, so she only has to squint at Bob’s weird axioms, everything else should be understantable.
But I think things will still get weird if Bob makes meta-logical arguments (ie Bob’s arguments are not just proofs in Bob’s logic), which seems quite probable.
But in that case Bob’s meta-logic might be compatible with Alice’s meta-logic. For instance usually I see practical constructive mathematicians work in a neutral or classical meta-logic. If Alice and Bob share a meta-logic, then they can easily talk about the models of the object logic in the shared meta-logic.
Yeah. For my case, I think it should be assumed that the meta-logics are as different as the object-logics, so that things continue to be confusing.