MatchingLogic.EntryIII.Conclusion

theorem MatchingLogic.finiteLocalModelExistence {S : Signature} : FiniteLocalModelExistence S ℕ

Every locally consistent finite list over an arbitrary ambient signature has a pointed model. Only its finite symbol restriction enters the canonical construction.

theorem MatchingLogic.finiteLocalCompleteness {S : Signature} : FiniteLocalCompleteness S ℕ

Unconditional finite-list local completeness over the source variable type Nat.

theorem MatchingLogic.strongLocalCompleteness_nat {S : Signature} : StrongLocalCompleteness S ℕ

Unconditional one-sorted strong local completeness over Nat.

theorem MatchingLogic.strongLocalCompleteness {S : Signature} {Var : Type} [DecidableEq Var] [Denumerable Var] : StrongLocalCompleteness S Var

Entry point (iii), at the source-faithful scope of one-sorted finitary signatures and a countably infinite element-variable type.

theorem MatchingLogic.global_completeness_entryIII {S : Signature} {Var : Type} [DecidableEq Var] [Denumerable Var] {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (hGamma : ∀ gamma ∈ Gamma, Closed gamma) (hphi : Closed phi) : GlobalCons Gamma phi ↔ Provable Gamma phi

The one-sorted case of Corollary 15 with both soundness and strong local completeness supplied by the development. Only the paper's closedness premises remain.