Countable connectives over arbitrary countable index types

BoundedFormulaω's iInf/iSup are ℕ-indexed. Constructions like the Hanf beth ladder (clause families over pairs of countable ordinals) and countable fragments quantify over countable-but-not-ℕ index types. This file provides the conjunction/disjunction over any countable index, in a two-layer API:

• the explicit-surjection core ciInfOfSurjective e φs / ciSupOfSurjective e φs — just iInf/iSup along e : ℕ → ι, with trivially-proved realization lemmas given Function.Surjective e;
• the [Countable ι] wrappers ciInf/ciSup, isolating the noncomputable enumeration choice (harmless defaults for empty ι: the tautology for ciInf, falsum for ciSup).

Only the realization lemmas are provided. No syntactic naturality API is built here: the enumeration is noncanonical, so definitional commutation statements would be unpleasant — consumers should work through realize_ciInf/realize_ciSup.

def FirstOrder.Language.BoundedFormulaω.ciInfOfSurjective {L : Language} {γ : Type} {n : ℕ} {ι : Type} (e : ℕ → ι) (φs : ι → L.BoundedFormulaω γ n) : L.BoundedFormulaω γ n

Countable conjunction along an explicit enumeration e : ℕ → ι.

Equations

• FirstOrder.Language.BoundedFormulaω.ciInfOfSurjective e φs = FirstOrder.Language.BoundedFormulaω.iInf fun (k : ℕ) => φs (e k)

def FirstOrder.Language.BoundedFormulaω.ciSupOfSurjective {L : Language} {γ : Type} {n : ℕ} {ι : Type} (e : ℕ → ι) (φs : ι → L.BoundedFormulaω γ n) : L.BoundedFormulaω γ n

Countable disjunction along an explicit enumeration e : ℕ → ι.

Equations

• FirstOrder.Language.BoundedFormulaω.ciSupOfSurjective e φs = FirstOrder.Language.BoundedFormulaω.iSup fun (k : ℕ) => φs (e k)

theorem FirstOrder.Language.BoundedFormulaω.realize_ciInfOfSurjective {L : Language} {γ : Type} {n : ℕ} {M : Type w} [L.Structure M] {ι : Type} {e : ℕ → ι} (he : Function.Surjective e) (φs : ι → L.BoundedFormulaω γ n) (v : γ → M) (xs : Fin n → M) : (ciInfOfSurjective e φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

theorem FirstOrder.Language.BoundedFormulaω.realize_ciSupOfSurjective {L : Language} {γ : Type} {n : ℕ} {M : Type w} [L.Structure M] {ι : Type} {e : ℕ → ι} (he : Function.Surjective e) (φs : ι → L.BoundedFormulaω γ n) (v : γ → M) (xs : Fin n → M) : (ciSupOfSurjective e φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

noncomputable def FirstOrder.Language.BoundedFormulaω.ciInf {L : Language} {γ : Type} {n : ℕ} {ι : Type} [Countable ι] (φs : ι → L.BoundedFormulaω γ n) : L.BoundedFormulaω γ n

Countable conjunction over a countable index type (tautology for empty ι).

Equations

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

noncomputable def FirstOrder.Language.BoundedFormulaω.ciSup {L : Language} {γ : Type} {n : ℕ} {ι : Type} [Countable ι] (φs : ι → L.BoundedFormulaω γ n) : L.BoundedFormulaω γ n

Countable disjunction over a countable index type (falsum for empty ι).

Equations

• FirstOrder.Language.BoundedFormulaω.ciSup φs = if h : Nonempty ι then FirstOrder.Language.BoundedFormulaω.ciSupOfSurjective ⋯.choose φs else FirstOrder.Language.BoundedFormulaω.falsum

theorem FirstOrder.Language.BoundedFormulaω.realize_ciInf {L : Language} {γ : Type} {n : ℕ} {M : Type w} [L.Structure M] {ι : Type} [Countable ι] (φs : ι → L.BoundedFormulaω γ n) (v : γ → M) (xs : Fin n → M) : (ciInf φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

theorem FirstOrder.Language.BoundedFormulaω.realize_ciSup {L : Language} {γ : Type} {n : ℕ} {M : Type w} [L.Structure M] {ι : Type} [Countable ι] (φs : ι → L.BoundedFormulaω γ n) (v : γ → M) (xs : Fin n → M) : (ciSup φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs