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 : Language} {α : Type u'} {n : ℕ} :

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

source

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

¬φ.all.IsAtomic

source

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

¬φ.ex.IsAtomic

source

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

(BoundedFormula.relabel f φ).IsAtomic

source

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

(BoundedFormula.liftAt k m φ).IsAtomic

source

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

(BoundedFormula.castLE h φ).IsAtomic

source

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

source

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

φ.IsAtomic → φ.IsQF

source

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

⊥.IsQF

source

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

φ.not.IsQF

source

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

⊤.IsQF

source

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

(φ ⊔ ψ).IsQF

source

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

(φ ⊓ ψ).IsQF

source

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

(relabel f φ).IsQF

source

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

(liftAt k m φ).IsQF

source

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

(castLE h φ).IsQF

source

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

¬φ.all.IsQF

source

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

¬φ.ex.IsQF

source

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

source

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

φ.IsQF → φ.IsPrenex

source

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

φ.IsPrenex

source

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 φ

source

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

(BoundedFormula.relabel f φ).IsPrenex

source

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

(BoundedFormula.castLE h φ).IsPrenex

source

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

(BoundedFormula.liftAt k m φ).IsPrenex

source

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

Instances For

source

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

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

source

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

(φ.toPrenexImpRight ψ).IsPrenex

source

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

Instances For

source

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

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

source

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

(φ.toPrenexImp ψ).IsPrenex

source

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

Instances For

source

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

φ.toPrenex.IsPrenex

source

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight {L : 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

source

theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp {L : 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

source

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_toPrenex {L : 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 : 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 : 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 : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) :

∅.Iff φ φ.toPrenex

source

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 φ

source

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 φ

source

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

source

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

φ.IsQF → φ.IsUniversal

source

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

φ.IsUniversal

source

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

source

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

φ.IsQF → φ.IsExistential

source

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

φ.IsExistential

source

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} :

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

source

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} :

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

source

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} :

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

source

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} :

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

source

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} :

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

source

class FirstOrder.Language.Theory.IsUniversal {L : 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 → BoundedFormula.IsUniversal φ

Instances

source

theorem FirstOrder.Language.Theory.IsUniversal.models_of_embedding {L : 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

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] :

↥S ⊨ T

source

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

(Insert.insert φ T).IsUniversal

source

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

(r.boundedFormula ts).IsAtomic

source

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

(r.boundedFormula ts).IsQF

source

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

BoundedFormula.IsUniversal r.reflexive

source

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

BoundedFormula.IsUniversal r.irreflexive

source

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

BoundedFormula.IsUniversal r.symmetric

source

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

BoundedFormula.IsUniversal r.antisymmetric

source

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

BoundedFormula.IsUniversal r.transitive

source

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

BoundedFormula.IsUniversal r.total

source

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

BoundedFormula.IsAtomic (graph f)

Documentation

Mathlib.ModelTheory.Complexity

Quantifier Complexity #

Main Definitions #

Main Results #