Quantifier Complexity #
This file defines quantifier complexity of first-order formulas, and constructs prenex normal forms.
Main Definitions #
FirstOrder.Language.BoundedFormula.IsAtomicdefines atomic formulas - those which are constructed only from terms and relations.FirstOrder.Language.BoundedFormula.IsQFdefines quantifier-free formulas - those which are constructed only from atomic formulas and boolean operations.FirstOrder.Language.BoundedFormula.IsPrenexdefines 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.toPrenexconstructs a prenex normal form of a given formula.
Main Results #
FirstOrder.Language.BoundedFormula.realize_toPrenexshows 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
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
Instances For
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}
(hφ : φ.IsQF)
(hψ : ψ.IsQF)
:
(φ ⊔ ψ).IsQF
theorem
FirstOrder.Language.BoundedFormula.IsQF.inf
{L : FirstOrder.Language}
{α : Type u'}
{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
Instances For
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
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight
{L : FirstOrder.Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
:
ψ.IsQF → φ.toPrenexImpRight ψ = φ.imp ψ
theorem
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight
{L : FirstOrder.Language}
{α : Type u'}
{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
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp
{L : FirstOrder.Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
:
φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
theorem
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp
{L : FirstOrder.Language}
{α : Type u'}
{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
Instances For
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}
(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}
(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}, ∅.Iff φ₁ φ₂ → (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}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂))
:
P φ
theorem
FirstOrder.Language.BoundedFormula.iff_toPrenex
{L : FirstOrder.Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α n)
:
∅.Iff φ φ.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}, ∅.Iff φ₁ φ₂ → (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}, ∅.Iff φ₁ φ₂ → (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
Instances For
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
Instances For
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_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}
:
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}
:
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}
:
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}
:
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}
:
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
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
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]
:
↥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)
:
theorem
FirstOrder.Language.Formula.isAtomic_graph
{L : FirstOrder.Language}
{n : ℕ}
(f : L.Functions n)
: