MatchingLogic.EntryIII.Truth

@[instance_reducible]

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

Local decidable equality used by the truth lemma.

Equations

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

theorem MatchingLogic.completed_truth {S : Signature} (hExist : CanonicalExistenceProperty S) (root : CanonicalCarrier S) (world : GeneratedCarrier root) (p : Pattern S ℕ) : p ∈ ↑↑world ↔ completedEmbed root world ∈ (completedModel root).denote (completedValuation root) p

Source Lemma 81, conditional only on the separately isolated canonical Existence Lemma.