The semantic gap condition (*) and the member predicate (issue #12, commit 4a)

Marker's property (*), in the frozen representation: a consistency-property member is S = Bφ ∪ Γ with Γ finite, and for every α < ω₁ there is an approximating model in which

• the root φ holds (in the base L-structure),
• every sentence of the finite remainder Γ holds (in the controlled constant expansion wc), and
• the rational constants mentioned by Γ are marked on an lt-chain with α-margins (a GapWitness over a strictly monotone enumeration that covers — possibly over-approximates — the mentioned rationals).

Deliberately, the witness does not realize the entire positive diagram Bφ (review acceptance check 1): a mentioned atom d_q < d_r is derived from the chain through the marks (StarWitness.realize_marked_atom), and unmentioned atoms are represented only by the chain/gap conditions.

WOMem is the member predicate: base containment, finite remainder, finite constant support, universe containment (the kernel's GenU, whose seed already holds every constant relation atom — in particular all of Bφ's diagram), and (*) at every countable ordinal.

Mentioned rational constants

def FirstOrder.Language.ratSupport {L : Language} (Γ : Set (L.withConstants ℕ).Sentenceω) : Set ℚ

The rationals whose constants are mentioned by a set of expansion sentences.

Equations

• FirstOrder.Language.ratSupport Γ = {q : ℚ | ∃ χ ∈ Γ, FirstOrder.Language.ratConstIdx q ∈ FirstOrder.Language.sentenceJConsts χ}

theorem FirstOrder.Language.ratSupport_mono {L : Language} {Γ Γ' : Set (L.withConstants ℕ).Sentenceω} (h : Γ ⊆ Γ') : ratSupport Γ ⊆ ratSupport Γ'

Monotonicity of the mentioned-rationals set.

The star witness

structure FirstOrder.Language.StarWitness {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (Γ : Set (L.withConstants ℕ).Sentenceω) (α : Ordinal.{0}) : Type 1

The (*) witness at level α: an approximating model realizing the root and the finite remainder, with the mentioned rationals marked on an lt-chain with α-margins. The marking enumeration may over-approximate the mentioned set (mark_cover is ⊆, not =) — closure rules extend it monotonically.

• M : Type

  the approximating model

• inst : L.Structure self.M
• ne : Nonempty self.M
• h : ℕ → self.M

  the constant interpretation

• base_realize : φ.Realize self.M

  the root holds in the base structure

• rem_realize (χ : (L.withConstants ℕ).Sentenceω) : χ ∈ Γ → χ.Realize self.M

  every remainder sentence holds in the controlled expansion

• m : ℕ

  number of marked rationals

• mark : Fin self.m → ℚ

  the marked rationals, in increasing order

• mark_mono : StrictMono self.mark
• mark_cover : ratSupport Γ ⊆ Set.range self.mark

  the marking covers every mentioned rational

• witness : GapWitness lt α fun (i : Fin self.m) => self.h (ratConstIdx (self.mark i))

  the marked constants sit on a chain with α-margins

def FirstOrder.Language.StarCondition {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (Γ : Set (L.withConstants ℕ).Sentenceω) (α : Ordinal.{0}) : Prop

The (*) condition: a witness exists.

Equations

• FirstOrder.Language.StarCondition φ lt Γ α = Nonempty (FirstOrder.Language.StarWitness φ lt Γ α)

theorem FirstOrder.Language.StarCondition.mono {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α β : Ordinal.{0}} (hβ : β ≤ α) (h : StarCondition φ lt Γ α) : StarCondition φ lt Γ β

Downward closure of (*) in α (via GapWitness.mono) — the consumer of the cofinal-fiber argument.

theorem FirstOrder.Language.StarCondition.mono_subset {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ Γ' : Set (L.withConstants ℕ).Sentenceω} (hΓ : Γ' ⊆ Γ) {α : Ordinal.{0}} (h : StarCondition φ lt Γ α) : StarCondition φ lt Γ' α

Shrinking the remainder preserves (*) (the marking still covers the smaller support).

Atomic realization at the controlled expansion

theorem FirstOrder.Language.realize_constTermS_wc {L : Language} {M : Type} {base : L.Structure M} {h : ℕ → M} (c : ℕ) (v : Empty ⊕ Fin 0 → M) : Term.realize v (constTermS c) = h c

The sentence-context constant realizes to its h-value at the controlled expansion.

theorem FirstOrder.Language.realize_relInst_wc {L : Language} {M : Type} {base : L.Structure M} {h : ℕ → M} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : (relInst R g).Realize M ↔ Structure.RelMap R fun (i : Fin l) => h (g i)

A constant relation instance realizes at the controlled expansion to the base relation on the constant values.

theorem FirstOrder.Language.realize_constEq_wc {L : Language} {M : Type} {base : L.Structure M} {h : ℕ → M} (a b : ℕ) : (constEq a b).Realize M ↔ h a = h b

A constant equality realizes at the controlled expansion to equality of the values.

The derived diagram: marked atoms hold through the chain

theorem FirstOrder.Language.StarWitness.realize_marked_atom {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) (hα : 0 < α) {i j : Fin W.m} (hij : i < j) : (ratLtAtom lt (W.mark i) (W.mark j)).Realize W.M

The mentioned-diagram derivation (review acceptance check 5): a positive diagram atom whose rationals are both marked holds in the witness's expansion — through RelChain and the marks, never by assuming the model realizes the diagram. Requires 0 < α (at α = 0 the margins are vacuous); consumers instantiate (*) at any positive level.

The member predicate

structure FirstOrder.Language.WOMem {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (S : Set (L.withConstants ℕ).Sentenceω) : Prop

The consistency-property member predicate (frozen D4): S = Bφ ∪ Γ with Γ finite — stated as base containment plus finiteness of the remainder — together with finite constant support of the remainder, containment in the kernel's enumeration universe (rooted at the lifted φ; the universe's seed already holds every constant relation atom, hence all of Bφ), and the semantic condition (*) at every countable ordinal.

• base_subset : baseDiagram φ lt ⊆ S
• rem_finite : (S \ baseDiagram φ lt).Finite
• rem_support : (⋃ χ ∈ S \ baseDiagram φ lt, sentenceJConsts χ).Finite
• subset_U : S ⊆ GenU (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ)
• star (α : Ordinal.{0}) : α < (Cardinal.aleph 1).ord → StarCondition φ lt (S \ baseDiagram φ lt) α