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.
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.