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