How the rules of a tableau act on the two components

This file collects the facts about the rules of a (split) tableau that the facts about a proper cluster in Pdl.ClusterFacts are proved from:

• vocabulary preservation (Lemma 9.2): along the tableau the vocabulary of each of the two components only shrinks;
• right rules do not change the left component, and left rules do not change the right component (provided the loaded formula is on the right);
• a node with a coarse child loaded on the right is itself loaded on the right, and a node with children applies a left or a right rule;
• loaded-path repeats and the Dershowitz-Manna measure: going down along left rules strictly decreases the label.

Entailment from the left component of a node

def FinePathIn.leftEntails {Hist : History} {Y : Sequent} {tab : Tableau Hist Y} (t : FinePathIn tab) (φ : Formula) : Prop

Λ₁(t) ⊨ φ: the formula φ follows from the left component of the fine node t.

Equations

• t.leftEntails φ = ∀ (W : Type) (M : KripkeModel W) (w : W), (∀ ψ ∈ t.label.left, evaluate M w ψ) → evaluate M w φ

Vocabulary preservation

Lemma 9.2 of the paper: along the tableau the vocabulary of each of the two components only shrinks. "By inspection of the rules": for local rules this is localRule_does_not_increase_vocab_L and localRule_does_not_increase_vocab_R, and for the PDL rules we check the six cases directly.

theorem mem_fvoc_iff {L : Finset Formula} {x : ℕ ⊕ ℕ} : x ∈ L.fvoc ↔ ∃ φ ∈ L, x ∈ φ.voc

Membership in the vocabulary of a Finset of formulas. This is Finset.mem_fvoc from Pdl/Interpolation/Local.lean.

theorem Sequent.left_fvoc_eq_of_eq {X Y : Sequent} (h : X = Y) : X.left.fvoc = Y.left.fvoc

Since sequents now use Finsets, being "set equal" is just being equal.

theorem Sequent.right_fvoc_eq_of_eq {X Y : Sequent} (h : X = Y) : X.right.fvoc = Y.right.fvoc

Since sequents now use Finsets, being "set equal" is just being equal.

theorem LocalRuleApp.left_fvoc_subset (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → Y.left.fvoc ⊆ lra.X.left.fvoc

A local rule application does not increase the vocabulary of the left component. This is the left half of localRuleApp_does_not_increase_jvoc.

theorem LocalRuleApp.right_fvoc_subset (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → Y.right.fvoc ⊆ lra.X.right.fvoc

A local rule application does not increase the vocabulary of the right component. This is the right half of localRuleApp_does_not_increase_jvoc.

theorem LocalPathIn.last_left_fvoc_subset {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp.last.left.fvoc ⊆ X.left.fvoc

Inside a local tableau the vocabulary of the left component only shrinks.

theorem LocalPathIn.last_right_fvoc_subset {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp.last.right.fvoc ⊆ X.right.fvoc

Inside a local tableau the vocabulary of the right component only shrinks.

theorem endNodesOf_left_fvoc_subset {X : Sequent} (lt : LocalTableau X) (Y : Sequent) : Y ∈ endNodesOf lt → Y.left.fvoc ⊆ X.left.fvoc

theorem endNodesOf_right_fvoc_subset {X : Sequent} (lt : LocalTableau X) (Y : Sequent) : Y ∈ endNodesOf lt → Y.right.fvoc ⊆ X.right.fvoc

theorem projection_fvoc_subset (A : ℕ) (L : Finset Formula) : (Finset.projection A L).fvoc ⊆ L.fvoc

theorem PdlRule.left_fvoc_subset {X Y : Sequent} (r : PdlRule X Y) : Y.left.fvoc ⊆ X.left.fvoc

A PDL rule does not increase the vocabulary of the left component.

theorem PdlRule.right_fvoc_subset {X Y : Sequent} (r : PdlRule X Y) : Y.right.fvoc ⊆ X.right.fvoc

A PDL rule does not increase the vocabulary of the right component.

theorem edge_left_fvoc_subset {H : History} {Z : Sequent} {tab' : Tableau H Z} {s t : PathIn tab'} (h : s ⋖_ t) : (nodeAt t).left.fvoc ⊆ (nodeAt s).left.fvoc

theorem edge_right_fvoc_subset {H : History} {Z : Sequent} {tab' : Tableau H Z} {s t : PathIn tab'} (h : s ⋖_ t) : (nodeAt t).right.fvoc ⊆ (nodeAt s).right.fvoc

theorem cEdge_left_fvoc_subset {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ◃ t) : (nodeAt t).left.fvoc ⊆ (nodeAt s).left.fvoc

theorem cEdge_right_fvoc_subset {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ◃ t) : (nodeAt t).right.fvoc ⊆ (nodeAt s).right.fvoc

theorem cReach_left_fvoc_subset {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ◃* t) : (nodeAt t).left.fvoc ⊆ (nodeAt s).left.fvoc

Lemma 9.2, left component: along ◃ the vocabulary only shrinks.

theorem cReach_right_fvoc_subset {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ◃* t) : (nodeAt t).right.fvoc ⊆ (nodeAt s).right.fvoc

Lemma 9.2, right component: along ◃ the vocabulary only shrinks.

theorem FinePathIn.label_left_fvoc_subset_base {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : f.label.left.fvoc ⊆ (nodeAt f.base).left.fvoc

The label of a fine node has a smaller vocabulary than the coarse node it lies in.

theorem FinePathIn.label_right_fvoc_subset_base {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : f.label.right.fvoc ⊆ (nodeAt f.base).right.fvoc

Right rules do not change the left component

The two "right" local rules only act on the right component and on a loaded formula on the right, so they leave the left component of the sequent unchanged. The (M) rule does change the left component, but it is a Tableau.pdl step and hence only applies to a basic sequent, whose right component is then basic as well.

theorem LocalRuleApp.left_eq_of_isRightRule (lra : LocalRuleApp) (h : lra.isRightRule = true) (Y : Sequent) : Y ∈ lra.C → Y.left = lra.X.left

theorem Sequent.basic_rightOnly {X : Sequent} (h : X.basic) : X.rightOnly.basic

The right component of a basic sequent is basic.

theorem FinePathIn.lra_or_basic_of_usesRightRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : f.usesRightRule = true → (∃ (lra : LocalRuleApp), f.lra? = some lra ∧ lra.isRightRule = true) ∨ f.label.basic

Where a right rule is applied, it is either a local rule or the node is basic (because the (M) rule is only applied at basic nodes).

theorem FinePathIn.children_left_eq_of_usesRightRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (hr : f.usesRightRule = true) (hb : ¬f.label.rightOnly.basic) (g : FinePathIn tab') : g ∈ f.children → g.label.left = f.label.left

At a node where a right rule is applied to a non-basic right component, all children have the same left component as the node itself.

theorem LocalRuleApp.not_rightOnly_basic_of_isRightRule (lra : LocalRuleApp) (h : lra.isRightRule = true) : ¬lra.X.rightOnly.basic

A right local rule cannot be applied when the right component of the sequent is basic: the rule only looks at the right component and at a loaded formula on the right, so it would also be applicable to the sequent with an empty left component.

def modRChildRightOnly (A : ℕ) (ξ : AnyFormula) (R : Finset Formula) : Sequent

The right component of the child obtained by applying the modal rule (M) to a sequent whose loaded formula ~⌊·A⌋ξ is on the right. Note that it only depends on A, on ξ and on the right component R of the sequent, and hence only on Λ₂ of the node.

Equations

• modRChildRightOnly A (AnyFormula.normal φ) R = (∅, {~φ} ∪ Finset.projection A R, none)
• modRChildRightOnly A (AnyFormula.loaded χ) R = (∅, Finset.projection A R, some (Sum.inr (~'χ)))

theorem FinePathIn.basicRightStep {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesRightRule = true) (hb : f.label.rightOnly.basic) : f.atBigRoot = true ∧ f.label.2.2 = none ∨ (∃ (g : FinePathIn tab'), f.children = {g} ∧ g.atBigRoot = true ∧ g.label.2.2 = none) ∨ ∃ (A : ℕ) (ξ : AnyFormula), f.label.2.2 = some (Sum.inr (~'⌊·A⌋ξ)) ∧ ∃ (g : FinePathIn tab'), f.children = {g} ∧ g.atBigRoot = true ∧ g.label.left = Finset.projection A f.label.left ∧ g.label.rightOnly = modRChildRightOnly A ξ f.label.2.1

At a fine node with a basic right component where a right rule is applied, that rule is one of the three PdlRules acting on the right — and in particular the node is a node in the coarse sense. The three cases are (L+), where the node is free, (L-), whose unique child is free, and the modal rule (M), whose unique child has the projected left component and a right component determined by Λ₂ of the node.

theorem FinePathIn.label_eq_nodeAt_base {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.atBigRoot = true) : f.label = nodeAt f.base

A fine node that is a node in the coarse sense has the label of that coarse node.

Left rules do not change the right component

Dually, a left local rule leaves the right component of the sequent unchanged, provided the loaded formula is on the right (otherwise the (¬) rule for the loaded formula on the left would change the Olf). The left PdlRules (L+), (L-) and (M) are all only applicable when the loaded formula is not on the right.

theorem LocalRuleApp.rightOnly_eq_of_isLeftRule (lra : LocalRuleApp) (h : lra.isLeftRule = true) (hR : lra.O.isRight) (Y : Sequent) : Y ∈ lra.C → Y.rightOnly = lra.X.rightOnly

theorem FinePathIn.leftRuleStep {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesLeftRule = true) : (∃ (lra : LocalRuleApp), f.lra? = some lra ∧ lra.isLeftRule = true) ∨ f.atBigRoot = true ∧ ¬f.label.2.2.isRight

Where a left rule is applied, it is a local rule, unless the loaded formula is not on the right (which for a node of a LoadedCluster cannot happen).

theorem FinePathIn.children_rightOnly_eq_of_usesLeftRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesLeftRule = true) (hR : f.label.2.2.isRight) (g : FinePathIn tab') : g ∈ f.children → g.label.rightOnly = f.label.rightOnly

Part of Lemma 9.7 (c): at a node with the loaded formula on the right where a left rule is applied, all children have the same right component as the node itself.

theorem LocalRuleApp.left_sat_of_isLeftRule {lra : LocalRuleApp} (hl : lra.isLeftRule = true) (hR : lra.O.isRight) {W : Type} {M : KripkeModel W} {w : W} (hw : ∀ φ ∈ lra.X.left, evaluate M w φ) : ∃ Y ∈ lra.C, ∀ φ ∈ Y.left, evaluate M w φ

Local invertibility of a left rule, for the left component only: if the left component of the premise holds at a world, then so does the left component of one of the conclusions.

Note that localRuleTruth does not give this, since it also speaks about the right component, which need not hold at the world in question. That the loaded formula is on the right is needed to exclude the rule for a loaded formula on the left.

theorem FinePathIn.leftEntails_of_children_of_usesLeftRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesLeftRule = true) (hR : f.label.2.2.isRight) {φ : Formula} (hch : ∀ g ∈ f.children, g.leftEntails φ) : f.leftEntails φ

Local invertibility at a fine node where a left rule is applied, for the left component only: if a formula follows from the left component of every child, then it follows from the left component of the node itself.

Loading on the right is inherited upwards, and rules with children are left or right

Two ingredients for the descent of Lemma 9.7 (d) below. First, a fine node that has a coarse child loaded on the right is itself loaded on the right — this is what lets us apply FinePathIn.children_rightOnly_eq_of_usesLeftRule at the fine nodes of a cluster. Second, a fine node with children applies a left or a right rule: the only local rules that are neither are the closing rules, and those have no children.

theorem LocalRuleApp.isRight_of_mem_C (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → Y.2.2.isRight → lra.X.2.2.isRight

If a child of a local rule application is loaded on the right, then so is its premise. The local rules for a loaded formula on the left never produce a loading on the right, and the one-sided rules do not change the loaded formula at all.

theorem LocalTableau.isRight_of_mem_endNodesOf {Z : Sequent} (lt : LocalTableau Z) (Y : Sequent) : Y ∈ endNodesOf lt → Y.2.2.isRight → Z.2.2.isRight

If some end node of a local tableau is loaded on the right, then so is its root.

theorem LocalPathIn.mem_endNodesOf_ltAt {Z : Sequent} {lt : LocalTableau Z} (lp : LocalPathIn lt) (Yh : ↥(endNodesOf lt)) : Yh ∈ lp.endNodesBelow → ↑Yh ∈ endNodesOf lp.ltAt

The end nodes below a local path are end nodes of the local tableau at that path.

theorem FinePathIn.isRight_of_mem_coarseChildrenBelow {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : ¬f.atBigRoot = true → ∀ q ∈ f.coarseChildrenBelow, (nodeAt q).2.2.isRight → f.label.2.2.isRight

A fine node that is not a coarse node and has a coarse child loaded on the right is itself loaded on the right. (For coarse nodes this is false: the (L+) rule loads a free node.)

theorem LocalRuleApp.isLeftRule_or_isRightRule_of_C_ne_empty (lra : LocalRuleApp) (h : lra.C ≠ ∅) : lra.isLeftRule = true ∨ lra.isRightRule = true

A local rule application with at least one child is a left or a right rule: only the closing rules (¬) are neither, and they have no results.

theorem FinePathIn.usesLeftRule_or_usesRightRule_of_children_ne_empty {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.children ≠ ∅) : f.usesLeftRule = true ∨ f.usesRightRule = true

A fine node that has children applies a left or a right rule.

Loaded-path repeats and the Dershowitz-Manna measure

The three lemmas here are what replaces the paper's Fact lprAreCritical in the proof of Lemma 9.7 (d) below: instead of showing that the modal rule is applied between a companion and its repeat we show that going down along left rules strictly decreases the Dershowitz-Manna measure of the label, while a companion carries exactly the same label as its repeat.

theorem PathIn.not_isLrep_of_edge {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ⋖_ t) : ¬s.isLrep

A node where a rule is applied is not a loaded-path repeat. This would better belong next to edge in Pdl/TableauPath.lean.

theorem FinePathIn.atBigRoot_of_base_isLrep {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.base.isLrep) : f.atBigRoot = true

A fine node whose base is a loaded-path repeat is that coarse node itself, because a loaded-path repeat is a leaf and hence has no local tableau with internal nodes. This would better belong next to atBigRoot in Pdl/Interpolation/FinePath.lean.

theorem FinePathIn.children_lt_Sequent_of_usesLeftRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesLeftRule = true) (hR : f.label.2.2.isRight) (g : FinePathIn tab') : g ∈ f.children → lt_Sequent g.label f.label

Where a left rule is applied at a node with the loaded formula on the right, the labels of all children are strictly smaller in the Dershowitz-Manna ordering: by FinePathIn.leftRuleStep the rule applied there is a local rule, and local rules decrease the measure.