MatchingLogic.Necessity

@[reducible, inline]

abbrev MatchingLogic.Necessity.S : Signature

One unary symbol.

Equations

• MatchingLogic.Necessity.S = { Sym := Unit, arity := fun (x : Unit) => 1 }

@[reducible, inline]

abbrev MatchingLogic.Necessity.M : Model S

Carrier {0,1,2}; the symbol sends 1 to 0 and everything else nowhere. Since 0 ∈ σ_M(1), the backward step of Definition 2 runs from the output to the argument: 0 ⇝ 1. So backward closure of {0} would force 1 ∈ {0}.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MatchingLogic.Necessity.C : Set (Fin 3)

The set {0}, which is not backward closed.

Equations

• MatchingLogic.Necessity.C = {0}

theorem MatchingLogic.Necessity.C_not_backwardClosed : ¬M.BackwardClosed C

The countermodel is stated for an arbitrary variable type, then instantiated both at Unit and at ℕ. The ℕ instance is the paper's setting, where the element variables are countably infinite, so this refutes the hypothesis-free statement in the paper's own domain and not merely in a degenerate one.

def MatchingLogic.Necessity.psi {Var : Type} (x : Var) : Pattern S Var

σ(x) for a chosen variable x.

Equations

• MatchingLogic.Necessity.psi x = MatchingLogic.Pattern.app () fun (x_1 : Fin (MatchingLogic.Necessity.S.arity ())) => MatchingLogic.Pattern.var x

def MatchingLogic.Necessity.rho {Var : Type} : Var → Fin 3

Both valuations send every variable outside C, so they satisfy AgreeOn.

Equations

• MatchingLogic.Necessity.rho x✝ = 1

def MatchingLogic.Necessity.rho' {Var : Type} : Var → Fin 3

The second constant valuation used by the agreement counterexample.

Equations

• MatchingLogic.Necessity.rho' x✝ = 2

theorem MatchingLogic.Necessity.agree {Var : Type} : AgreeOn C rho rho'

theorem MatchingLogic.Necessity.denote_rho {Var : Type} [DecidableEq Var] (x : Var) : M.denote rho (psi x) = {0}

theorem MatchingLogic.Necessity.denote_rho' {Var : Type} [DecidableEq Var] (x : Var) : M.denote rho' (psi x) = ∅

theorem MatchingLogic.Necessity.locality_needs_backwardClosed {Var : Type} [DecidableEq Var] (x : Var) : ¬∀ (ψ : Pattern S Var) (ρ ρ' : Var → Fin 3), AgreeOn C ρ ρ' → M.denote ρ ψ ∩ C = M.denote ρ' ψ ∩ C

The hypothesis of Lemma 9 cannot be dropped, for any variable type that has at least one variable. Without backward closure the conclusion fails, on a three-element model.

theorem MatchingLogic.Necessity.locality_needs_backwardClosed_nat : ¬∀ (ψ : Pattern S ℕ) (ρ ρ' : ℕ → Fin 3), AgreeOn C ρ ρ' → M.denote ρ ψ ∩ C = M.denote ρ' ψ ∩ C

The paper's setting: countably infinite element variables.