MatchingLogic.Locality

def MatchingLogic.AgreeOn {S : Signature} {Var : Type} {M : Model S} (C : Set M.carrier) (ρ ρ' : Var → M.carrier) : Prop

The agreement condition of Lemma 9: on C the two valuations coincide, and off C they are both off C.

Equations

• MatchingLogic.AgreeOn C ρ ρ' = ∀ (x : Var), ρ x = ρ' x ∧ ρ x ∈ C ∨ ρ x ∉ C ∧ ρ' x ∉ C

theorem MatchingLogic.Model.app_inter_backwardClosed {S : Signature} {M : Model S} {C : Set M.carrier} (hC : M.BackwardClosed C) (σ : S.Sym) (A : Fin (S.arity σ) → Set M.carrier) : M.app σ A ∩ C = (M.app σ fun (i : Fin (S.arity σ)) => A i ∩ C) ∩ C

The concrete identity behind the app/symbol case of the paper's proof: σ_M(A₁,…,Aₙ) ∩ C = σ_M(A₁∩C,…,Aₙ∩C) ∩ C. Backward closure of C is used to pull each witnessing tuple entry into C once the produced point already lies in C.

theorem MatchingLogic.AgreeOn.update {S : Signature} {Var : Type} [DecidableEq Var] {M : Model S} {C : Set M.carrier} {ρ ρ' : Var → M.carrier} (h : AgreeOn C ρ ρ') (x : Var) (a : M.carrier) : AgreeOn C (Function.update ρ x a) (Function.update ρ' x a)

AgreeOn is preserved by matched updates: updating both valuations at the same variable to the same value keeps them agreeing, whether or not that value lies in C.

theorem MatchingLogic.locality {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) {C : Set M.carrier} (hC : M.BackwardClosed C) (ψ : Pattern S Var) (ρ ρ' : Var → M.carrier) (h : AgreeOn C ρ ρ') : M.denote ρ ψ ∩ C = M.denote ρ' ψ ∩ C

Lemma 9 (locality). A backward-closed C together with one bit per variable -- whether that variable's value lies in C -- determines truth on C.