Jason (jcreed) wrote,

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: logic, math

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment