Coded infinitary connectives

An infinitary formula branches over one fixed carrier κ. A conjunction or disjunction indexed by another type ι is expressed at κ along an index coding c : IndexCoding ι κ: each index k : κ that decodes to i : ι carries the i-th branch, and each undecodable index carries a semantically neutral branch, ⊤ for a conjunction and ⊥ for a disjunction. Indices that decode to the same i carry the same branch. The realization of the coded connective is therefore the ι-indexed conjunction or disjunction, whatever the coding.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.iInfAlong: the ι-indexed conjunction at carrier κ.
• FirstOrder.Language.BoundedFormulaInf.iSupAlong: the ι-indexed disjunction at carrier κ.

Main results

• FirstOrder.Language.BoundedFormulaInf.realize_iInfAlong: the coded conjunction is realized exactly when every branch is.
• FirstOrder.Language.BoundedFormulaInf.realize_iSupAlong: the coded disjunction is realized exactly when some branch is.

References

• Ported from cameronfreer/infinitary-logic at commit 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, whose coded connectives are in Mathlib/ModelTheory/Infinitary/Reindex.lean in cameronfreer/mathlib4 at commit 346a4bd3f95e8591976c91259badc6d2c300f638.
• Divergences from these sources: the coded connectives have their own module, apart from whole-formula transport; their bodies are not exposed and are used through the defining equations iInfAlong_def and iSupAlong_def; the realization laws are derived from the padding laws IndexCoding.comp_pad, IndexCoding.forall_pad_true_iff and IndexCoding.exists_pad_false_iff.

def FirstOrder.Language.BoundedFormulaInf.iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : L.BoundedFormulaInf κ α n

The coded conjunction of an ι-indexed family at carrier κ, along a coding: an index decoding to i carries the i-th conjunct, and an undecodable index carries ⊤.

def FirstOrder.Language.BoundedFormulaInf.iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : L.BoundedFormulaInf κ α n

The coded disjunction of an ι-indexed family at carrier κ, along a coding: an index decoding to i carries the i-th disjunct, and an undecodable index carries ⊥.

theorem FirstOrder.Language.BoundedFormulaInf.iInfAlong_def {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : iInfAlong c φs = iInf (c.pad ⊤ φs)

The coded conjunction is the carrier conjunction of the family padded with ⊤.

theorem FirstOrder.Language.BoundedFormulaInf.iSupAlong_def {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : iSupAlong c φs = iSup (c.pad ⊥ φs)

The coded disjunction is the carrier disjunction of the family padded with ⊥.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : TauCeti.IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} : (iInfAlong c φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

The coded conjunction is realized exactly when every conjunct is. The padding branches are ⊤, which is always realized.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : TauCeti.IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} : (iSupAlong c φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

The coded disjunction is realized exactly when some disjunct is. The padding branches are ⊥, which is never realized.