MatchingLogic.Independence

Hypotheses that cannot be dropped

theorem MatchingLogic.semantic_localization_needs_closed_Γ : ¬∀ (S : Signature) (Var : Type) (x : DecidableEq Var) (Γ : Set (Pattern S Var)) (φ : Pattern S Var), Closed φ → (GlobalCons Γ φ ↔ LocalCons (localize Γ) φ)

Theorem 13 DOES need every member of Γ closed.

An open Γ constrains the model through the valuation quantifier hidden inside totality, and localization cannot see that.

Localization is not decoration

theorem MatchingLogic.localize_not_redundant : ¬∀ (S : Signature) (Var : Type) (x : DecidableEq Var) (Γ : Set (Pattern S Var)) (φ : Pattern S Var), (∀ γ ∈ Γ, Closed γ) → Closed φ → (GlobalCons Γ φ ↔ LocalCons Γ φ)

Replacing Δ_Γ by Γ makes Theorem 13 false, even for closed Γ and closed φ. So the localization in semantic_localization is load-bearing and the theorem forbids something.