The source-fragment adapter: from an honest fragment to a Henkin-closed universe

Syntactic model existence for a theory inside an honest Fragment of a relational language, through the constants-expanded universe of that fragment (issue #19B, step 3).

The constants-expanded universe

Fragment.withNatConstantsSentences F is the set of sentences of L[[ℕ]] obtained by taking a member ⟨n, φ⟩ of F at any arity, mapping it into the constants expansion, and closing its n bound variables by constants. Every arity contributes: that is what makes universal-instance closure follow from Fragment.all_mem (the body of a universal is a member at arity n + 1, and appending the chosen constant to the parameter tuple is the instance — instConst_closeBy_all_remainder). No substitution field is added to any fragment structure.

The basis

Fragment deliberately omits what the kernel's atomic and negation fields need; Fragment.HenkinBasis supplies exactly that: falsum, closure under negation at every arity, one equality template at arity two, and one relation template per symbol. Closing the templates by constants produces every constEq and every relInst. The adapter consumes only Fragment and HenkinBasis; the coded-family closure of AdmissibleFragment never enters.

The theorem

Fragment.exists_countable_model_of_aconsistent_withConstants: for a countable fragment with a basis, a theory T ⊆ F.sentenceSlice that is consistent in the expanded universe has a countable model of T itself, as an L-structure, obtained by forgetting the constants. The hypothesis is consistency in withNatConstantsSentences F, and the theorem is named for it. Transporting base-language consistency into the expanded universe is a separate question, recorded as a deferred design branch in docs/admissible-interface-contract.md §8.

Sentence slice and the constants-expanded universe

def FirstOrder.Language.Fragment.sentenceSlice {L : Language} (F : L.Fragment) : Set L.Sentenceω

The sentences of a fragment: its members at arity zero.

Equations

• F.sentenceSlice = {φ : L.Sentenceω | ⟨0, φ⟩ ∈ F}

theorem FirstOrder.Language.Fragment.mem_sentenceSlice {L : Language} {F : L.Fragment} {φ : L.Sentenceω} : φ ∈ F.sentenceSlice ↔ ⟨0, φ⟩ ∈ F

def FirstOrder.Language.Fragment.withNatConstantsSentences {L : Language} (F : L.Fragment) : Set (L.withConstants ℕ).Sentenceω

The constants-expanded universe: every member of F, at every arity, mapped into L[[ℕ]] and closed by constants.

Equations

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

theorem FirstOrder.Language.Fragment.closeBy_mapLanguage_mem {L : Language} {F : L.Fragment} {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : ⟨n, φ⟩ ∈ F) (a : Fin n → ℕ) : closeBy (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) a ∈ F.withNatConstantsSentences

theorem FirstOrder.Language.Fragment.mapLanguage_mem_withNatConstantsSentences {L : Language} {F : L.Fragment} {φ : L.Sentenceω} (h : φ ∈ F.sentenceSlice) : BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ ∈ F.withNatConstantsSentences

Theory inclusion: a sentence of the fragment, mapped into the expansion, lies in the universe.

theorem FirstOrder.Language.Fragment.mapLanguage_image_subset {L : Language} {F : L.Fragment} {T : Set L.Sentenceω} (hT : T ⊆ F.sentenceSlice) : BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T ⊆ F.withNatConstantsSentences

theorem FirstOrder.Language.Fragment.withNatConstantsSentences_countable {L : Language} {F : L.Fragment} (hF : F.toSet.Countable) : F.withNatConstantsSentences.Countable

Countability: countably many members, each with countably many parameter tuples.

The basis

def FirstOrder.Language.Fragment.equalTemplate (L : Language) : L.BoundedFormulaω Empty 2

The equality template x₀ = x₁ at arity two.

Equations

• FirstOrder.Language.Fragment.equalTemplate L = FirstOrder.Language.BoundedFormulaω.equal (FirstOrder.Language.var (Sum.inr 0)) (FirstOrder.Language.var (Sum.inr 1))

def FirstOrder.Language.Fragment.relTemplate {L : Language} {l : ℕ} (R : L.Relations l) : L.BoundedFormulaω Empty l

The relation template R(x₀, …, x_{l-1}) at arity l.

Equations

• FirstOrder.Language.Fragment.relTemplate R = FirstOrder.Language.BoundedFormulaω.rel R fun (i : Fin l) => FirstOrder.Language.var (Sum.inr i)

structure FirstOrder.Language.Fragment.HenkinBasis {L : Language} (F : L.Fragment) : Prop

The Henkin basis of a fragment: what Fragment omits and the kernel's atomic and negation fields need. Separate from AdmissibleFragment; no fragment structure gains a field.

• falsum_mem : ⟨0, BoundedFormulaω.falsum⟩ ∈ F
• not_mem {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ F → ⟨n, φ.not⟩ ∈ F
• equalTemplate_mem : ⟨2, equalTemplate L⟩ ∈ F
• relTemplate_mem {l : ℕ} (R : L.Relations l) : ⟨l, relTemplate R⟩ ∈ F

theorem FirstOrder.Language.Fragment.henkinBasis_hfFragment {L : Language} : L.hfFragment.HenkinBasis

The finitary fragment has a basis.

theorem FirstOrder.Language.Fragment.henkinBasis_top {L : Language} : top.HenkinBasis

The full fragment has a basis.

Closing the templates gives the atoms

theorem FirstOrder.Language.Fragment.closeBy_equalTemplate {L : Language} (a b : ℕ) : closeBy (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) (equalTemplate L)) ![a, b] = constEq a b

theorem FirstOrder.Language.Fragment.closeBy_relTemplate {L : Language} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : closeBy (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) (relTemplate R)) g = relInst R g

Decomposing a member of the universe by its head constructor

The universe is Henkin-closed

theorem FirstOrder.Language.Fragment.henkinClosed_withNatConstantsSentences {L : Language} {F : L.Fragment} (hB : F.HenkinBasis) : HenkinClosed F.withNatConstantsSentences

The constants-expanded universe of a fragment with a basis is Henkin-closed. Connective components come from the fragment's component closure, negation and the atoms from the basis, and universal instances from Fragment.all_mem through instConst_closeBy_all_remainder.

Assembly

theorem FirstOrder.Language.Fragment.model_reduct_of_model_mapLanguage_image {L : Language} (T : L.Theoryω) {N : Type} [(L.withConstants ℕ).Structure N] (h : Theoryω.Model (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T) N) : T.Model N

Forgetting the constants: an L[[ℕ]]-model of the mapped theory is, as its L-reduct, a model of the theory. A three-line argument from realize_mapLanguage, kept local so that no Marker-stage module is imported.

theorem FirstOrder.Language.Fragment.exists_countable_model_of_aconsistent_withConstants {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {F : L.Fragment} (hF : F.toSet.Countable) (hB : F.HenkinBasis) {T : L.Theoryω} (hT : T ⊆ F.sentenceSlice) (hcons : AConsistent F.withNatConstantsSentences (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' T)) : ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (_ : Countable M), T.Model M

Syntactic model existence over a source fragment (relational core). A theory inside a countable fragment with a basis that is consistent in the fragment's constants-expanded universe has a countable model, as an L-structure. No countability of T; the consistency hypothesis is in the expanded universe, and the theorem is named for it.