Quantifier Complexity #

This file defines quantifier complexity of first-order formulas, and constructs prenex normal forms.

Main Definitions #

FirstOrder.Language.BoundedFormula.IsAtomic defines atomic formulas - those which are constructed only from terms and relations.
FirstOrder.Language.BoundedFormula.IsQF defines quantifier-free formulas - those which are constructed only from atomic formulas and boolean operations.
FirstOrder.Language.BoundedFormula.IsPrenex defines when a formula is in prenex normal form - when it consists of a series of quantifiers applied to a quantifier-free formula.
FirstOrder.Language.BoundedFormula.toPrenex constructs a prenex normal form of a given formula.

Main Results #

FirstOrder.Language.BoundedFormula.realize_toPrenex shows that the prenex normal form of a formula has the same realization as the original formula.

inductive FirstOrder.Language.BoundedFormula.IsAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → Prop

An atomic formula is either equality or a relation symbol applied to terms. Note that ⊥ and ⊤ are not considered atomic in this convention.

equal: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)), (t₁.bdEqual t₂).IsAtomic
rel: ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)), (R.boundedFormula ts).IsAtomic

Instances For

source

theorem FirstOrder.Language.BoundedFormula.not_all_isAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :

¬φ.all.IsAtomic

source

theorem FirstOrder.Language.BoundedFormula.not_ex_isAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :

¬φ.ex.IsAtomic

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsAtomic) (f : α → β ⊕ Fin n) :

(FirstOrder.Language.BoundedFormula.relabel f φ).IsAtomic

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k : ℕ} {m : ℕ} (h : φ.IsAtomic) :

(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsAtomic

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.castLE {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {l : ℕ} {φ : L.BoundedFormula α l} {h : l ≤ n} (hφ : φ.IsAtomic) :

(FirstOrder.Language.BoundedFormula.castLE h φ).IsAtomic

source

inductive FirstOrder.Language.BoundedFormula.IsQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → Prop

A quantifier-free formula is a formula defined without quantifiers. These are all equivalent to boolean combinations of atomic formulas.

falsum: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, FirstOrder.Language.BoundedFormula.falsum.IsQF
of_isAtomic: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsQF
imp: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ₁ φ₂ : L.BoundedFormula α n}, φ₁.IsQF → φ₂.IsQF → (φ₁.imp φ₂).IsQF

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} :

φ.IsAtomic → φ.IsQF

source

theorem FirstOrder.Language.BoundedFormula.isQF_bot {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

⊥.IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) :

φ.not.IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.top {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

⊤.IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.sup {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) :

(φ ⊔ ψ).IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.inf {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) :

(φ ⊓ ψ).IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsQF) (f : α → β ⊕ Fin n) :

(FirstOrder.Language.BoundedFormula.relabel f φ).IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k : ℕ} {m : ℕ} (h : φ.IsQF) :

(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsQF

source

theorem FirstOrder.Language.BoundedFormula.IsQF.castLE {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {l : ℕ} {φ : L.BoundedFormula α l} {h : l ≤ n} (hφ : φ.IsQF) :

(FirstOrder.Language.BoundedFormula.castLE h φ).IsQF

source

theorem FirstOrder.Language.BoundedFormula.not_all_isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :

¬φ.all.IsQF

source

theorem FirstOrder.Language.BoundedFormula.not_ex_isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :

¬φ.ex.IsQF

source

inductive FirstOrder.Language.BoundedFormula.IsPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → Prop

Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers applied to a quantifier-free formula.

of_isQF: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsPrenex
all: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → φ.all.IsPrenex
ex: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → φ.ex.IsPrenex

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsQF.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} :

φ.IsQF → φ.IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :

φ.IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {n : ℕ} → L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : φ.IsPrenex) (hq : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (ha : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) (hn : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, P ψ → P ψ.not) :

P φ

source

theorem FirstOrder.Language.BoundedFormula.IsPrenex.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsPrenex) (f : α → β ⊕ Fin n) :

(FirstOrder.Language.BoundedFormula.relabel f φ).IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.IsPrenex.castLE {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} (hφ : φ.IsPrenex) {n : ℕ} {h : l ≤ n} :

(FirstOrder.Language.BoundedFormula.castLE h φ).IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.IsPrenex.liftAt {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k : ℕ} {m : ℕ} (h : φ.IsPrenex) :

(FirstOrder.Language.BoundedFormula.liftAt k m φ).IsPrenex

source

def FirstOrder.Language.BoundedFormula.toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n

An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ is quantifier-free and ψ is in prenex normal form, then φ.toPrenexImpRight ψ is a prenex normal form for φ.imp ψ.

Equations

One or more equations did not get rendered due to their size.
x.toPrenexImpRight ψ.all = ((FirstOrder.Language.BoundedFormula.liftAt 1 x✝ x).toPrenexImpRight ψ).all
x✝.toPrenexImpRight x = x✝.imp x

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} :

ψ.IsQF → φ.toPrenexImpRight ψ = φ.imp ψ

source

theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsPrenex) :

(φ.toPrenexImpRight ψ).IsPrenex

source

def FirstOrder.Language.BoundedFormula.toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n

An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ and ψ are in prenex normal form, then φ.toPrenexImp ψ is a prenex normal form for φ.imp ψ.

Equations

((φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum).toPrenexImp x = (φ.toPrenexImp (FirstOrder.Language.BoundedFormula.liftAt 1 x✝ x)).all
φ.all.toPrenexImp x = (φ.toPrenexImp (FirstOrder.Language.BoundedFormula.liftAt 1 x✝ x)).ex
x✝.toPrenexImp x = x✝.toPrenexImpRight x

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} :

φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ

source

theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsPrenex) (hψ : ψ.IsPrenex) :

(φ.toPrenexImp ψ).IsPrenex

source

def FirstOrder.Language.BoundedFormula.toPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → L.BoundedFormula α n

For any bounded formula φ, φ.toPrenex is a semantically-equivalent formula in prenex normal form.

Equations

FirstOrder.Language.BoundedFormula.falsum.toPrenex = ⊥
(FirstOrder.Language.BoundedFormula.equal t₁ t₂).toPrenex = t₁.bdEqual t₂
(FirstOrder.Language.BoundedFormula.rel R ts).toPrenex = FirstOrder.Language.BoundedFormula.rel R ts
(f₁.imp f₂).toPrenex = f₁.toPrenex.toPrenexImp f₂.toPrenex
f.all.toPrenex = f.toPrenex.all

Instances For

source

theorem FirstOrder.Language.BoundedFormula.toPrenex_isPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) :

φ.toPrenex.IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsPrenex) {v : α → M} {xs : Fin n → M} :

(φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

source

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsPrenex) (hψ : ψ.IsPrenex) {v : α → M} {xs : Fin n → M} :

(φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_toPrenex {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M] (φ : L.BoundedFormula α n) {v : α → M} {xs : Fin n → M} :

φ.toPrenex.Realize v xs ↔ φ.Realize v xs

source

theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ⊥) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) (hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :

P φ

source

theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ⊥) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) (hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :

P φ

source

theorem FirstOrder.Language.BoundedFormula.iff_toPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) :

∅.Iff φ φ.toPrenex

source

theorem FirstOrder.Language.BoundedFormula.induction_on_all_ex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n) (hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) (hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) (hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :

P φ

source

theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n) (hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (hnot : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, P φ → P φ.not) (hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) (hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) :

P φ

source

inductive FirstOrder.Language.BoundedFormula.IsUniversal {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → Prop

A universal formula is a formula defined by applying only universal quantifiers to a quantifier-free formula.

of_isQF: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsUniversal
all: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsUniversal → φ.all.IsUniversal

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsQF.isUniversal {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} :

φ.IsQF → φ.IsUniversal

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isUniversal {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :

φ.IsUniversal

source

inductive FirstOrder.Language.BoundedFormula.IsExistential {L : FirstOrder.Language} {α : Type u'} {n : ℕ} :

L.BoundedFormula α n → Prop

An existential formula is a formula defined by applying only existential quantifiers to a quantifier-free formula.

of_isQF: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsExistential
ex: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsExistential → φ.ex.IsExistential

Instances For

source

theorem FirstOrder.Language.BoundedFormula.IsQF.isExistential {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} :

φ.IsQF → φ.IsExistential

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.isExistential {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :

φ.IsExistential

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] {F : Type u_3} [FunLike F M N] {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [L.HomClass F M N] {f : F} (hInj : Function.Injective ⇑f) {v : α → M} {xs : Fin n → M} :

φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

source

theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] {F : Type u_3} [FunLike F M N] {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [EmbeddingLike F M N] [L.HomClass F M N] (f : F) {v : α → M} {xs : Fin n → M} :

φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

source

theorem FirstOrder.Language.BoundedFormula.IsQF.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] {F : Type u_3} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hQF : φ.IsQF) (f : F) {v : α → M} {xs : Fin n → M} :

φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

source

theorem FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] {F : Type u_3} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hU : φ.IsUniversal) (f : F) {v : α → M} {xs : Fin n → M} :

φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs

source

theorem FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] {F : Type u_3} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hE : φ.IsExistential) (f : F) {v : α → M} {xs : Fin n → M} :

φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

source

class FirstOrder.Language.Theory.IsUniversal {L : FirstOrder.Language} (T : L.Theory) :

Prop

A theory is universal when it is comprised only of universal sentences - these theories apply also to substructures.

isUniversal_of_mem : ∀ ⦃φ : L.Sentence⦄, φ ∈ T → FirstOrder.Language.BoundedFormula.IsUniversal φ

Instances

source

theorem FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem {L : FirstOrder.Language} {T : L.Theory} [self : T.IsUniversal] ⦃φ : L.Sentence⦄ :

φ ∈ T → FirstOrder.Language.BoundedFormula.IsUniversal φ

source

theorem FirstOrder.Language.Theory.IsUniversal.models_of_embedding {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} [hT : T.IsUniversal] {N : Type u_1} [L.Structure N] [N ⊨ T] (f : L.Embedding M N) :

M ⊨ T

source