## October 28th, 2012

### (no subject)

People walk by, cars drive by, and it all happens while the reporters are stressing that people absolutely should not be outside. It's basically like watching a wildlife expert talk about how you should never taunt an angry bear while somebody in the background runs across the screen being chased by a grizzly and yelling, "You want the sandwich? You want the sandwich? Come and get it, ha ha ha!"

http://www.npr.org/blogs/monkeysee/2011/08/29/140032831/why-did-i-watch-fourteen-hours-of-the-weather-channel-im-not-sure

### (no subject)

So wins again at the game of discovering that certain fairly long-held mathematical beliefs of mine are totally false. The last one was a certain technical lemma in a paper I wrote (but did not publish) with Frank, and repairing it was extremely instructive --- I realized that Belnap's display property is actually completely essential to focusing working right.

Today's example is that Pfenning-Davies modal box and Simpson modal box are not equivalent even if you don't allow diamond! Well, at least if you do allow falsehood. Rob's counterexample is what you get if you take (⋄A ⇒ □B) ⇒ □(A ⇒ B) --- which simpson proves, and pfenning-davies does not --- and replace the diamond with a demorganized-box:

(¬□¬A ⇒ □B) ⇒ □(A ⇒ B)

which simpson also proves, and which pfenning-davies still does not.

Actually, as long as we're allowing falsehood/negation, this can be simplified to the question of whether necessary negations behave like negations with respect to Brouwer's theorem:

¬¬□¬A ⇒ □¬A

So the only thing left that's feasible to try to prove is that "classical pfenning-davies" is the same as "classical simpson". This is pretty much exactly what these notes refer to as the "soundness of labeled deduction" at the end of section 6.2, and for which they appeal to semantic Kripke-model-ish proofs to prove. Blech, semantics!

But the purely syntactic proof in Simpson's thesis --- the one that he uses to show that any labelled (intuitionistic) proof has a Hilbert proof --- seems to extend nicely to showing that any labelled classical proof has a classical Pfenning-Davies proof. The trick is considering the Simpson sequents whose labels form a tree. For each such sequent S there is a single proposition, call it S*, that (in Simpson) asynchronously unpacks to S. The induction hypothesis is: if simpson proves S, then Pfenning-Davies proves |- S*. Then you just plod along checking that each Simpson inference rule is sound under that propositional reification.

An example of this reification is as follows. Suppose the "initial" world x can see worlds y and w, and world y can see world z. If S is the (classical) Simpson sequent
 ⊢ A @ x, B @ y, C @ y, D @ z, E @ w (1)

then S* is
 A v □(B v C v □D) v □E (2)

what we're doing is just sticking a box in around every subtree of the world-tree, and turning all commas into disjunctions. Observe that starting backwards proof-search from (2) at world x does indeed produce (1) in Simpson's proof theory.

An interesting thing to note is this proof very clearly fails if you try to throw in first-order quantifiers, precisely because forall fails to commute with "A v" (in the sense that ∀x.A v B(x) ⊢ A v ∀x.B(x) fails) and with □ (in the sense that Barcan's formula fails in PD).