MatchingLogic.EntryIII.CanonicalCore

@[instance_reducible]

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

Local decidable equality used by the canonical-model construction.

Equations

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

def MatchingLogic.CanonicalCarrier (S : Signature) : Type

A point of the canonical model is a maximal locally consistent set with fresh Henkin witnesses. The ordinary witnessed interface is recovered below.

Equations

• MatchingLogic.CanonicalCarrier S = { Gamma : Set (MatchingLogic.Pattern S ℕ) // MatchingLogic.IsMCS Gamma ∧ MatchingLogic.FreshWitnessed Gamma }

@[instance_reducible]

instance MatchingLogic.CanonicalCarrier.coeSet {S : Signature} : Coe (CanonicalCarrier S) (Set (Pattern S ℕ))

Equations

• MatchingLogic.CanonicalCarrier.coeSet = { coe := fun (Gamma : MatchingLogic.CanonicalCarrier S) => ↑Gamma }

@[simp]

theorem MatchingLogic.CanonicalCarrier.coe_mk {S : Signature} (Gamma : Set (Pattern S ℕ)) (h : IsMCS Gamma ∧ FreshWitnessed Gamma) : ↑⟨Gamma, h⟩ = Gamma

theorem MatchingLogic.CanonicalCarrier.isMCS {S : Signature} (Gamma : CanonicalCarrier S) : IsMCS ↑Gamma

The underlying theory of a canonical point is an MCS.

theorem MatchingLogic.CanonicalCarrier.freshWitnessed {S : Signature} (Gamma : CanonicalCarrier S) : FreshWitnessed ↑Gamma

The underlying theory of a canonical point has fresh Henkin witnesses.

theorem MatchingLogic.CanonicalCarrier.witnessed {S : Signature} (Gamma : CanonicalCarrier S) : Witnessed ↑Gamma

Forgetting freshness recovers the interface used by the basic Truth Lemma.

theorem MatchingLogic.IsMCS.exists_var_mem_of_witnessed {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) (hW : Witnessed Gamma) : ∃ (y : ℕ), Pattern.var y ∈ Gamma

Every witnessed MCS contains an element-variable pattern. This is the source's Existence rule followed by the MCS's witness implication.

theorem MatchingLogic.CanonicalCarrier.exists_var_mem {S : Signature} (Gamma : CanonicalCarrier S) : ∃ (y : ℕ), Pattern.var y ∈ ↑Gamma

Carrier-specialized form of variable existence.

def MatchingLogic.canonicalInterp {S : Signature} (sigma : S.Sym) (components : Fin (S.arity sigma) → CanonicalCarrier S) : Set (CanonicalCarrier S)

Source Definition 72: Gamma is an output of sigma at component worlds components exactly when every pointwise choice of patterns from those worlds forms a sigma-application belonging to Gamma.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.canonicalModel {S : Signature} (root : CanonicalCarrier S) : Model S

The one-sorted canonical model. The designated root is used only to supply the required nonempty-carrier witness.

Equations

• MatchingLogic.canonicalModel root = { carrier := MatchingLogic.CanonicalCarrier S, nonempty := ⋯, interp := MatchingLogic.canonicalInterp }

@[simp]

theorem MatchingLogic.mem_canonicalInterp {S : Signature} {sigma : S.Sym} {components : Fin (S.arity sigma) → CanonicalCarrier S} {Gamma : CanonicalCarrier S} : Gamma ∈ canonicalInterp sigma components ↔ ∀ (args : Fin (S.arity sigma) → Pattern S ℕ), (∀ (i : Fin (S.arity sigma)), args i ∈ ↑(components i)) → Pattern.app sigma args ∈ ↑Gamma

@[simp]

theorem MatchingLogic.canonicalModel_interp {S : Signature} (root : CanonicalCarrier S) (sigma : S.Sym) (components : Fin (S.arity sigma) → CanonicalCarrier S) : (canonicalModel root).interp sigma components = canonicalInterp sigma components

theorem MatchingLogic.mem_canonicalModel_interp {S : Signature} (root : CanonicalCarrier S) {sigma : S.Sym} {components : Fin (S.arity sigma) → CanonicalCarrier S} {Gamma : CanonicalCarrier S} : Gamma ∈ (canonicalModel root).interp sigma components ↔ ∀ (args : Fin (S.arity sigma) → Pattern S ℕ), (∀ (i : Fin (S.arity sigma)), args i ∈ ↑(components i)) → Pattern.app sigma args ∈ ↑Gamma

Singleton argument consistency

theorem MatchingLogic.LocProvable.provable_empty {S : Signature} {p : Pattern S ℕ} (h : LocProvable ∅ p) : Provable ∅ p

With no local premises, local derivability collapses to ordinary empty-theory provability.

theorem MatchingLogic.IsMCS.singleton_argument_locConsistent {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) {sigma : S.Sym} {args : Fin (S.arity sigma) → Pattern S ℕ} (happ : Pattern.app sigma args ∈ Gamma) (i : Fin (S.arity sigma)) : LocConsistent {args i}

If an application belongs to an MCS, each singleton theory generated by one of its arguments is locally consistent. Otherwise framing an argument's derived bottom into the application and then propagating bottom contradicts the MCS consistency.