MatchingLogic.Sorted

structure MatchingLogic.Sorted.MSignature : Type 1

A many-sorted finitary signature.

• Srt : Type

  The type of sorts.

• Sym : Type

  The type of operation symbols.

• arity : self.Sym → ℕ

  The number of arguments of each operation symbol.

• argSort (σ : self.Sym) : Fin (self.arity σ) → self.Srt

  The sort of each argument position.

• resSort : self.Sym → self.Srt

  The result sort of each operation symbol.

inductive MatchingLogic.Sorted.MPattern (S : MSignature) (Var : Type) : S.Srt → Type

Patterns, indexed by their sort. ex x s' φ binds x AT SORT s' inside a pattern φ of sort s; the bound sort need not be the sort of the body, and in Proposition 30 it is not.

• var {S : MSignature} {Var : Type} : Var → (s : S.Srt) → MPattern S Var s
• app {S : MSignature} {Var : Type} (σ : S.Sym) : ((i : Fin (S.arity σ)) → MPattern S Var (S.argSort σ i)) → MPattern S Var (S.resSort σ)
• imp {S : MSignature} {Var : Type} {s : S.Srt} : MPattern S Var s → MPattern S Var s → MPattern S Var s
• bot {S : MSignature} {Var : Type} {s : S.Srt} : MPattern S Var s
• ex {S : MSignature} {Var : Type} {s : S.Srt} : Var → (s' : S.Srt) → MPattern S Var s → MPattern S Var s

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.nt {S : MSignature} {Var : Type} {s : S.Srt} (φ : MPattern S Var s) : MPattern S Var s

Sorted negation.

Equations

• φ.nt = φ.imp MatchingLogic.Sorted.MPattern.bot

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.tp {S : MSignature} {Var : Type} {s : S.Srt} : MPattern S Var s

Sorted truth.

Equations

• MatchingLogic.Sorted.MPattern.tp = MatchingLogic.Sorted.MPattern.bot.imp MatchingLogic.Sorted.MPattern.bot

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.and {S : MSignature} {Var : Type} {s : S.Srt} (φ ψ : MPattern S Var s) : MPattern S Var s

Sorted conjunction.

Equations

• φ.and ψ = (φ.imp ψ.nt).nt

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.orP {S : MSignature} {Var : Type} {s : S.Srt} (φ ψ : MPattern S Var s) : MPattern S Var s

Sorted disjunction.

Equations

• φ.orP ψ = φ.nt.imp ψ

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.iff {S : MSignature} {Var : Type} {s : S.Srt} (φ ψ : MPattern S Var s) : MPattern S Var s

Sorted biconditional.

Equations

• φ.iff ψ = (φ.imp ψ).and (ψ.imp φ)

@[reducible, inline]

abbrev MatchingLogic.Sorted.MPattern.al {S : MSignature} {Var : Type} {s : S.Srt} (x : Var) (s' : S.Srt) (φ : MPattern S Var s) : MPattern S Var s

Sorted universal quantification.

Equations

• MatchingLogic.Sorted.MPattern.al x s' φ = (MatchingLogic.Sorted.MPattern.ex x s' φ.nt).nt

structure MatchingLogic.Sorted.MModel (S : MSignature) : Type 1

A many-sorted model: a nonempty carrier per sort, and each symbol interpreted from its argument sorts to subsets of its result sort.

• carrier : S.Srt → Type

  The carrier type at each sort.

• nonempty (s : S.Srt) : Nonempty (self.carrier s)
• interp (σ : S.Sym) : ((i : Fin (S.arity σ)) → self.carrier (S.argSort σ i)) → Set (self.carrier (S.resSort σ))

  The set-valued interpretation of each operation symbol.

@[reducible, inline]

abbrev MatchingLogic.Sorted.MVal {S : MSignature} (M : MModel S) (Var : Type) : Type

A sorted valuation.

Equations

• MatchingLogic.Sorted.MVal M Var = ((s : S.Srt) → Var → M.carrier s)

noncomputable def MatchingLogic.Sorted.mupdate {S : MSignature} {Var : Type} (M : MModel S) (ρ : MVal M Var) (s' : S.Srt) (x : Var) (a : M.carrier s') : MVal M Var

Updating a sorted valuation at one variable of one sort. This is the only place the sort indexing costs anything: the new value has sort s', so it can only be installed at sort s', and the equality has to be transported.

Equations

• MatchingLogic.Sorted.mupdate M ρ s' x a t y = if y = x then if ht : t = s' then ⋯ ▸ a else ρ t y else ρ t y

def MatchingLogic.Sorted.MModel.app {S : MSignature} (M : MModel S) (σ : S.Sym) (A : (i : Fin (S.arity σ)) → Set (M.carrier (S.argSort σ i))) : Set (M.carrier (S.resSort σ))

The pointwise extension of a symbol, at its sorts.

Equations

• M.app σ A = {u : M.carrier (S.resSort σ) | ∃ (a : (i : Fin (S.arity σ)) → M.carrier (S.argSort σ i)), (∀ (i : Fin (S.arity σ)), a i ∈ A i) ∧ u ∈ M.interp σ a}

noncomputable def MatchingLogic.Sorted.mdenote {S : MSignature} {Var : Type} (M : MModel S) (ρ : MVal M Var) {s : S.Srt} : MPattern S Var s → Set (M.carrier s)

The denotation, sort by sort.

Equations

• MatchingLogic.Sorted.mdenote M ρ (MatchingLogic.Sorted.MPattern.var x_2 x✝) = {ρ x✝ x_2}
• MatchingLogic.Sorted.mdenote M ρ MatchingLogic.Sorted.MPattern.bot = ∅
• MatchingLogic.Sorted.mdenote M ρ (MatchingLogic.Sorted.MPattern.app σ f) = M.app σ fun (i : Fin (S.arity σ)) => MatchingLogic.Sorted.mdenote M ρ (f i)
• MatchingLogic.Sorted.mdenote M ρ (φ.imp ψ) = (MatchingLogic.Sorted.mdenote M ρ φ)ᶜ ∪ MatchingLogic.Sorted.mdenote M ρ ψ
• MatchingLogic.Sorted.mdenote M ρ (MatchingLogic.Sorted.MPattern.ex x_3 s' φ) = ⋃ (a : M.carrier s'), MatchingLogic.Sorted.mdenote M (MatchingLogic.Sorted.mupdate M ρ s' x_3 a) φ

theorem MatchingLogic.Sorted.mdenote_al {S : MSignature} {Var : Type} (M : MModel S) (ρ : MVal M Var) {s : S.Srt} (x : Var) (s' : S.Srt) (φ : MPattern S Var s) : mdenote M ρ (MPattern.al x s' φ) = ⋂ (a : M.carrier s'), mdenote M (mupdate M ρ s' x a) φ

The denotation clause for sorted universal quantification.

theorem MatchingLogic.Sorted.MModel.app_eq_empty {S : MSignature} (M : MModel S) (σ : S.Sym) (A : (i : Fin (S.arity σ)) → Set (M.carrier (S.argSort σ i))) (i : Fin (S.arity σ)) (h : A i = ∅) : M.app σ A = ∅

A many-sorted symbol application is empty if one argument is empty.

def MatchingLogic.Sorted.MModel.Sat {S : MSignature} {Var : Type} (M : MModel S) {s : S.Srt} (φ : MPattern S Var s) : Prop

M ⊨ φ: φ is total at its own sort under every valuation.

Equations

• M.Sat φ = ∀ (ρ : MatchingLogic.Sorted.MVal M Var), MatchingLogic.Sorted.mdenote M ρ φ = Set.univ

def MatchingLogic.Sorted.MModel.SatSetHet {S : MSignature} {Var : Type} (M : MModel S) (Γ : Set ((s : S.Srt) × MPattern S Var s)) : Prop

M ⊨ Γ for a HETEROGENEOUS theory: a set of sorted patterns, each total at its own sort. This is the paper's notion — nothing there requires the members of a theory to share a sort.

Equations

• M.SatSetHet Γ = ∀ p ∈ Γ, M.Sat p.snd

def MatchingLogic.Sorted.MModel.SatSet {S : MSignature} {Var : Type} (M : MModel S) {s : S.Srt} (Γ : Set (MPattern S Var s)) : Prop

M ⊨ Γ for a theory whose members all have one sort. A convenience: it is what Proposition 30 needs, since its Γ is a singleton of sort a. It is a special case of SatSetHet, not a different notion — satSetHet_homogeneous below records that.

Equations

• M.SatSet Γ = ∀ γ ∈ Γ, M.Sat γ

theorem MatchingLogic.Sorted.satSetHet_homogeneous {S : MSignature} {Var : Type} (M : MModel S) {s : S.Srt} (Γ : Set (MPattern S Var s)) : M.SatSet Γ ↔ M.SatSetHet {p : (s : S.Srt) × MPattern S Var s | ∃ γ ∈ Γ, p = ⟨s, γ⟩}

The homogeneous notion is the heterogeneous one restricted to a single sort. Without this the restriction in SatSet would be silent, and an audit flagged exactly that.

def MatchingLogic.Sorted.MGlobalCons {S : MSignature} {Var : Type} {sΓ sφ : S.Srt} (Γ : Set (MPattern S Var sΓ)) (φ : MPattern S Var sφ) : Prop

Γ ⊨ φ, where Γ and φ may live at DIFFERENT sorts -- which is exactly the situation Proposition 30 exploits.

Equations

• MatchingLogic.Sorted.MGlobalCons Γ φ = ∀ (M : MatchingLogic.Sorted.MModel S), M.SatSet Γ → M.Sat φ

def MatchingLogic.Sorted.MGlobalConsHet {S : MSignature} {Var : Type} (Γ : Set ((s : S.Srt) × MPattern S Var s)) {sφ : S.Srt} (φ : MPattern S Var sφ) : Prop

Global consequence from a heterogeneous theory.

Equations

• MatchingLogic.Sorted.MGlobalConsHet Γ φ = ∀ (M : MatchingLogic.Sorted.MModel S), M.SatSetHet Γ → M.Sat φ

The signature of Proposition 30

inductive MatchingLogic.Sorted.Srt3 : Type

Three sorts, b, a, c.

• b : Srt3
• a : Srt3
• c : Srt3

@[instance_reducible]

instance MatchingLogic.Sorted.instDecidableEqSrt3 : DecidableEq Srt3

Equations

• MatchingLogic.Sorted.instDecidableEqSrt3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive MatchingLogic.Sorted.Sym3 : Type

Two symbols, f : b → a and g : b → c.

• f : Sym3
• g : Sym3

@[instance_reducible]

instance MatchingLogic.Sorted.instDecidableEqSym3 : DecidableEq Sym3

Equations

• MatchingLogic.Sorted.instDecidableEqSym3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev MatchingLogic.Sorted.S3 : MSignature

The signature of Proposition 30. Note NO symbol has an argument of sort a; that is what the non-derivability half will turn on.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.Sorted.fAp {Var : Type} (ψ : MPattern S3 Var Srt3.b) : MPattern S3 Var Srt3.a

f(ψ) for ψ of sort b.

Equations

• MatchingLogic.Sorted.fAp ψ = MatchingLogic.Sorted.MPattern.app MatchingLogic.Sorted.Sym3.f fun (x : Fin (MatchingLogic.Sorted.S3.arity MatchingLogic.Sorted.Sym3.f)) => ψ

@[reducible, inline]

abbrev MatchingLogic.Sorted.gAp {Var : Type} (ψ : MPattern S3 Var Srt3.b) : MPattern S3 Var Srt3.c

g(ψ) for ψ of sort b.

Equations

• MatchingLogic.Sorted.gAp ψ = MatchingLogic.Sorted.MPattern.app MatchingLogic.Sorted.Sym3.g fun (x : Fin (MatchingLogic.Sorted.S3.arity MatchingLogic.Sorted.Sym3.g)) => ψ

@[reducible, inline]

abbrev MatchingLogic.Sorted.Γ3 {Var : Type} (x y : Var) : Set (MPattern S3 Var Srt3.a)

Γ = {∀x:b ∀y:b. f(x ∧ y)}, a theory of sort a.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.Sorted.φ3 {Var : Type} (x y : Var) : MPattern S3 Var Srt3.c

φ = ∀x:b ∀y:b. (g(x) ↔ g(y)), a pattern of sort c.

Equations

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

Proposition 30, semantic half

@[reducible, inline]

abbrev MatchingLogic.Sorted.singletonM3 : MModel S3

The singleton model used for satisfiability in Proposition 30.

Equations

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

theorem MatchingLogic.Sorted.Γ3_satisfiable {Var : Type} (x y : Var) : ∃ (M : MModel S3), M.SatSet (Γ3 x y)

Γ is satisfiable. Take every carrier a singleton and f, g total.

theorem MatchingLogic.Sorted.Γ3_entails_φ3 {Var : Type} (x y : Var) (hxy : x ≠ y) : MGlobalCons (Γ3 x y) (φ3 x y)

Γ ⊨ φ.

The paper: if M_b had distinct r, s, the valuation with ρ(x) = r, ρ(y) = s gives ρ(x ∧ y) = ∅, and symbols propagate ∅, so ρ(f(x ∧ y)) = ∅, which is not M_a because carriers are nonempty. Hence M_b is a singleton, every valuation sends x and y to the same element, and ρ(g(x) ↔ g(y)) = M_c for every ρ.