Language maps on infinitary formulas

A language homomorphism g : L →ᴸ L' acts on the infinitary formulas of L, at every carrier ι, symbol by symbol: each term is mapped by Mathlib's LHom.onTerm, each relation symbol by g.onRelation, and the logical structure is kept. This is the infinitary form of Mathlib's LHom.onBoundedFormula.

When an L'-structure on M expands an L-structure along g (g.IsExpansionOn M), the image of a formula is realized exactly when the formula is. Every passage between languages, such as adding constants or restricting to the symbols a formula mentions, transfers truth through this result.

Main definitions

• FirstOrder.Language.LHom.onBoundedFormulaInf: the action of a language homomorphism on infinitary formulas.

Main results

• FirstOrder.Language.LHom.realize_onBoundedFormulaInf: along an expansion, the image of a formula is realized exactly when the formula is.
• FirstOrder.Language.LHom.realize_sentenceInf_onBoundedFormulaInf: its form for sentences.
• FirstOrder.Language.LHom.id_onBoundedFormulaInf and FirstOrder.Language.LHom.comp_onBoundedFormulaInf: the action is functorial.
• FirstOrder.Language.LHom.onBoundedFormulaInf_toInf, FirstOrder.Language.LHom.onBoundedFormulaInf_mapBound, FirstOrder.Language.LHom.onBoundedFormulaInf_castLE and FirstOrder.Language.LHom.onBoundedFormulaInf_reindex: the action commutes with the embedding of finitary formulas, with relabelling and weakening of bound-variable slots, and with transport along a coding of carriers; along the way it commutes with ⊥, ⊤, negation, existential quantification and the coded connectives iInfAlong and iSupAlong.
• FirstOrder.Language.LEquiv.realize_onBoundedFormulaInf: realization is preserved by translation along a language equivalence, the target structure being the reduct along the inverse map.

References

• Ported from cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b: mapLanguage and realize_mapLanguage in InfinitaryLogic/Lomega1omega/Operations.lean.
• Divergences from that source: the action is defined at every carrier ι rather than at ℕ, between languages in arbitrary universes rather than a common one, and as a method of the language homomorphism named after Mathlib's finitary LHom.onBoundedFormula; the functor laws are new.

def FirstOrder.Language.LHom.onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} : L.BoundedFormulaInf ι α n → L'.BoundedFormulaInf ι α n

The action of a language homomorphism on infinitary formulas: each term is mapped by g.onTerm, each relation symbol by g.onRelation, and the logical structure is kept.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_falsum {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} : g.onBoundedFormulaInf BoundedFormulaInf.falsum = BoundedFormulaInf.falsum

A language map fixes the false formula.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_equal {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : g.onBoundedFormulaInf (BoundedFormulaInf.equal t₁ t₂) = BoundedFormulaInf.equal (g.onTerm t₁) (g.onTerm t₂)

A language map maps both sides of an equation.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_rel {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : g.onBoundedFormulaInf (BoundedFormulaInf.rel R ts) = BoundedFormulaInf.rel (g.onRelation R) fun (i : Fin l) => g.onTerm (ts i)

A language map maps the relation symbol and the terms of a relational atom.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_imp {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (φ.imp ψ) = (g.onBoundedFormulaInf φ).imp (g.onBoundedFormulaInf ψ)

A language map commutes with implication.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_all {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : g.onBoundedFormulaInf φ.all = (g.onBoundedFormulaInf φ).all

A language map commutes with universal quantification.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_iSup {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (BoundedFormulaInf.iSup φs) = BoundedFormulaInf.iSup fun (i : ι) => g.onBoundedFormulaInf (φs i)

A language map commutes with disjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_iInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (BoundedFormulaInf.iInf φs) = BoundedFormulaInf.iInf fun (i : ι) => g.onBoundedFormulaInf (φs i)

A language map commutes with conjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.LHom.realize_onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {M : Type w} [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) : (g.onBoundedFormulaInf φ).Realize v xs ↔ φ.Realize v xs

Realization along an expansion. If the L'-structure on M expands its L-structure along g, the image of an infinitary formula under g is realized exactly when the formula is. This is the infinitary form of Mathlib's LHom.realize_onBoundedFormula.

@[simp]

theorem FirstOrder.Language.LHom.realize_sentenceInf_onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} (g : L →ᴸ L') {M : Type w} [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] (φ : L.SentenceInf ι) : SentenceInf.Realize (g.onBoundedFormulaInf φ) M ↔ φ.Realize M

Realization of sentences along an expansion. If the L'-structure on M expands its L-structure along g, the image of an infinitary sentence under g holds exactly when the sentence does.

@[simp]

theorem FirstOrder.Language.LHom.id_onBoundedFormulaInf {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : (LHom.id L).onBoundedFormulaInf φ = φ

The identity language map acts as the identity on infinitary formulas.

@[simp]

theorem FirstOrder.Language.LHom.comp_onBoundedFormulaInf {L : Language} {L' : Language} {L'' : Language} {ι : Type uι} {α : Type uα} (g : L' →ᴸ L'') (f : L →ᴸ L') {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : (g.comp f).onBoundedFormulaInf φ = g.onBoundedFormulaInf (f.onBoundedFormulaInf φ)

The action of a composite language map is the composite of the actions.

Commutation with the operations on formulas

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_bot {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} : g.onBoundedFormulaInf ⊥ = ⊥

A language map fixes ⊥.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_not {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf φ.not = (g.onBoundedFormulaInf φ).not

A language map commutes with negation.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_ex {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : g.onBoundedFormulaInf φ.ex = (g.onBoundedFormulaInf φ).ex

A language map commutes with existential quantification.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_top {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} : g.onBoundedFormulaInf ⊤ = ⊤

A language map fixes ⊤.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_iInfAlong {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} {ι' : Type u_1} (c : TauCeti.IndexCoding ι' ι) (φs : ι' → L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (BoundedFormulaInf.iInfAlong c φs) = BoundedFormulaInf.iInfAlong c fun (i : ι') => g.onBoundedFormulaInf (φs i)

A language map commutes with coded conjunctions.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_iSupAlong {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} {ι' : Type u_1} (c : TauCeti.IndexCoding ι' ι) (φs : ι' → L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (BoundedFormulaInf.iSupAlong c φs) = BoundedFormulaInf.iSupAlong c fun (i : ι') => g.onBoundedFormulaInf (φs i)

A language map commutes with coded disjunctions.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_toInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {n : ℕ} (φ : L.BoundedFormula α n) : g.onBoundedFormulaInf φ.toInf = (g.onBoundedFormula φ).toInf

A language map commutes with the embedding of finitary formulas: translating a finitary formula and then embedding it is embedding it and then translating.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_mapBound {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {m n : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) : g.onBoundedFormulaInf (BoundedFormulaInf.mapBound f φ) = BoundedFormulaInf.mapBound f (g.onBoundedFormulaInf φ)

A language map commutes with relabelling the bound-variable slots.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_castLE {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) : g.onBoundedFormulaInf (BoundedFormulaInf.castLE h φ) = BoundedFormulaInf.castLE h (g.onBoundedFormulaInf φ)

A language map commutes with weakening.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_reindex {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} {κ : Type u_1} (g : L →ᴸ L') (c : TauCeti.IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : g.onBoundedFormulaInf (BoundedFormulaInf.reindex c φ) = BoundedFormulaInf.reindex c (g.onBoundedFormulaInf φ)

A language map commutes with transporting formulas along a coding of carriers.

@[simp]

theorem FirstOrder.Language.LEquiv.realize_onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (e : L ≃ᴸ L') {M : Type w} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) : (e.toLHom.onBoundedFormulaInf φ).Realize v xs ↔ φ.Realize v xs

Realization along a language equivalence. An L-structure, reinterpreted as an L'-structure along the inverse map, realizes the translation of an infinitary formula exactly when it realizes the formula.