Carrier transport for infinitary formulas

An infinitary formula branches over one fixed carrier. Along an index coding c : IndexCoding ι κ, a formula at carrier ι is transported to carrier κ by replacing each ι-indexed conjunction or disjunction with the corresponding coded connective at κ.

Transport is functorial: along the identity coding it is the identity, and along a composite coding it is the composite of the transports, both syntactically. It preserves realization, and it fixes the image of the finitary embedding. Along an equivalence of carriers it is a bijection of syntax, reindexEquiv. Along IndexCoding.ofEncodable, it recodes a formula over an encodable carrier into L_{ω₁ω}.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.reindex: transport along an index coding.
• FirstOrder.Language.BoundedFormulaInf.reindexEquiv: transport along a carrier equivalence, as an equivalence of syntax.
• FirstOrder.Language.BoundedFormulaInf.toOmega: recoding a formula over an encodable carrier into L_{ω₁ω}.

Main results

• FirstOrder.Language.BoundedFormulaInf.reindex_id and FirstOrder.Language.BoundedFormulaInf.reindex_trans: functoriality.
• FirstOrder.Language.BoundedFormulaInf.realize_reindex and FirstOrder.Language.BoundedFormulaInf.realize_toOmega: transport preserves realization.
• FirstOrder.Language.BoundedFormulaInf.reindex_toInf: transport fixes finitary formulas.

References

• Ported from cameronfreer/infinitary-logic at commit 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, whose carrier transport is Mathlib/ModelTheory/Infinitary/Reindex.lean in cameronfreer/mathlib4 at commit 346a4bd3f95e8591976c91259badc6d2c300f638.
• Divergences from these sources: the coded connectives are in a separate module; the body of reindex is not exposed and is used through its constructor equations; the round trip along an equivalence is derived from IndexCoding.ofEquiv_trans_ofEquiv_symm.

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

Transport a formula along a coding of its carrier: each ι-indexed conjunction or disjunction becomes the corresponding coded connective at carrier κ.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_falsum {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) : reindex c falsum = falsum

Transport fixes the false formula.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_equal {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (t₁ t₂ : L.Term (α ⊕ Fin n)) : reindex c (equal t₁ t₂) = equal t₁ t₂

Transport fixes equations.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_rel {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : reindex c (rel R ts) = rel R ts

Transport fixes relational atoms.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_imp {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φ ψ : L.BoundedFormulaInf ι α n) : reindex c (φ.imp ψ) = (reindex c φ).imp (reindex c ψ)

Transport commutes with implication.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_all {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α (n + 1)) : reindex c φ.all = (reindex c φ).all

Transport commutes with universal quantification.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_iSup {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf ι α n) : reindex c (iSup φs) = iSupAlong c fun (i : ι) => reindex c (φs i)

Transport turns a disjunction over the carrier into the coded disjunction.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_iInf {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf ι α n) : reindex c (iInf φs) = iInfAlong c fun (i : ι) => reindex c (φs i)

Transport turns a conjunction over the carrier into the coded conjunction.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_not {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α n) : reindex c φ.not = (reindex c φ).not

Transport commutes with negation.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_ex {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α (n + 1)) : reindex c φ.ex = (reindex c φ).ex

Transport commutes with existential quantification.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_top {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) : reindex c ⊤ = ⊤

Transport fixes ⊤.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_bot {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : TauCeti.IndexCoding ι κ) : reindex c ⊥ = ⊥

Transport fixes ⊥.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_id {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : reindex (TauCeti.IndexCoding.id ι) φ = φ

Transport along the identity coding is the identity, syntactically.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_alls {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : TauCeti.IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : reindex c φ.alls = (reindex c φ).alls

Transport commutes with the universal closure of all bound-variable slots.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_exs {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : TauCeti.IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : reindex c φ.exs = (reindex c φ).exs

Transport commutes with the existential closure of all bound-variable slots.

theorem FirstOrder.Language.BoundedFormulaInf.reindex_trans {L : Language} {ι : Type uι} {κ : Type uκ} {μ : Type uμ} {α : Type u'} (c₁ : TauCeti.IndexCoding ι κ) (c₂ : TauCeti.IndexCoding κ μ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : reindex (c₁.trans c₂) φ = reindex c₂ (reindex c₁ φ)

Transport along a composite coding is the composite of the transports, syntactically.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_ofEquiv_symm_reindex_ofEquiv {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) (φ : L.BoundedFormulaInf ι α n) : reindex (TauCeti.IndexCoding.ofEquiv e.symm) (reindex (TauCeti.IndexCoding.ofEquiv e) φ) = φ

Transport along an equivalence and back is the identity, syntactically.

def FirstOrder.Language.BoundedFormulaInf.reindexEquiv {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) : L.BoundedFormulaInf ι α n ≃ L.BoundedFormulaInf κ α n

A carrier equivalence is an equivalence of syntax: transport along it and along its inverse are mutually inverse.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindexEquiv_apply {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) (φ : L.BoundedFormulaInf ι α n) : (reindexEquiv e) φ = reindex (TauCeti.IndexCoding.ofEquiv e) φ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindexEquiv_symm_apply {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) (φ : L.BoundedFormulaInf κ α n) : (reindexEquiv e).symm φ = reindex (TauCeti.IndexCoding.ofEquiv e.symm) φ

def FirstOrder.Language.BoundedFormulaInf.toOmega {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} [Encodable ι] (φ : L.BoundedFormulaInf ι α n) : L.BoundedFormulaω α n

Recode a formula over an encodable carrier into L_{ω₁ω}, by transport along the coding IndexCoding.ofEncodable.

theorem FirstOrder.Language.BoundedFormulaInf.toOmega_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} [Encodable ι] (φ : L.BoundedFormulaInf ι α n) : φ.toOmega = reindex (TauCeti.IndexCoding.ofEncodable ι) φ

The recoding into L_{ω₁ω} is transport along IndexCoding.ofEncodable.

@[simp]

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

Transport preserves realization.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_toOmega {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] [Encodable ι] (φ : L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) : Realize φ.toOmega v xs ↔ φ.Realize v xs

Recoding into L_{ω₁ω} preserves realization.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.reindex_toInf {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : TauCeti.IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormula α n) : reindex c φ.toInf = φ.toInf

Transport fixes finitary formulas: the finitary embedding at carrier κ factors through every coding into κ.