IntroductionTetheringCut and Identity for the Tethered Sequent CalculusFrom JS4 to Tethered Sequent CalculusFrom Tethered Sequent Calculus to JS4Tethered Natural DeductionLecture Notes onTethered Semantics15-816: Modal LogicFrank PfenningLecture 17March 25, 20101 IntroductionIn this lecture we continue our search for a multiple-world semantics forthe intutionistic logic of validity and possibility, dubbed JS4. As we haveseen in the previous lecture, the fragment without possibility, disjunction,and falsehood has a sound and complete semantics with IS4. Once thoseare added, however, the IS4 semantics proves too many propositions. Forexample, the IS4 axiom (or theorem) ♦(A∨B) ⊃ ♦A∨♦B requires a decisionhere about a disjunction which is only known to be true at some reachableworld. The objection lodged by JS4 can also be understood if we interpretreachability in a temporal way. In that case, the above proposition wouldmean that we have to make a decision now based on information that willonly be available to us in the future.One solution, which will also be useful later when we discuss the modalinterpretation of so-called substructural logics, is to give a mixed semanticswhich employs both multiple judgments and worlds. We will take greatcare to make sure all actions in this logic are local. It turns out that this isenough to rule out temporal paradoxes such as the one above and obtain asemantics that is both sound and complete for JS4. This lecture is based onjoint work with William Lovas and Jason Reed.2 TetheringThe basic idea of the tethered sequent calculus is that there is a currentworld, namely the world associated with the proposition on the right-handLECTURE NOTES MARCH 25, 2010L17.2 Tethered Semanticsside of the sequent, and that all left rules are restricted to take place inthe current world. The name “tether” derives from the intuition that theproposition on the left are tied to the current world on the right.For the ordinary intuitionistic connectives, tethering is completely straight-forward. We have two judgments: A is true at world w which can be eitherin the antecedent or succedent of the sequent.P @w ∈ ΓΓ =⇒ P @ winitΓ, A@w =⇒ B @ wΓ =⇒ A ⊃ B @ w⊃RΓ, A ⊃ B@w =⇒ A @ w Γ, A ⊃ B@w, B@w =⇒ C @ wΓ, A ⊃ B@w =⇒ C @ w⊃LΓ =⇒ A @ wΓ =⇒ A ∨ B @ w∨R1Γ =⇒ B @ wΓ =⇒ A ∨ B @ w∨R2Γ, A ∨ B@w, A@w =⇒ C @ w Γ, A ∨ B@w , B@w =⇒ C @ wΓ, A ∨ B@w =⇒ C @ w∨Lno ⊥R Γ, ⊥@w =⇒ C @ w⊥LFigure 1: Tethered sequent calculus, fragment with ⊃, ∨, ⊥When we try to tether the modal operators, however, we find somedifficulties. For example, with the rulesΓ, w ≤ α =⇒ A @ αΓ =⇒ A @ w Rα?Γ≤` w ≤ w0Γ, A@w, A@w0=⇒ C @ wΓ, A@w =⇒ C @ w L?the identity principle fails: after A@h =⇒ A @ α A@h =⇒ A @ h Rαthe left rule cannot be applied to the assumption A@h because h 6= α.LECTURE NOTES MARCH 25, 2010Tethered Semantics L17.3Perhaps surprisingly, the solution is to eliminate accessibility altogether.This goes back to the time we introduced the modal logic of validity, wherewe mentioned multiple worlds, but we did not mention accessibility (nordid it seem to come up). However, this does require us to introduce a newjugment which we write A ! which means that A is true in all worlds. Wethen haveΓ =⇒ A @ αΓ =⇒ A @ w RαΓ, A@w, A ! =⇒ C @ wΓ, A@w =⇒ C @ w LΓ, A !, A@w =⇒ C @ wΓ, A ! =⇒ C @ wcopyIn the R rule, α must be a new world parameter, and would make senseto make this explicit as a hypothesis α world. We elide these additionalassumptions.The judgmental rule copy is also tethered in the sense that the new hy-pothesis A@w must be at the current world, even though A ! is universal.We make a similar adjustment to the rules for possibility. We have anew judgment A ? w which means that A is possible at w.Γ =⇒ A ? wΓ =⇒ ♦A @ w♦RΓ, ♦A@w, A@α =⇒ C ? αΓ, ♦A@w =⇒ C ? w♦LαΓ =⇒ A @ wΓ =⇒ A ? whereIn the ♦L rule, we use the assumption ♦A@w to show that C is possibleat w by moving to a new world α where A is true and showing that C ispossible there. So tethering affects both the conclusion and the premise.Now we have to generalize the previous rules left rules to permit a con-clusion A @ w or A ? w. We write “∗” for a variable which is either “@” or“?”. The rules are summarized in Figure2.One interesting aspect of the tethered sequent calculus is that all hy-potheses are persistent: once made, they will be in the context for the restof the proof (constructed bottom-up). In contrast, in JS4 the R rule clearsthat truth context, because truth cannot be used in the proof of validity.This means that this calculus is well-suited for implementation in logicalframeworks based on hypothetical judgments such as LF.In the example below we have elided assumptions that are no longerLECTURE NOTES MARCH 25, 2010L17.4 Tethered SemanticsP @w ∈ ΓΓ =⇒ P @ winitΓ, A@w =⇒ B @ wΓ =⇒ A ⊃ B @ w⊃RΓ, A ⊃ B@w =⇒ A @ w Γ, A ⊃ B@w, B@w =⇒ C ∗ wΓ, A ⊃ B@w =⇒ C ∗ w⊃LΓ =⇒ A @ wΓ =⇒ A ∨ B @ w∨R1Γ =⇒ B @ wΓ =⇒ A ∨ B @ w∨R2Γ, A ∨ B@w, A@w =⇒ C ∗ w Γ, A ∨ B@w , B@w =⇒ C ∗ wΓ, A ∨ B@w =⇒ C ∗ w∨Lno ⊥R Γ, ⊥@w =⇒ C ∗ w⊥LΓ =⇒ A @ αΓ =⇒ A @ w RαΓ, A@w, A ! =⇒ C ∗ wΓ, A@w =⇒ C ∗ w LΓ, A !, A@w =⇒ C ∗ wΓ, A ! =⇒ C ∗ wcopyΓ =⇒ A ? wΓ =⇒ ♦A @ w♦RΓ, ♦A@w, A@α =⇒ C ? αΓ, ♦A@w =⇒ C ? w♦LαΓ =⇒ A @ wΓ =⇒ A ? whereFigure 2: Tethered sequent calculus, ∗ ∈ {@, ? }LECTURE NOTES MARCH 25, 2010Tethered Semantics L17.5needed (despite the fact that all are persistent).A@α =⇒ A @ αinitB@α =⇒ B @ αinitA ⊃ B@α, A@α =⇒ B @ α⊃L(A ⊃ B) !, A@α =⇒ B @ αcopy(A ⊃ B) !, A@α =⇒ B ? αhere(A ⊃ B) !, ♦A@h =⇒ B ? h♦L(A ⊃ B) !, ♦A@h =⇒ ♦B @ h♦R (A ⊃ B)@h, ♦A@h =⇒ ♦B @ h L=⇒ (A ⊃ B) ⊃(♦A ⊃ ♦B) @ h⊃I × 2We can also try a counterexample to the completeness of JS4 with respectto IS4: after one step♦(A ∨ B)@h =⇒ ♦A ∨ ♦B @ h=⇒ ♦(A ∨ B) ⊃ ♦A ∨ ♦B @ hwe are stuck, because ♦L requires the succedent to have the form C ? hwhich it does not.In general, there seems to be a really close correspondence betweenproof in the sequent calculus in JS4 and its tethered semantics. Before weestablish that, we should verify the internal properties of the tethered