Formula-defined constants in interpreted structures

A relational interpretation can be expanded by target constants whose values are uniquely specified by source formulas on its domain. Validity requires existence and uniqueness inside the interpreted domain; it is a hypothesis on the source structure, not an implicit choice of default values. For finitely many constants, the pullback existentially quantifies their tuples, asserts their definitions and domain membership, and uses Mathlib's native constants-to-variables equivalence followed by the existing relational pullback. Free variables and selected constants occupy disjoint summands, so bound variables cannot capture either.

The canonical full-tuple instance and its numeric-preserving composition are supplied separately in Ordered.FullTuple and Ordered.FullTuple.Composition. This generic extension retains explicit validity hypotheses for arbitrary interpreted domains.

Main definitions

• Cslib.Logic.FO.Interpretation.WithConstants: formulas defining additional target constants.
• Cslib.Logic.FO.Interpretation.WithConstants.Valid: unique selection of a domain tuple.
• Cslib.Logic.FO.Interpretation.WithConstants.modelStructure: the expanded interpreted structure.
• Cslib.Logic.FO.Interpretation.WithConstants.onFormula: native formula pullback.

Main results

• Cslib.Logic.FO.Interpretation.WithConstants.realize_onFormula: formula truth preservation.
• Cslib.Logic.FO.Interpretation.WithConstants.realize_onSentence: sentence truth preservation.

References

• N. Immerman, Descriptive Complexity, Definitions 1.26 and 3.3, and Proposition 3.5. The explicit validity predicate supplies the well-definedness of constants.

structure Cslib.Logic.FO.Interpretation.WithConstants {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) (γ : Type u_3) : Type (max (max (max u u_1) u_3) v)

Additional target constants specified by formulas on the interpreted domain.

• constant : γ → L.Formula ι

  The defining formula for each constant; domain membership is imposed separately.

def Cslib.Logic.FO.Interpretation.WithConstants.Valid {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) (M : Type w) [L.Structure M] : Prop

Every target constant has exactly one value inside the interpreted domain.

noncomputable def Cslib.Logic.FO.Interpretation.WithConstants.value {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] (h : D.Valid M) (c : γ) : I.Model M

The unique interpreted-domain tuple selected by a valid constant definition.

theorem Cslib.Logic.FO.Interpretation.WithConstants.value_spec {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] (h : D.Valid M) (c : γ) : (D.constant c).Realize ↑(D.value h c)

theorem Cslib.Logic.FO.Interpretation.WithConstants.eq_value {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] (h : D.Valid M) (c : γ) (x : I.Model M) (hx : (D.constant c).Realize ↑x) : x = D.value h c

A tuple satisfying a constant definition is its selected value.

theorem Cslib.Logic.FO.Interpretation.WithConstants.Valid.of_eq {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] {L'' : FirstOrder.Language} {I' : Interpretation L L'' ι} {D' : I'.WithConstants γ} {D : I.WithConstants γ} (h : D.Valid M) (hdom : I'.domain = I.domain) (hcon : D'.constant = D.constant) : D'.Valid M

Validity depends only on the domain formula and the constant definitions.

theorem Cslib.Logic.FO.Interpretation.WithConstants.val_value_eq {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] {L'' : FirstOrder.Language} {I' : Interpretation L L'' ι} {D' : I'.WithConstants γ} {D : I.WithConstants γ} (hdom : I'.domain = I.domain) (hcon : D'.constant = D.constant) (h : D.Valid M) (h' : D'.Valid M) (c : γ) : ↑(D'.value h' c) = ↑(D.value h c)

Two constant extensions with the same domain and constant formulas select the same underlying tuples.

@[instance_reducible]

noncomputable def Cslib.Logic.FO.Interpretation.WithConstants.modelStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] [L'.IsRelational] (h : D.Valid M) : (L'.withConstants γ).Structure (I.Model M)

The interpreted relational structure expanded by its uniquely defined constants.

theorem Cslib.Logic.FO.Interpretation.WithConstants.modelStructure_coe_constant {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] [L'.IsRelational] (h : D.Valid M) (c : γ) : ↑(L'.con c) = D.value h c

A target constant denotes the uniquely selected interpreted-domain tuple.

noncomputable def Cslib.Logic.FO.Interpretation.WithConstants.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) [L'.IsRelational] [Finite ι] [Finite γ] {α : Type u_3} (φ : (L'.withConstants γ).Formula α) : L.Formula (α × ι)

Pull back a formula with target constants by quantifying their uniquely defined tuples.

theorem Cslib.Logic.FO.Interpretation.WithConstants.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] [L'.IsRelational] [Finite ι] [Finite γ] {α : Type u_3} (h : D.Valid M) (φ : (L'.withConstants γ).Formula α) (v : α → I.Model M) : ((D.onFormula φ).Realize fun (p : α × ι) => ↑(v p.1) p.2) ↔ φ.Realize v

The pullback preserves every assignment of the original free variables.

noncomputable def Cslib.Logic.FO.Interpretation.WithConstants.onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) [L'.IsRelational] [Finite ι] [Finite γ] (φ : (L'.withConstants γ).Sentence) : L.Sentence

Pull back a sentence containing the defined target constants.

theorem Cslib.Logic.FO.Interpretation.WithConstants.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {γ : Type u_2} {I : Interpretation L L' ι} (D : I.WithConstants γ) {M : Type w} [L.Structure M] [L'.IsRelational] [Finite ι] [Finite γ] (h : D.Valid M) (φ : (L'.withConstants γ).Sentence) : M ⊨ D.onSentence φ ↔ I.Model M ⊨ φ

Truth of a sentence is preserved by the constant-aware interpretation.