The region formulas and the left half of the correctness of θ_r #
This file continues the development of Pdl.ClusterItp with
- Definition 10.2: the region formulas
ρ_x, and - Lemma 10.3:
Γ₁ ⊨ θ_r.
A proper prefix of x is one of the addresses searched by QuasiTab.companion?.
Two semantic lemmas #
stepToStar in the form used in the companion case of Lemma 10.3: if φ is preserved
along α and implies ψ, then φ implies [α*]ψ.
Definition 10.2: the region formulas #
Def 10.2: the formula ρ_x = ⋁ { ⋀ Λ₁(t) | t ∈ R_x } for a node x of the
quasi-tableau, where R_x is the region of x (Def 9.10). When there is no node at
address x we return ⊥, the empty disjunction.
Equations
Instances For
ρ_x holds iff some node of the region R_x has all its left formulas true.
The region, and hence ρ_x, only depends on the type and the label of the node.
Nodes of type 1 and of type 2 with the same label have the same region (Def 9.10).
Lemma 10.3: Γ₁ ⊨ θ_r #
The proof of Lemma 10.3 in the paper goes through the claim that ρ_x ⊨ σ(ι_x) for every
node x of the quasi-tableau, where σ sends the internal variable q_x to the region
formula ρ_x. We call this claim LoadedCluster.RhoSat.
The claim ρ_x ⊨ ι_x⟨σ⟩ of the proof of Lemma 10.3, where the substitution σ sends
each internal variable q_z to the region formula ρ_z.
Equations
- C.RhoSat θ x = ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (C.rho x) → evaluate M w (QFormula.subst C.rho (C.iitp θ x))
Instances For
The cases of the claim #
Each case of the leaf-to-root induction in the proof of Lemma 10.3 is a separate lemma.
Where the paper uses that the child of a node of type k has type k+1 and the same
label — which is part of the construction in Def 9.8 but not of the data type QuasiTab —
this is an explicit hypothesis.
Case k(x) = 1 and x a repeat: ι_x = q_{c(x)} and ρ_x = ρ_{c(x)}.
Case k(x) = 1 where x is neither a leaf nor a companion: ι_x = ι_y and
ρ_x = ρ_y, because the unique child y has type 2 and the same label.
Entailment from the left component of a node #
The claim of the proof of Lemma 10.3 is often used in the equivalent form
ρ_x ⊨ ι_x⟨σ⟩ iff Λ₁(t) ⊨ ι_x⟨σ⟩ for all t ∈ R_x, see rhoSat_iff.
A node of C⁺ whose right component is not in Λ₂[C] is an exit node.
Λ₁(t) ⊨ θ_Δ for all exit nodes t with right component Δ, i.e. Lemma 9.14 (a)
in the form of an entailment.
Case k(x) = 1 where x is a leaf that is not a repeat: ι_x = θ_{Δ_x} and every
node of the region is an exit node, so Lemma 9.14 (a) applies.
Case k(x) = 2: the unique child y has type 3 and the same label Δ, and
ι_x = [¬θ_Δ?]ι_y. Here R_x = C⁺_Δ but R_y = C^R_Δ, so we use the inner induction of
the paper, which is PaperFacts.leftPropagation.
Case k(x) = 3 with Δ_x basic: the unique child y has type 1 and its label is the
sequent obtained by applying the modal rule, and ι_x = [a]ι_y.
Case k(x) = 3 with Δ_x not basic: the children y_i have type 1 and are labelled
with the sequents Π_i of the right rule applied at Δ_x, and ι_x = ⋀ᵢ ι_{y_i}.
Case k(x) = 1 where x is a companion: the unique child y has type 2 and the same
label, so ρ_x = ρ_y, and ι_x = gfp x ι_y. Writing the normal form of ι_y as
⋀ᵢ[αᵢ]q_x ∧ ⋀ⱼ[βⱼ]q_{zⱼ} ∧ ψ the induction hypothesis says that ρ implies
[α]ρ ∧ ⋀ⱼ[βⱼ]σ(q_{zⱼ}) ∧ ψ where α = ⋃ᵢαᵢ, so stepToStar gives the claim.
The claim for all nodes of the quasi-tableau #
The leaf-to-root induction of the proof of Lemma 10.3 follows the recursion of
QuasiTab.build, i.e. of Definition 9.8.
The claim ρ_x ⊨ ι_x⟨σ⟩ for all nodes of the quasi-tableau, by leaf-to-root induction.
The hypothesis on the history is the invariant of Definition 9.8: every sequent in the
history of the construction is the label of a node of type 1 strictly above x, which is
what makes a leaf whose label is in the history a repeat.
The claim ρ_x ⊨ ι_x⟨σ⟩ at the root of the quasi-tableau.
Lemma 10.3 #
Lemma 10.3: Γ₁ ⊨ θ_r, i.e. the left component of the root of the cluster together
with the negation of the interpolant of Definition 9.20 is unsatisfiable.