In modal logic reasoning about just truth and falsehood is no longer sufficient. A formula φ can be true in one world and false in another, we have to take worlds into account. Our sequents as defined previously have no such notion.
To do this we will create a tree of sequents, one for each set of worlds that we consider. The root of this tree will correspond to all worlds, while a child corresponds only to worlds reachable by a certain agent. We write down this tree as a hierarchical sequent.
Definition: A hierarchical sequent is a set of signed formulas and nested hierarchical sequents. We use the notation [Γ]i for a nested sequent that represents a world reachable by agent i.
To give a concrete example consider the hierarchical sequent
This hierarchical sequent corresponds directly to the formula p ∨ □1((q ∧ ¬p) ∨ p) ∨ □2(¬q). We can also draw the sequent in a graph that looks very much like a model:
The arrows go to arbitrary worlds, so in the image if we manage to proof q- for this arbitrary world on the right we have indeed shown that q- must be true in all worlds reachable by agent 2.
Semantically nested sequents behave the same as the □ operator. The difference is that a nested sequent contains a whole set of signed formulas and nested sequents, not just a single subformula.
There is now a minor technical problem: how do we work with these sequents? We are not allowed to use any rules 'inside' nested sequents, while out intention is that that is possible. To work around this problem we introduce the deep application meta-rules:
These meta-rules allow us to apply rules and axioms inside nested sequents, any rule that can turn a sequent inside brackets from Γ into Δ can now also work on [Γ]i, turning it into [Δ]i.
With hierarchical sequents the rule for the modal box operator becomes simple
Semantically the sequent above and below the line are exactly the same.
On its own the box rule is not very useful, we can not use it to prove more interesting modal formulas. These formulas will also contain negatively occurring boxes (or positive diamonds). What does □i φ- mean? It means that there is a world in which φ does not hold. Since any world will do, so will the arbitrary world from the positive box rule. If we can show φ- in that world the proof is complete. So all we have to do is add φ- to the each nested sequent:
Note that in this rule it becomes important to keep a copy of the BBiφ- formula. The reason is that there might be more than one nested sequent and we need to add φ- to each of them. To avoid problems with non-termination we require that φ+ ∉ Δ before the rule is applied.
As an example consider a derivation of the K-distribution 'axiom': K1 (a → b) → ( K1 a → K1 b). For brevity reasons the unused formulas are not included.
Including all unused formulas the left application of the axiom is to