MatchingLogic.SetVariables

inductive MatchingLogic.SetVariables.SPattern (S : Signature) (Var SVar : Type) : Type

Patterns extended with free set variables. There is no μ and no binder for set variables: the point of Remark 17 concerns FREE set variables only.

• var {S : Signature} {Var SVar : Type} : Var → SPattern S Var SVar
• svar {S : Signature} {Var SVar : Type} : SVar → SPattern S Var SVar
• app {S : Signature} {Var SVar : Type} (σ : S.Sym) : (Fin (S.arity σ) → SPattern S Var SVar) → SPattern S Var SVar
• imp {S : Signature} {Var SVar : Type} : SPattern S Var SVar → SPattern S Var SVar → SPattern S Var SVar
• bot {S : Signature} {Var SVar : Type} : SPattern S Var SVar
• ex {S : Signature} {Var SVar : Type} : Var → SPattern S Var SVar → SPattern S Var SVar

structure MatchingLogic.SetVariables.SVal {S : Signature} (M : Model S) (Var SVar : Type) : Type

A valuation now sends element variables to points and set variables to arbitrary subsets.

• elem : Var → M.carrier

  The valuation of element variables.

• sets : SVar → Set M.carrier

  The valuation of set variables.

def MatchingLogic.SetVariables.sdenote {S : Signature} {Var SVar : Type} [DecidableEq Var] (M : Model S) : SVal M Var SVar → SPattern S Var SVar → Set M.carrier

The denotation, extending Section 2 with the clause ρ(X) = ρ(X).

Equations

• One or more equations did not get rendered due to their size.
• MatchingLogic.SetVariables.sdenote M x✝ (MatchingLogic.SetVariables.SPattern.var x_2) = {x✝.elem x_2}
• MatchingLogic.SetVariables.sdenote M x✝ (MatchingLogic.SetVariables.SPattern.svar X) = x✝.sets X
• MatchingLogic.SetVariables.sdenote M x✝ MatchingLogic.SetVariables.SPattern.bot = ∅
• MatchingLogic.SetVariables.sdenote M x✝ (MatchingLogic.SetVariables.SPattern.app σ f) = M.app σ fun (i : Fin (S.arity σ)) => MatchingLogic.SetVariables.sdenote M x✝ (f i)
• MatchingLogic.SetVariables.sdenote M x✝ (a.imp b) = (MatchingLogic.SetVariables.sdenote M x✝ a)ᶜ ∪ MatchingLogic.SetVariables.sdenote M x✝ b

def MatchingLogic.SetVariables.SSat {S : Signature} {Var SVar : Type} [DecidableEq Var] (M : Model S) (φ : SPattern S Var SVar) : Prop

M ⊨ φ, with the valuation quantifier ranging over set valuations too -- which is exactly what makes a free set variable behave unlike a constant.

Equations

• MatchingLogic.SetVariables.SSat M φ = ∀ (ρ : MatchingLogic.SetVariables.SVal M Var SVar), MatchingLogic.SetVariables.sdenote M ρ φ = Set.univ

def MatchingLogic.SetVariables.SGlobalCons {S : Signature} {Var SVar : Type} [DecidableEq Var] (Γ : Set (SPattern S Var SVar)) (φ : SPattern S Var SVar) : Prop

Γ ⊨ φ in the extended language.

Equations

• MatchingLogic.SetVariables.SGlobalCons Γ φ = ∀ (M : MatchingLogic.Model S), (∀ γ ∈ Γ, MatchingLogic.SetVariables.SSat M γ) → MatchingLogic.SetVariables.SSat M φ

The two halves of the counterexample

theorem MatchingLogic.SetVariables.not_ssat_svar {S : Signature} {Var SVar : Type} [DecidableEq Var] (M : Model S) (X : SVar) : ¬SSat M (SPattern.svar X)

No model satisfies a bare set variable, because the valuation sending it to ∅ makes it not total. This is the step a constant does not admit.

theorem MatchingLogic.SetVariables.sGlobalCons_svar_bot {S : Signature} {Var SVar : Type} [DecidableEq Var] (X : SVar) : SGlobalCons {SPattern.svar X} SPattern.bot

Hence {X} ⊨ ⊥ holds vacuously.

@[reducible, inline]

abbrev MatchingLogic.SetVariables.constSig : Signature

The signature with a single constant d.

Equations

• MatchingLogic.SetVariables.constSig = { Sym := Unit, arity := fun (x : Unit) => 0 }

@[reducible, inline]

abbrev MatchingLogic.SetVariables.dPat {Var : Type} : Pattern constSig Var

d itself, as a pattern of the base language.

Equations

• MatchingLogic.SetVariables.dPat = MatchingLogic.Pattern.app () fun (i : Fin (MatchingLogic.SetVariables.constSig.arity ())) => i.elim0

@[reducible, inline]

abbrev MatchingLogic.SetVariables.fullConstModel : Model constSig

A one-point model in which the constant d denotes the whole carrier.

Equations

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

theorem MatchingLogic.SetVariables.not_globalCons_const_bot {Var : Type} [DecidableEq Var] : ¬GlobalCons {dPat} Pattern.bot

But {d} ⊭ ⊥, as the model with d_M = M shows. So replacing the set variable by a constant changes the truth of the consequence.

theorem MatchingLogic.SetVariables.set_variable_is_not_a_constant {Var SVar : Type} [DecidableEq Var] (X : SVar) : SGlobalCons {SPattern.svar X} SPattern.bot ∧ ¬GlobalCons {dPat} Pattern.bot

Remark 17. Reading a free set variable as a constant does not preserve global consequence: the same Γ ⊨ φ is true on the left and false on the right. So Corollary 15 does not extend to patterns with free set variables.