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).