MatchingLogic.EntryIII.Compactness

def MatchingLogic.EntryIII.relLanguage (S : Signature) : FirstOrder.Language

The relational first-order signature associated to a matching-logic signature. sigma of matching arity k becomes a relation of arity k + 1; coordinate zero is the output/current point.

Equations

• MatchingLogic.EntryIII.relLanguage S = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => { sigma : S.Sym // S.arity sigma + 1 = n } }

instance MatchingLogic.EntryIII.relLanguage_isRelational (S : Signature) : (relLanguage S).IsRelational

def MatchingLogic.EntryIII.relSym {S : Signature} (sigma : S.Sym) : (relLanguage S).Relations (S.arity sigma + 1)

The relation symbol associated to a matching symbol.

Equations

• MatchingLogic.EntryIII.relSym sigma = ⟨sigma, ⋯⟩

noncomputable def MatchingLogic.EntryIII.Pattern.toFOAux {S : Signature} {Var : Type} [DecidableEq Var] (p : Pattern S Var) {alpha : Type u} : (Var → alpha) → alpha → (relLanguage S).Formula alpha

Relational FOL translation at named free variables eta and current point cur. The recursive calls may enlarge the free-variable type with finitely many local witness variables; iExs binds exactly those variables.

Equations

• One or more equations did not get rendered due to their size.
• MatchingLogic.EntryIII.Pattern.toFOAux (MatchingLogic.Pattern.var x_4) x✝¹ x✝ = (FirstOrder.Language.var x✝).equal (FirstOrder.Language.var (x✝¹ x_4))
• MatchingLogic.EntryIII.Pattern.toFOAux MatchingLogic.Pattern.bot x✝¹ x✝ = ⊥
• MatchingLogic.EntryIII.Pattern.toFOAux (phi.imp psi) x✝¹ x✝ = (MatchingLogic.EntryIII.Pattern.toFOAux phi x✝¹ x✝).imp (MatchingLogic.EntryIII.Pattern.toFOAux psi x✝¹ x✝)

noncomputable def MatchingLogic.EntryIII.Pattern.toFOFormula {S : Signature} {Var : Type} [DecidableEq Var] (p : Pattern S Var) : (relLanguage S).Formula (Option Var)

Translation with free variable none for the current point and some x for the matching-logic valuation of x.

Equations

• MatchingLogic.EntryIII.Pattern.toFOFormula p = MatchingLogic.EntryIII.Pattern.toFOAux p some none

noncomputable def MatchingLogic.EntryIII.Pattern.toFOSentence {S : Signature} {Var : Type} [DecidableEq Var] (p : Pattern S Var) : ((relLanguage S).withConstants (Option Var)).Sentence

Sentence translation. Mathlib's constants extension names the current point and every matching-logic variable.

Equations

• MatchingLogic.EntryIII.Pattern.toFOSentence p = FirstOrder.Language.Formula.equivSentence (MatchingLogic.EntryIII.Pattern.toFOFormula p)

@[instance_reducible]

def MatchingLogic.EntryIII.Model.toFOStructure {S : Signature} (M : Model S) : (relLanguage S).Structure M.carrier

Interpret the relational FOL signature in a matching-logic model.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.EntryIII.Model.ofFOStructure {S : Signature} {Var : Type} (A : Type) [Nonempty A] [((relLanguage S).withConstants (Option Var)).Structure A] : Model S

Recover a matching-logic model from a structure in the constants-expanded relational language.

Equations

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

def MatchingLogic.EntryIII.Model.ofFOValuation {S : Signature} {Var : Type} (A : Type) [((relLanguage S).withConstants (Option Var)).Structure A] : Var → A

Valuation recovered from the named constants.

Equations

• MatchingLogic.EntryIII.Model.ofFOValuation A x = ↑((MatchingLogic.EntryIII.relLanguage S).con (some x))

def MatchingLogic.EntryIII.Model.ofFOCurrent {S : Signature} {Var : Type} (A : Type) [((relLanguage S).withConstants (Option Var)).Structure A] : A

Distinguished current point recovered from the named constant.

Equations

• MatchingLogic.EntryIII.Model.ofFOCurrent A = ↑((MatchingLogic.EntryIII.relLanguage S).con none)

theorem MatchingLogic.EntryIII.realize_toFOAux_of_rel {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) [(relLanguage S).Structure M.carrier] (hcompat : ∀ (sigma : S.Sym) (out : M.carrier) (args : Fin (S.arity sigma) → M.carrier), FirstOrder.Language.Structure.RelMap (relSym sigma) (Fin.cons out args) ↔ out ∈ M.interp sigma args) (p : Pattern S Var) {alpha : Type u} (eta : Var → alpha) (cur : alpha) (v : alpha → M.carrier) : (Pattern.toFOAux p eta cur).Realize v ↔ v cur ∈ M.denote (v ∘ eta) p

Correctness of the open-formula translation for any relational structure whose relation maps agree with a matching-logic model.

theorem MatchingLogic.EntryIII.realize_toFOAux {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (p : Pattern S Var) {alpha : Type u} (eta : Var → alpha) (cur : alpha) (v : alpha → M.carrier) : (Pattern.toFOAux p eta cur).Realize v ↔ v cur ∈ M.denote (v ∘ eta) p

Correctness specialized to the FOL structure built from a matching model.

def MatchingLogic.EntryIII.Model.toFOParameters {S : Signature} {Var : Type} (M : Model S) (rho : Var → M.carrier) (u : M.carrier) : Option Var → M.carrier

A valuation of the FOL parameters from a matching valuation and current point.

Equations

• MatchingLogic.EntryIII.Model.toFOParameters M rho u none = u
• MatchingLogic.EntryIII.Model.toFOParameters M rho u (some x_1) = rho x_1

theorem MatchingLogic.EntryIII.realize_toFOSentence {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (rho : Var → M.carrier) (u : M.carrier) (p : Pattern S Var) : M.carrier ⊨ Pattern.toFOSentence p ↔ u ∈ M.denote rho p

Correctness of sentence translation in the constants expansion built from a matching model, valuation, and current point.

theorem MatchingLogic.EntryIII.realize_toFOSentence_ofFOStructure {S : Signature} {Var : Type} [DecidableEq Var] (A : Type) [Nonempty A] [((relLanguage S).withConstants (Option Var)).Structure A] (p : Pattern S Var) : A ⊨ Pattern.toFOSentence p ↔ Model.ofFOCurrent A ∈ (Model.ofFOStructure A).denote (Model.ofFOValuation A) p

Correctness in an arbitrary structure of the constants-expanded language, after recovering its matching model, valuation, and current point.

noncomputable def MatchingLogic.EntryIII.counterTheory {S : Signature} {Var : Type} [DecidableEq Var] (Delta : Set (Pattern S Var)) (phi : Pattern S Var) : ((relLanguage S).withConstants (Option Var)).Theory

The first-order theory describing a counterexample to Delta ⊨loc phi.

Equations

• MatchingLogic.EntryIII.counterTheory Delta phi = MatchingLogic.EntryIII.Pattern.toFOSentence '' Delta ∪ {FirstOrder.Language.Formula.not (MatchingLogic.EntryIII.Pattern.toFOSentence phi)}

theorem MatchingLogic.EntryIII.not_counterTheory_isSatisfiable {S : Signature} {Var : Type} [DecidableEq Var] {Delta : Set (Pattern S Var)} {phi : Pattern S Var} (hlocal : LocalCons Delta phi) : ¬(counterTheory Delta phi).IsSatisfiable

A local semantic consequence has no FOL countermodel under the translation.

theorem MatchingLogic.EntryIII.counterTheory_isSatisfiable_of_counterexample {S : Signature} {Var : Type} [DecidableEq Var] {Delta : Set (Pattern S Var)} {phi : Pattern S Var} (M : Model S) (rho : Var → M.carrier) (u : M.carrier) (hDelta : u ∈ M.denoteSet rho Delta) (hphi : u ∉ M.denote rho phi) : (counterTheory Delta phi).IsSatisfiable

Conversely, a matching counterexample yields a model of the FOL counterexample theory.

theorem MatchingLogic.EntryIII.localCons_iff_not_counterTheory_isSatisfiable {S : Signature} {Var : Type} [DecidableEq Var] {Delta : Set (Pattern S Var)} {phi : Pattern S Var} : LocalCons Delta phi ↔ ¬(counterTheory Delta phi).IsSatisfiable

Exact semantic equivalence used by the compactness reduction.

theorem MatchingLogic.EntryIII.localCons_compact {S : Signature} {Var : Type} [DecidableEq Var] {Delta : Set (Pattern S Var)} {phi : Pattern S Var} (hlocal : LocalCons Delta phi) : ∃ (l : List (Pattern S Var)), (∀ delta ∈ l, delta ∈ Delta) ∧ LocalCons {delta : Pattern S Var | delta ∈ l} phi

Semantic local compactness for matching logic. No countability assumption is needed on the matching-symbol type or on the variable type.

theorem MatchingLogic.localCons_compact {S : Signature} {Var : Type} [DecidableEq Var] {Delta : Set (Pattern S Var)} {phi : Pattern S Var} (hlocal : LocalCons Delta phi) : ∃ (l : List (Pattern S Var)), (∀ delta ∈ l, delta ∈ Delta) ∧ LocalCons {delta : Pattern S Var | delta ∈ l} phi

Public form of semantic local compactness, used to reduce arbitrary signatures to the finite symbol support of finitely many premises and the conclusion.