MatchingLogic.EntryIII.FiniteReduction

def MatchingLogic.FiniteLocalCompleteness (S : Signature) (Var : Type) [DecidableEq Var] : Prop

Strong local completeness restricted to theories presented by finite lists.

Equations

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

theorem MatchingLogic.Model.denote_conj_eq_denoteSet_list {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (rho : Var → M.carrier) (l : List (Pattern S Var)) : M.denote rho (conj l) = M.denoteSet rho {delta : Pattern S Var | delta ∈ l}

A finite conjunction denotes the same set as the conjunctive denotation of the corresponding list-membership theory.

theorem MatchingLogic.localCons_list_iff {S : Signature} {Var : Type} [DecidableEq Var] (l : List (Pattern S Var)) (phi : Pattern S Var) : LocalCons {delta : Pattern S Var | delta ∈ l} phi ↔ ∀ (M : Model S) (rho : Var → M.carrier), M.denote rho (conj l) ⊆ M.denote rho phi

Pointwise form of local consequence from a finite list.

theorem MatchingLogic.strongLocalCompleteness_of_finiteLocalCompleteness {S : Signature} {Var : Type} [DecidableEq Var] (hfinite : FiniteLocalCompleteness S Var) : StrongLocalCompleteness S Var

Semantic compactness reduces full strong local completeness to its finite-list form.