November 4th, 2012

(no subject)

There's three kinds of equivalence of logical systems (or portions of them) that keep recurring --- at least in the course my research life, anyway. The idea of stratifying weaker and stronger equivalences is rife in mathematics in general, and in the case of logics specifically, I think maybe Girard sketched some out long ago, but I can't find the reference at the moment. I know Nigam and Miller described some in this '09 Journal of Automated Reasoning paper. They call them relative completeness, (when two proof systems prove the same set of propositions) full completeness of proofs, (when two proof systems have bijectively corresponding sets of proofs) and full completeness of (open) derivations (when two proof systems have isomorphic partial proofs)

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

1. Coming up with another logic L3
2. Figuring out translations # : L1 → L3 and \$ : L2 → L3
3. 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.