## Hierarchical sequents

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

## Modal rules

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 BB_{i}φ^{-} 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.

## Example

As an example consider a derivation of the K-distribution 'axiom': K_{1} (a → b) → ( K_{1} a → K_{1} b).
For brevity reasons the unused formulas are not included.

Graphically:

Including all unused formulas the left application of the axiom is to