MatchingLogic.Definedness

@[reducible, inline]

abbrev MatchingLogic.defSig (S : Signature) : Signature

The signature enriched with a unary definedness symbol, written none.

Equations

• MatchingLogic.defSig S = { Sym := Option S.Sym, arity := fun (s : Option S.Sym) => match s with | none => 1 | some σ => S.arity σ }

def MatchingLogic.emb {S : Signature} {Var : Type} : Pattern S Var → Pattern (defSig S) Var

Definedness-free patterns embed into the enriched language.

Equations

• MatchingLogic.emb (MatchingLogic.Pattern.var x_1) = MatchingLogic.Pattern.var x_1
• MatchingLogic.emb MatchingLogic.Pattern.bot = MatchingLogic.Pattern.bot
• MatchingLogic.emb (a.imp b) = (MatchingLogic.emb a).imp (MatchingLogic.emb b)
• MatchingLogic.emb (MatchingLogic.Pattern.ex x_1 a) = MatchingLogic.Pattern.ex x_1 (MatchingLogic.emb a)
• MatchingLogic.emb (MatchingLogic.Pattern.app σ f) = MatchingLogic.Pattern.app (some σ) fun (i : Fin ((MatchingLogic.defSig S).arity (some σ))) => MatchingLogic.emb (f i)

def MatchingLogic.defined {S : Signature} {Var : Type} (φ : Pattern (defSig S) Var) : Pattern (defSig S) Var

⌈φ⌉.

Equations

• MatchingLogic.defined φ = MatchingLogic.Pattern.app none fun (x : Fin ((MatchingLogic.defSig S).arity none)) => φ

def MatchingLogic.definednessAxiom {S : Signature} {Var : Type} (x : Var) : Pattern (defSig S) Var

The axiom ⌈x⌉ of the paper.

Equations

• MatchingLogic.definednessAxiom x = MatchingLogic.defined (MatchingLogic.Pattern.var x)

def MatchingLogic.expand {S : Signature} (M : Model S) : Model (defSig S)

The expansion of a definedness-free model: the same carrier, the same symbols, and definedness interpreted as constantly everything on singletons — which the pointwise extension turns into univ on nonempty arguments and ∅ on empty ones.

Equations

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

theorem MatchingLogic.denote_emb {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (φ : Pattern S Var) : (expand M).denote ρ (emb φ) = M.denote ρ φ

The embedding preserves denotation.

theorem MatchingLogic.expand_sat_definednessAxiom {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (x : Var) : (expand M).Sat (definednessAxiom x)

The expansion satisfies the definedness axiom, so it really is a model of Γ ∪ {⌈x⌉} whenever M is a model of Γ.

theorem MatchingLogic.denote_defined {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (φ : Pattern (defSig S) Var) : ((expand M).denote ρ (defined φ) = Set.univ ↔ ((expand M).denote ρ φ).Nonempty) ∧ ((expand M).denote ρ (defined φ) = ∅ ↔ (expand M).denote ρ φ = ∅)

⌈·⌉ has the semantics of Section 2 in the expansion: univ when the argument is inhabited, ∅ when it is empty. This is a control: if it failed, expand would not be interpreting definedness.

theorem MatchingLogic.definedness_conservative {S : Signature} {Var : Type} [DecidableEq Var] (hL : StrongLocalCompleteness S Var) {Γ : Set (Pattern S Var)} {φ : Pattern S Var} (hΓ : ∀ γ ∈ Γ, Closed γ) (hφ : Closed φ) (x : Var) (h : Provable (emb '' Γ ∪ {definednessAxiom x}) (emb φ)) : Provable Γ φ

Corollary 16 (conservativity of definedness).

Note (S) is supplied rather than assumed — soundness is a theorem here, and it holds at defSig S as at any signature. (L) remains a hypothesis, inherited from Corollary 15, and is needed at the BASE signature only.