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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 φ

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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

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}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

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}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_toPrenex {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : ∅.SemanticallyEquivalent φ φ.toPrenex

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}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

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}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

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

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

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

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

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

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

theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [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)

theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [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)

theorem FirstOrder.Language.BoundedFormula.IsQF.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [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

theorem FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [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

theorem FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [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)

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 φ

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

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_4} [L.Structure N] [N ⊨ T] (f : L.Embedding M N) : M ⊨ T

instance FirstOrder.Language.Substructure.models_of_isUniversal {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) (T : L.Theory) [T.IsUniversal] [M ⊨ T] : { x : M // x ∈ S } ⊨ T

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Theory.IsUniversal.insert {L : FirstOrder.Language} {T : L.Theory} [hT : T.IsUniversal] {φ : L.Sentence} (hφ : FirstOrder.Language.BoundedFormula.IsUniversal φ) : (insert φ T).IsUniversal

theorem FirstOrder.Language.Relations.isAtomic {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (r.boundedFormula ts).IsAtomic

theorem FirstOrder.Language.Relations.isQF {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (r.boundedFormula ts).IsQF

theorem FirstOrder.Language.Relations.isUniversal_reflexive {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.reflexive

theorem FirstOrder.Language.Relations.isUniversal_irreflexive {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.irreflexive

theorem FirstOrder.Language.Relations.isUniversal_symmetric {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.symmetric

theorem FirstOrder.Language.Relations.isUniversal_antisymmetric {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.antisymmetric

theorem FirstOrder.Language.Relations.isUniversal_transitive {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.transitive

theorem FirstOrder.Language.Relations.isUniversal_total {L : FirstOrder.Language} (r : L.Relations 2) : FirstOrder.Language.BoundedFormula.IsUniversal r.total

theorem FirstOrder.Language.Formula.isAtomic_graph {L : FirstOrder.Language} {n : ℕ} (f : L.Functions n) : FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Formula.graph f)