Jason (jcreed) wrote,

Damn it.

Found what might be construed as a counterexample to a cherished informal principle I love to use as a rule of thumb: first, fix a cut principle; (i.e., choose what you mean by cut elimination) Now if two connectives you are thinking of have the same left rule but different right rules (symmetrically, if they have the same right rule but different left rules) one of them is wrong.

The counterexample comes from proof irrelevance. I was going back and looking at the Awodey-Bauer paper, and got to thinking about how their modality is idempotent, while the Pfenning'01 triangle (as found in Ruy's and his stuff from '06 too) is not. I figured one of two things must be the case: (a) there is a way to adapt whatever made the Awodey-Bauer triangle idempotent to a more strictly judgmental setting, in which case it would have the same promotion-based right rule as does Pfenning's, but you'd have to choose a different cut principle, or (b) there just ain't.

Apparently I was wrong. (a) is half true --- you have the same right rule as usual, and you just make the left rule such that it lets you decompose triangle under a divides, like
Γ, y ÷ A ⊦ M : C

Γ, x ÷ △A ⊦ let tri y = x in M : C

but the (irrelevant) cut principle is infuriatingly the same! It's still
Γ ⊦ N : A      Γ, x ÷ A ⊦ M : C

Γ ⊦ [N/x]M : C

Weirdly, if you have both the idempotent and nonidempotent triangle modalities in a system simultaneously, the nonidempotent one fails cut-elimination: the only reason its cut-elimination proof works is that, ordinarily, you can rule out one funny case where you would be decomposing a connective under a ÷ — which is exactly what the idempotent one does.

To put it another way, picture the cartesian product of all the rules that could have been used to derive the two derivations going into a cut. The commutative cases paint vertical and horizontal stripes across this picture. When we think about the case where D :: Γ ⊦ N : A was derived using △L, the only cases left "unpainted" for E :: Γ, x ÷ A ⊦ M : C are ones where the principal formula is introduced. But we lack any rules (in the fully nonidempotent system) that would do such a thing, so we're done.

For this reason I have to think idempotent △ is the "more right" of the two. Even though the traditional (at least the traditions I've been brought up with :) one still works by itself, it seems more fragile. I might somehow weasel out of this by saying that restrictions on which judgments are open to decomposition changes the meaning of the cut principle per se but I haven't warmed up to this explanation yet.

Maybe there's just a Reverse Logical Gresham's Law operating here, that good connectives drive out the bad...
Tags: math, proof irrelevance, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded