MatchingLogic.Composite

theorem MatchingLogic.cover_denote_closed {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (C : Set M.carrier) (hC : M.BackwardClosed C) (hne : C.Nonempty) (star : M.carrier) (hstar : star ∉ C) {ψ : Pattern S Var} (hψ : Closed ψ) (ν : Var → ↑C × Bool) (ρ : Var → M.carrier) (p : ↑C × Bool) : p ∈ (cover M C hne).denote ν ψ ↔ ↑p.1 ∈ M.denote ρ ψ

Corollary 12. For closed ψ, ⟦ψ⟧_N = (⟦ψ⟧_M ∩ C) × {0,1}. The ∩ C and the × {0,1} are both absorbed by the carrier ↥C × Bool: the statement says a point of N lies in ⟦ψ⟧_N exactly when its underlying point of C lies in ⟦ψ⟧_M, whichever copy it is in.

theorem MatchingLogic.cover_sat_iff {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (C : Set M.carrier) (hC : M.BackwardClosed C) (hne : C.Nonempty) (star : M.carrier) (hstar : star ∉ C) {ψ : Pattern S Var} (hψ : Closed ψ) (ρ : Var → M.carrier) : (cover M C hne).Sat ψ ↔ C ⊆ M.denote ρ ψ

Corollary 12, second half: N ⊨ ψ iff C ⊆ ⟦ψ⟧_M.

Note that star and hstar appear nowhere in the statement, only in the proof (Lemma 11 consumes them). They are not vestigial: requiring a point outside C is how this theorem carries Definition 10's standing assumption C ≠ M. A caller must exhibit one, so Corollary 12 does NOT apply when C = M -- which is exactly why Theorem 13 handles that case separately.

theorem MatchingLogic.semantic_localization_of_closed_Γ {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {φ : Pattern S Var} (hΓ : ∀ γ ∈ Γ, Closed γ) : GlobalCons Γ φ ↔ LocalCons (localize Γ) φ

Theorem 13 (semantic localization). Γ ⊨ φ ↔ Δ_Γ ⊨loc φ.

(⇐) is Lemma 7. (⇒) is contrapositive: a local countermodel gives a point w with w ∈ ⟦Δ_Γ⟧ and w ∉ ⟦φ⟧; take C := ⇝*[w], which is backward closed, contains w, and satisfies C ⊆ ⟦Γ⟧ by Lemma 8. If C = M we are done; otherwise the double cover N of Definition 10 satisfies Γ and refutes φ, by Corollary 12.

theorem MatchingLogic.semantic_localization {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {φ : Pattern S Var} (hΓ : ∀ γ ∈ Γ, Closed γ) (_hφ : Closed φ) : GlobalCons Γ φ ↔ LocalCons (localize Γ) φ

Theorem 13 (paper-facing statement). The paper assumes the conclusion closed globally; the mechanized proof above shows that assumption is unused.