MatchingLogic.EntryIII.Countertheory

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

Finite pointed-model existence: every locally consistent theory presented by a list has a model, valuation, and point matching all its members.

Equations

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

theorem MatchingLogic.locProvable_empty_iff {S : Signature} {Var : Type} [DecidableEq Var] {phi : Pattern S Var} : LocProvable ∅ phi ↔ Provable ∅ phi

Source Proposition 3.5(3), in the repository's finite-list presentation: local and ordinary theoremhood coincide for the empty theory.

theorem MatchingLogic.countertheory_locConsistent_of_not_provable {S : Signature} {Var : Type} [DecidableEq Var] {l : List (Pattern S Var)} {phi : Pattern S Var} (hnot : ¬Provable ∅ ((conj l).imp phi)) : LocConsistent {delta : Pattern S Var | delta ∈ [conj l, phi.nt]}

If conj l → phi is not a theorem, then the finite countertheory consisting of conj l and ¬phi is locally consistent.

theorem MatchingLogic.finiteLocalCompleteness_of_finiteLocalModelExistence {S : Signature} {Var : Type} [DecidableEq Var] (hmodel : FiniteLocalModelExistence S Var) : FiniteLocalCompleteness S Var

Finite pointed-model existence implies finite local completeness.