Semantic entailment for L_{ω₁ω} (issue #8 kernel step 1)

The frozen entailment convention of the Craig interpolation arc (docs/craig-audit.md §2): set-level entailment is the primitive, carriers are Type 0, and models are nonempty (standard model theory; forced here because the fresh-constant elimination arguments expand a base structure by constant interpretations, which no empty carrier admits).

Language.{0,0} throughout, per the arc's D2 freeze.

def FirstOrder.Language.Theoryω.Entails {L : Language} (T : L.Theoryω) (ψ : L.Sentenceω) : Prop

Semantic entailment from a theory (the primitive form): every nonempty Type 0 model of T realizes ψ.

Equations

• T.Entails ψ = ∀ (M : Type) [inst : L.Structure M] [Nonempty M], T.Model M → ψ.Realize M

def FirstOrder.Language.Sentenceω.Entails {L : Language} (φ ψ : L.Sentenceω) : Prop

Semantic entailment between sentences — the headline convention, derived from the set-level primitive.

Equations

• φ.Entails ψ = {φ}.Entails ψ

theorem FirstOrder.Language.Theoryω.entails_of_mem {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (h : φ ∈ T) : T.Entails φ

theorem FirstOrder.Language.Theoryω.Entails.mono {L : Language} {T T' : L.Theoryω} {φ : L.Sentenceω} (h : T.Entails φ) (hT : T ⊆ T') : T'.Entails φ

Entailment is monotone in the theory.

theorem FirstOrder.Language.Theoryω.Entails.cut {L : Language} {T : L.Theoryω} {φ ψ : L.Sentenceω} (hφ : T.Entails φ) (hψ : (insert φ T).Entails ψ) : T.Entails ψ

Cut: an entailed sentence can be added to the premises without changing entailments.

theorem FirstOrder.Language.Sentenceω.Entails.refl {L : Language} (φ : L.Sentenceω) : φ.Entails φ

theorem FirstOrder.Language.Sentenceω.entails_iff {L : Language} {φ ψ : L.Sentenceω} : φ.Entails ψ ↔ ∀ (M : Type) [inst : L.Structure M] [Nonempty M], φ.Realize M → ψ.Realize M

theorem FirstOrder.Language.Sentenceω.Entails.trans {L : Language} {φ ψ χ : L.Sentenceω} (h₁ : φ.Entails ψ) (h₂ : ψ.Entails χ) : φ.Entails χ