Semantic expansion of a two-sorted generated sublanguage (neutral prerequisite)

GeneratedSublanguage.lean is purely syntactic; this neutral companion adds the semantic side of the two-sorted symbol-generated sublanguage symbSublang F R: the base-language expansion of a sublanguage structure and its realization/entailment transport. Kept separate from GeneratedSublanguage.lean (which has no Structure/Realize dependency) and independent of any Conditional file.

• expandSymbStructureBase — from a (symbSublang F R).Structure M build an L.Structure M (symbols outside the generating sets interpreted arbitrarily / as False); the base analogue of the constants-expanded expandSymbStructure.
• reduct_expandSymbStructureBase — the reduct along symbSublangIncl F R recovers the original sublanguage structure.
• realize_restrictSymbols_expandSymbStructureBase — realizing φ.restrictSymbols in the sublanguage structure is realizing φ in the expansion (the high-leverage transport lemma).
• entails_restrictSymbols_singleton — a base-L entailment restricts to the sublanguage, via the expansion of an arbitrary sublanguage model.

@[reducible]

noncomputable def FirstOrder.Language.expandSymbStructureBase {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) {M : Type} [Nonempty M] [instM : (symbSublang F R).Structure M] : L.Structure M

Base expansion of a two-sorted sublanguage structure. Function/relation symbols in the generating sets are interpreted by the sublanguage structure; the rest are filled in arbitrarily (functions) / as False (relations).

Equations

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

theorem FirstOrder.Language.reduct_expandSymbStructureBase {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) {M : Type} [Nonempty M] [instM : (symbSublang F R).Structure M] : (symbSublangIncl F R).reduct M = instM

The reduct along symbSublangIncl recovers the original sublanguage structure.

theorem FirstOrder.Language.realize_restrictSymbols_expandSymbStructureBase {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) {M : Type} [Nonempty M] [instM : (symbSublang F R).Structure M] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (hF : φ.functionsIn ⊆ F) (hR : φ.relationsIn ⊆ R) (v : Empty → M) (xs : Fin n → M) : (φ.restrictSymbols hF hR).Realize v xs ↔ φ.Realize v xs

Realization transport: realizing φ.restrictSymbols in the sublanguage structure is realizing φ in the base expansion.

theorem FirstOrder.Language.entails_restrictSymbols_singleton {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (r₁ r₂ : L.Sentenceω) (hr₁F : BoundedFormulaω.functionsIn r₁ ⊆ F) (hr₁R : BoundedFormulaω.relationsIn r₁ ⊆ R) (hr₂F : BoundedFormulaω.functionsIn r₂ ⊆ F) (hr₂R : BoundedFormulaω.relationsIn r₂ ⊆ R) (hE : r₁.Entails r₂) : Sentenceω.Entails (BoundedFormulaω.restrictSymbols r₁ hr₁F hr₁R) (BoundedFormulaω.restrictSymbols r₂ hr₂F hr₂R)

Entailment transport (singleton form): a base-L entailment restricts to the sublanguage, via the base expansion of any sublanguage model.