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 : 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 : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (t₁.bdEqual t₂).IsAtomic
- rel {L : 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 : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α (n + 1))
:
theorem
FirstOrder.Language.BoundedFormula.not_ex_isAtomic
{L : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α (n + 1))
:
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.relabel
{L : Language}
{α : Type u'}
{β : Type v'}
{n m : ℕ}
{φ : L.BoundedFormula α m}
(h : φ.IsAtomic)
(f : α → β ⊕ Fin n)
:
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.liftAt
{L : Language}
{α : Type u'}
{l : ℕ}
{φ : L.BoundedFormula α l}
{k m : ℕ}
(h : φ.IsAtomic)
:
(BoundedFormula.liftAt k m φ).IsAtomic
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.castLE
{L : Language}
{α : Type u'}
{n l : ℕ}
{φ : L.BoundedFormula α l}
{h : l ≤ n}
(hφ : φ.IsAtomic)
:
inductive
FirstOrder.Language.BoundedFormula.IsQF
{L : 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 : Language} {α : Type u'} {n : ℕ} : BoundedFormula.falsum.IsQF
- of_isAtomic {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) : φ.IsQF
- imp {L : Language} {α : Type u'} {n : ℕ} {φ₁ φ₂ : L.BoundedFormula α n} (h₁ : φ₁.IsQF) (h₂ : φ₂.IsQF) : (φ₁.imp φ₂).IsQF
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.isQF
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.not
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
(h : φ.IsQF)
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.sup
{L : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
(hφ : φ.IsQF)
(hψ : ψ.IsQF)
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.inf
{L : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
(hφ : φ.IsQF)
(hψ : ψ.IsQF)
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.liftAt
{L : Language}
{α : Type u'}
{l : ℕ}
{φ : L.BoundedFormula α l}
{k m : ℕ}
(h : φ.IsQF)
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.castLE
{L : Language}
{α : Type u'}
{n l : ℕ}
{φ : L.BoundedFormula α l}
{h : l ≤ n}
(hφ : φ.IsQF)
:
theorem
FirstOrder.Language.BoundedFormula.not_all_isQF
{L : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α (n + 1))
:
theorem
FirstOrder.Language.BoundedFormula.not_ex_isQF
{L : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α (n + 1))
:
inductive
FirstOrder.Language.BoundedFormula.IsPrenex
{L : 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 : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) : φ.IsPrenex
- all {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex) : φ.all.IsPrenex
- ex {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex) : φ.ex.IsPrenex
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsQF.isPrenex
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
:
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
(h : φ.IsAtomic)
:
φ.IsPrenex
theorem
FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not
{L : 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 : Language}
{α : Type u'}
{β : Type v'}
{n m : ℕ}
{φ : L.BoundedFormula α m}
(h : φ.IsPrenex)
(f : α → β ⊕ Fin n)
:
theorem
FirstOrder.Language.BoundedFormula.IsPrenex.castLE
{L : Language}
{α : Type u'}
{l : ℕ}
{φ : L.BoundedFormula α l}
(hφ : φ.IsPrenex)
{n : ℕ}
{h : l ≤ n}
:
theorem
FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
{L : Language}
{α : Type u'}
{l : ℕ}
{φ : L.BoundedFormula α l}
{k m : ℕ}
(h : φ.IsPrenex)
:
(BoundedFormula.liftAt k m φ).IsPrenex
def
FirstOrder.Language.BoundedFormula.toPrenexImpRight
{L : 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 : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
:
ψ.IsQF → φ.toPrenexImpRight ψ = φ.imp ψ
theorem
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight
{L : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
(hφ : φ.IsQF)
(hψ : ψ.IsPrenex)
:
(φ.toPrenexImpRight ψ).IsPrenex
def
FirstOrder.Language.BoundedFormula.toPrenexImp
{L : 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 : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
:
φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
theorem
FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp
{L : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormula α n}
(hφ : φ.IsPrenex)
(hψ : ψ.IsPrenex)
:
(φ.toPrenexImp ψ).IsPrenex
def
FirstOrder.Language.BoundedFormula.toPrenex
{L : 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 : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α n)
:
theorem
FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not
{L : 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 : 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 : Language}
{α : Type u'}
{n : ℕ}
(φ : L.BoundedFormula α n)
:
theorem
FirstOrder.Language.BoundedFormula.induction_on_all_ex
{L : 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 : 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 : 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 : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) : φ.IsUniversal
- all {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsUniversal) : φ.all.IsUniversal
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsQF.isUniversal
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
:
φ.IsQF → φ.IsUniversal
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.isUniversal
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
(h : φ.IsAtomic)
:
inductive
FirstOrder.Language.BoundedFormula.IsExistential
{L : 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 : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) : φ.IsExistential
- ex {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsExistential) : φ.ex.IsExistential
Instances For
theorem
FirstOrder.Language.BoundedFormula.IsQF.isExistential
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
:
φ.IsQF → φ.IsExistential
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.isExistential
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormula α n}
(h : φ.IsAtomic)
:
theorem
FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective
{L : 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 : 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 : 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 : 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 : 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 → BoundedFormula.IsUniversal φ
Instances
instance
FirstOrder.Language.Substructure.models_of_isUniversal
{L : Language}
{M : Type w}
[L.Structure M]
(S : L.Substructure M)
(T : L.Theory)
[T.IsUniversal]
[M ⊨ T]
:
theorem
FirstOrder.Language.Theory.IsUniversal.insert
{L : Language}
{T : L.Theory}
[hT : T.IsUniversal]
{φ : L.Sentence}
(hφ : BoundedFormula.IsUniversal φ)
:
(Insert.insert φ T).IsUniversal
theorem
FirstOrder.Language.Relations.isUniversal_antisymmetric
{L : Language}
(r : L.Relations 2)
: