MatchingLogic.EntryIII.ModelExistence

@[instance_reducible]

noncomputable def MatchingLogic.instDecidableEqPatternNatModelExistence {S : Signature} : DecidableEq (Pattern S ℕ)

Local decidable equality used by the finite-model construction.

Equations

• MatchingLogic.instDecidableEqPatternNatModelExistence = Classical.decEq (MatchingLogic.Pattern S ℕ)

theorem MatchingLogic.finiteLocalModelExistence_of_canonicalExistence {S : Signature} [Countable (Pattern S ℕ)] (hExist : CanonicalExistenceProperty S) : FiniteLocalModelExistence S ℕ

Conditional finite pointed-model existence, obtained from a fresh-witnessed MCS root and the completed canonical Truth Lemma.

theorem MatchingLogic.finiteLocalCompleteness_of_canonicalExistence {S : Signature} [Countable (Pattern S ℕ)] (hExist : CanonicalExistenceProperty S) : FiniteLocalCompleteness S ℕ

Conditional finite-list local completeness.

theorem MatchingLogic.strongLocalCompleteness_nat_of_canonicalExistence {S : Signature} [Countable (Pattern S ℕ)] (hExist : CanonicalExistenceProperty S) : StrongLocalCompleteness S ℕ

Conditional strong local completeness over the source variable type Nat, using semantic compactness after the finite-list result.