MatchingLogic.EntryIII.Completion

@[instance_reducible]

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

Local decidable equality used by the model-completion construction.

Equations

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

def MatchingLogic.Missing {S : Signature} (root : CanonicalCarrier S) : Prop

Some element variable is absent from every world generated by root.

Equations

• MatchingLogic.Missing root = ∃ (x : ℕ), ∀ (world : MatchingLogic.GeneratedCarrier root), MatchingLogic.Pattern.var x ∉ ↑↑world

def MatchingLogic.CompletedCarrier {S : Signature} (root : CanonicalCarrier S) : Type

The source's conditional completion: all generated worlds are present, while none is a legal point exactly when Missing root holds.

Equations

• MatchingLogic.CompletedCarrier root = { o : Option (MatchingLogic.GeneratedCarrier root) // o = none → MatchingLogic.Missing root }

def MatchingLogic.CompletedCarrier.isStar {S : Signature} {root : CanonicalCarrier S} (point : CompletedCarrier root) : Prop

A completed point is the added star precisely when its option is none.

Equations

• point.isStar = (↑point = none)

def MatchingLogic.completedEmbed {S : Signature} (root : CanonicalCarrier S) (world : GeneratedCarrier root) : CompletedCarrier root

Embed a generated world into the completed carrier.

Equations

• MatchingLogic.completedEmbed root world = ⟨some world, ⋯⟩

def MatchingLogic.completedStar {S : Signature} {root : CanonicalCarrier S} (hmissing : Missing root) : CompletedCarrier root

Construct the star point from evidence that a variable is missing.

Equations

• MatchingLogic.completedStar hmissing = ⟨none, ⋯⟩

theorem MatchingLogic.completedEmbed_injective {S : Signature} (root : CanonicalCarrier S) : Function.Injective (completedEmbed root)

The generated-world embedding is injective.

theorem MatchingLogic.completedStar_ne_embed {S : Signature} {root : CanonicalCarrier S} (hmissing : Missing root) (world : GeneratedCarrier root) : completedStar hmissing ≠ completedEmbed root world

The conditional star is distinct from every embedded generated world.

theorem MatchingLogic.exists_completedStar_iff_missing {S : Signature} (root : CanonicalCarrier S) : (∃ (point : CompletedCarrier root), point.isStar) ↔ Missing root

The representation has a star point exactly in the source's missing-variable case.

theorem MatchingLogic.completedCarrier_cases {S : Signature} {root : CanonicalCarrier S} (point : CompletedCarrier root) : (∃ (world : GeneratedCarrier root), point = completedEmbed root world) ∨ ∃ (hmissing : Missing root), point = completedStar hmissing

Every completed point is either an embedded generated world or the unique conditional star.

Completed interpretation

def MatchingLogic.completedInterp {S : Signature} (root : CanonicalCarrier S) (sigma : S.Sym) (inputs : Fin (S.arity sigma) → CompletedCarrier root) : Set (CompletedCarrier root)

Source Definition 79's interpretation. The existential tuple makes the three cases exact: a star input admits no tuple; real outputs are the generated interpretation; and star is an additional output exactly when some real input is the generated root.

Equations

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

@[reducible, inline]

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

The completed one-sorted model.

Equations

• MatchingLogic.completedModel root = { carrier := MatchingLogic.CompletedCarrier root, nonempty := ⋯, interp := MatchingLogic.completedInterp root }

@[simp]

theorem MatchingLogic.mem_completedInterp {S : Signature} {root : CanonicalCarrier S} {sigma : S.Sym} {inputs : Fin (S.arity sigma) → CompletedCarrier root} {output : CompletedCarrier root} : output ∈ completedInterp root sigma inputs ↔ ∃ (components : Fin (S.arity sigma) → GeneratedCarrier root), (∀ (i : Fin (S.arity sigma)), inputs i = completedEmbed root (components i)) ∧ ((∃ (world : GeneratedCarrier root), output = completedEmbed root world ∧ world ∈ generatedInterp root sigma components) ∨ output.isStar ∧ ∃ (i : Fin (S.arity sigma)), components i = generatedRoot root)

@[simp]

theorem MatchingLogic.completedModel_interp {S : Signature} (root : CanonicalCarrier S) (sigma : S.Sym) (inputs : Fin (S.arity sigma) → CompletedCarrier root) : (completedModel root).interp sigma inputs = completedInterp root sigma inputs

theorem MatchingLogic.mem_completedModel_interp {S : Signature} {root : CanonicalCarrier S} {sigma : S.Sym} {inputs : Fin (S.arity sigma) → CompletedCarrier root} {output : CompletedCarrier root} : output ∈ (completedModel root).interp sigma inputs ↔ output ∈ completedInterp root sigma inputs

theorem MatchingLogic.completedInterp_eq_empty_of_input_star {S : Signature} {root : CanonicalCarrier S} {sigma : S.Sym} {inputs : Fin (S.arity sigma) → CompletedCarrier root} (i : Fin (S.arity sigma)) (hstar : (inputs i).isStar) : completedInterp root sigma inputs = ∅

Any star input forces the completed symbol interpretation to be empty.

theorem MatchingLogic.completedEmbed_mem_completedInterp_iff {S : Signature} (root : CanonicalCarrier S) {sigma : S.Sym} (components : Fin (S.arity sigma) → GeneratedCarrier root) (world : GeneratedCarrier root) : (completedEmbed root world ∈ completedInterp root sigma fun (i : Fin (S.arity sigma)) => completedEmbed root (components i)) ↔ world ∈ generatedInterp root sigma components

On all-real inputs, real output membership is exactly membership in the generated interpretation.

theorem MatchingLogic.completedStar_mem_completedInterp_iff {S : Signature} {root : CanonicalCarrier S} (hmissing : Missing root) {sigma : S.Sym} (components : Fin (S.arity sigma) → GeneratedCarrier root) : (completedStar hmissing ∈ completedInterp root sigma fun (i : Fin (S.arity sigma)) => completedEmbed root (components i)) ↔ ∃ (i : Fin (S.arity sigma)), components i = generatedRoot root

On all-real inputs, star is output exactly when one component is the generated root.

Completed valuation

noncomputable def MatchingLogic.completedValuation {S : Signature} (root : CanonicalCarrier S) (x : ℕ) : CompletedCarrier root

Select the unique generated world containing var x, when one exists; otherwise select the conditional star justified by x itself.

Equations

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

theorem MatchingLogic.completedValuation_isStar_iff {S : Signature} (root : CanonicalCarrier S) (x : ℕ) : (completedValuation root x).isStar ↔ ∀ (world : GeneratedCarrier root), Pattern.var x ∉ ↑↑world

The completed valuation is star exactly for variables missing from all generated worlds.

theorem MatchingLogic.completedValuation_eq_embed_iff {S : Signature} (root : CanonicalCarrier S) (x : ℕ) (world : GeneratedCarrier root) : completedValuation root x = completedEmbed root world ↔ Pattern.var x ∈ ↑↑world

The selection is well-defined: it names an embedded world exactly when that world contains the variable, with uniqueness supplied by Lemma 78.

theorem MatchingLogic.completedValuation_surjective {S : Signature} (root : CanonicalCarrier S) : Function.Surjective (completedValuation root)

Every point of the completed carrier is named by some element variable.