Facts about a proper cluster (Section 9 of the paper)

This file proves the facts about a proper loaded cluster C that the proofs of Lemma 10.1 (Pdl.ClusterItp) and Lemma 10.3 (Pdl.ClusterRho) use:

• LoadedCluster.exists_right_of_proper is Lemma 9.7 (d): if C_Δ is non-empty then so is C^R_Δ;
• LoadedCluster.vocL_fineCLplus and LoadedCluster.vocR_fineCLplus say that the vocabulary of both components only shrinks along the tableau, applied to the nodes of C⁺, all of which are below the root r of the cluster;
• LoadedCluster.loadedProgVoc_of_proper says that the leading atomic program a of the loaded formula of a basic Δ ∈ Λ₂[C] is in the joint vocabulary of the root;
• LoadedCluster.leftPropagation_of_proper is the inner induction in the proof of Lemma 10.3;
• LoadedCluster.rightRuleChildren_of_uniform is Lemma 9.7 (f) — the only place where uniformity of the tableau is needed;
• LoadedCluster.modalStep_of is Lemma 9.7 (e) in the semantic form used in the proof of Lemma 10.3.

All of them are proved from properness of the cluster, which is part of LoadedCluster, except for rightRuleChildren_of_uniform which also needs LoadedCluster.HasUniformSteps.

The facts about the rules of the tableau that they rely on are in Pdl.RuleFacts.

The two standing assumptions of the paper

The paper fixes a uniform closed tableau and a proper cluster in it, and both assumptions are used in Section 9. Neither of them holds for an arbitrary values of the Tableau type.

• the Tableau type does not force any coherence between the rules applied at different nodes, whereas uniformity (U1/U2) makes the rule applied at a node with a loaded, non-basic right component depend only on that component.

This is captured in the form needed here in LoadedCluster.HasUniformSteps.

Note that this file never unfolds LoadedCluster.HasUniformSteps: it is only used opaquely, as the hypothesis of LoadedCluster.stepOf_spec and as the conclusion of LoadedCluster.uniformOfUniTab. So the definition of HasUniformSteps may still be changed (for example from a List comparison to a Finset.image one) without affecting anything here, as long as those two statements are kept.

The vocabulary fields

theorem LoadedCluster.root_cReach_base_of_mem_fineCLplus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : f ∈ C.fineCLplus) : C.root ◃* f.base

Every fine node of C⁺ is ◃-reachable from the root of the cluster.

theorem LoadedCluster.vocL_fineCLplus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (f : FinePathIn tab) : f ∈ C.fineCLplus → f.label.left.fvoc ⊆ (nodeAt C.root).left.fvoc

The vocabulary of the left component only shrinks below the root of the cluster.

theorem LoadedCluster.vocR_fineCLplus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (f : FinePathIn tab) : f ∈ C.fineCLplus → f.label.right.fvoc ⊆ (nodeAt C.root).right.fvoc

The vocabulary of the right component only shrinks below the root of the cluster.

The remaining fields

theorem LoadedCluster.basicModalStepAt {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hb : Δ.basic) {t : FinePathIn tab} (ht : t ∈ C.nodesWithFineRight Δ) : ∃ (A : ℕ) (ξ : AnyFormula), Δ.2.2 = some (Sum.inr (~'⌊·A⌋ξ)) ∧ ∃ (g : FinePathIn tab), t.children = {g} ∧ g.atBigRoot = true ∧ g.label.left = Finset.projection A t.label.left ∧ g.label.rightOnly = modRChildRightOnly A ξ Δ.2.1

Lemma 9.7 (e): at a node t of C^R_Δ with Δ basic the rule applied is the modal rule (M) for the loaded formula ~⌊·A⌋ξ of Δ. Its unique child u satisfies Λ₁(u) = (Λ₁(t))_A, and its right component only depends on Δ.

Properness is needed to exclude the two other right PdlRules: (L+) is only applied at a free node, while (L-) makes its unique child free, and both contradict Lemma 9.4 (a) because by Lemma 9.4 (c) some child of t is again in the cluster.

theorem LoadedCluster.exists_child_rightOnly_of_mem_stepOf {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ Pi : Sequent} (hPi : Pi ∈ C.stepOf Δ) : ∃ f ∈ C.nodesWithFineRight Δ, ∃ g ∈ f.children, g.label.rightOnly = Pi

Every element of stepOf Δ is the right component of a child of some node of C^R_Δ, namely of the first one.

The descent for Lemma 9.7 (d)

The paper picks a node t ∈ C_Δ that is minimal in the tree order and then follows left-rule children downwards; by FinePathIn.children_rightOnly_eq_of_usesLeftRule this stays inside C_Δ, and closing rules are excluded because they have no children while Lemma 9.4 (c) (nonLpr_some_child_in_C, which needs properness) provides one.

The descent itself is FinePathIn.descent from Pdl.FinePathDescent: fine children are not structurally smaller, so the recursion is justified by the well-foundedness of the flipped fine child relation.

theorem LoadedCluster.memFine_label_isRight {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : C.memFine f) : f.label.2.2.isRight

Every fine node of the cluster is loaded on the right, i.e. Lemma 9.4 (a) at the fine level. For nodes that are coarse nodes this is all_right_loaded; for the intermediate nodes of a local tableau it follows because a coarse child of theirs is in the cluster and loading on the right is inherited upwards inside a local tableau.

theorem LoadedCluster.isRight_of_mem_lambdaTwo {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hΔ : Δ ∈ C.lambdaTwo) : Δ.2.2.isRight

Every label in Λ₂[C] is loaded on the right.

theorem LoadedCluster.exists_right_or_lrep {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hΔ : Δ ∈ C.lambdaTwo) : C.nodesWithFineRight Δ ≠ [] ∨ ∃ f ∈ C.nodesWithFine Δ, f.base.isLrep

The descent of Lemma 9.7 (d): if C_Δ is non-empty then either C^R_Δ is non-empty, or C_Δ contains a loaded-path repeat.

Starting from any node of C_Δ we follow children: as long as no right rule is applied and no repeat is reached, the node has a child in the cluster (Lemma 9.4 (c), which needs properness) with the same right component (Lemma 9.7 (c)), and the descent terminates by FinePathIn.descent — but a childless node of the cluster which is not a repeat would contradict Lemma 9.4 (c).

This is the paper's descent. It is no longer needed for Lemma 9.7 (d) below, which is now proved via isLrep_of_mem_nodesWithFine, but it is kept as the direct formalisation of the argument in the paper.

theorem LoadedCluster.exists_companion_mem_nodesWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} {f : FinePathIn tab} (hf : f ∈ C.nodesWithFine Δ) (hl : f.base.isLrep) : ∃ (c : PathIn tab), c.toFine ∈ C.nodesWithFine Δ ∧ ¬c.isLrep ∧ nodeAt c = f.label

If a node of C_Δ is a loaded-path repeat then its companion is again a node of C_Δ, it carries the same label, and it is not a loaded-path repeat itself.

That the companion is in the cluster is Lemma 9.4 (c) (lpr_comp_in_C); that it carries the same label is nodeAt_companionOf_setEq — note that with Finset sequents this is literal equality; and it is not a repeat because it is a proper ancestor of the repeat, while a repeat is a leaf.

theorem LoadedCluster.isLrep_of_mem_nodesWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hR : C.nodesWithFineRight Δ = []) (f : FinePathIn tab) : f ∈ C.nodesWithFine Δ → f.base.isLrep

Every node of C_Δ is a loaded-path repeat, provided C^R_Δ is empty.

This is the key step for Lemma 9.7 (d). The proof is by well-founded induction on the label along the Dershowitz-Manna ordering lt_Sequent: at a node of C_Δ that is not a repeat a left rule is applied — a right rule is excluded by the assumption — so by Lemma 9.4 (c) there is a child in the cluster, its right component is still Δ by Lemma 9.7 (c) and its label is strictly smaller. Applying the induction hypothesis to that child makes it a repeat, and then its companion is again in C_Δ with the same, hence still smaller, label, but is not a repeat — contradicting the induction hypothesis.

theorem LoadedCluster.exists_right_of_proper {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → C.nodesWithFineRight Δ ≠ []

Lemma 9.7 (d): if C_Δ is non-empty then so is C^R_Δ.

Where the paper uses its Fact lprAreCritical — on the path from a companion to its repeat the modal rule is applied at least once — we argue with the Dershowitz-Manna measure instead: if C^R_Δ were empty then by isLrep_of_mem_nodesWithFine all nodes of C_Δ would be loaded-path repeats, but the companion of such a repeat is again in C_Δ and is not a repeat. (Since Sequent now uses Finsets, a repeat carries exactly the same label as its companion, cf. nodeAt_companionOf_setEq.)

theorem LoadedCluster.loadedProgVoc_of_proper {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : (nodeAt C.root).left ≠ ∅ → ∀ Δ ∈ C.lambdaTwo, Δ.basic → Δ.loadedProg.voc ⊆ jvoc (nodeAt C.root)

The leading atomic program of a basic label of Λ₂[C] is in the joint vocabulary.

That it is in the vocabulary of Γ₂ is vocabulary preservation. That it is in the vocabulary of Γ₁ — which the paper does not mention, but which its Lemma 10.1 needs — uses Lemma 9.7 (e): the modal rule is applied at some t ∈ C^R_Δ and its child u is again in C, so Λ₁(u) = (Λ₁(t))_a is non-empty by Lemma 9.5 (b), which forces a box ⌈a⌉ψ in Λ₁(t).

theorem LoadedCluster.leftPropagation_of_proper {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → ∀ (φ : Formula), (∀ u ∈ C.nodesWithFineRight Δ, u.leftEntails φ) → (∀ u ∈ C.exitsWithFine Δ, u.leftEntails φ) → ∀ t ∈ C.plusNodesWithFine Δ, t.leftEntails φ

The inner induction in the proof of Lemma 10.3: if a formula follows from the left component of every node of C^R_Δ and of every exit node with right component Δ, then it follows from the left component of every node of C⁺_Δ. This packages Lemma 9.7 (a) — every node of C_Δ is in C^L_Δ or in C^R_Δ — with the local invertibility of the rules applied at the nodes of C^L_Δ.

The argument is a descent along the children of t: an exit is covered by the second hypothesis and a node of C^R_Δ by the first, while at a node of C^L_Δ all children stay in C⁺_Δ (by FinePathIn.children_rightOnly_eq_of_usesLeftRule and LoadedCluster.mem_fineCLplus_of_child) and the local invertibility of the left rule applied there transfers the entailment back up. That last step is FinePathIn.leftEntails_of_children_of_usesLeftRule; note that FinePathIn.locally_sound is not enough here, because it speaks about the whole label while leftEntails only assumes the left component, so we need the left-only invertibility LocalRuleApp.left_sat_of_isLeftRule.

The descent is not along the fine child relation but, as in isLrep_of_mem_nodesWithFine, by well-founded induction on the label along the Dershowitz-Manna ordering lt_Sequent: left rules strictly decrease the label, and this makes the remaining case, a loaded-path repeat in C_Δ, work out. At such a repeat no rule is applied, but by exists_companion_mem_nodesWithFine its companion is again a node of C_Δ with exactly the same label and is not a repeat, so the claim at the companion — which is the same claim, since leftEntails only depends on the label — is obtained from the very same case distinction, at the same label.

Properness of the cluster is used through LoadedCluster.exists_child_memFine_of_not_isLrep (Lemma 9.4 (c)), which is why no separate properness hypothesis is needed.

theorem LoadedCluster.rightRuleChildren_of_uniform {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hU : C.HasUniformSteps) (Δ : Sequent) : Δ ∈ C.lambdaTwo → ¬Δ.basic → ∀ t ∈ C.nodesWithFineRight Δ, ∀ Pi ∈ C.stepOf Δ, ∃ u ∈ C.plusNodesWithFine Pi, u.label.left = t.label.left

Lemma 9.7 (f): at a non-basic Δ the children of any t ∈ C^R_Δ are the Λ₁(t);Π for Π ∈ stepOf Δ. Here only the existence of a node of C⁺_Π with the same left component as t is recorded, which is what the proof of Lemma 10.3 uses.

theorem LoadedCluster.modalStep_of {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → Δ.basic → ∀ t ∈ C.nodesWithFineRight Δ, ∀ Pi ∈ C.stepOf Δ, ∃ u ∈ C.plusNodesWithFine Pi, ∀ (W : Type) (M : KripkeModel W) (w v : W), (∀ ψ ∈ t.label.left, evaluate M w ψ) → relate M Δ.loadedProg w v → ∀ ψ ∈ u.label.left, evaluate M v ψ

Lemma 9.7 (e), in the semantic form used in the proof of Lemma 10.3.

Note that no uniformity is needed here: by basicModalStepAt the right components of the children of a node of C^R_Δ with Δ basic are determined by Δ alone, so the list stepOf Δ, read off the first node of C^R_Δ, describes the children of every node of C^R_Δ.