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.
Tags:
• #### (no subject)

After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

• #### (no subject)

Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

• #### (no subject)

Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic

Your reply will be screened

Your IP address will be recorded

• 1 comment