But I don't think these are exactly the three I keep coming across, though maybe two of them are. I feel inclined to call two propositions A and B (maybe which live in different proof systems) equiprovable (write it as A ⇔ B) if I know
⊢ A if and only if ⊢ B
so Nigam-Miller's notion relative completeness is a statement about every proposition being equiprovable in one proof system relative to another.
I want to call A and B (which maybe live in different proof systems) focally equivalent (write it as A ≅ B) if I have a bijection on proofs
(⊢ A) ↔ (⊢ B)
so Nigam-Miller's notion full completeness on proofs is a statement about every proposition in one proof system having a focally equivalent partner in the other.
But also I want to call two propositions A and B (in the same proof system) interprovable when I know
A ⊣⊢ B
whose relevance to Nigam-Miller's classification, Idunno what it is.
The point of saying all this is that my favorite thing to do lately is take a theorem about two logics, call them L1 and L2, that says that merely A ⇔ B (for any "suitably corresponding" propositions A that live in L1 and B that lives in L2) strengthening this by
- Coming up with another logic L3
- Figuring out translations # : L1 → L3 and $ : L2 → L3
- Proving A ≅ A# ⊣⊢ B$ ≅ B
The reason I like this is that it feels like revealing that L1 and L2 are both "really just subsets" of L3, and L3 "knows internally" (in the sense of interprovability) that they are equivalent.
Which is to say, I almost thought I woke up with the kernel of such a proof in my head for classical Pfenning-Davies vs. classical Simpson, but it turned out not to work. SO CLOSE.