Mathlib Map

Theorems · Inductive type · logic and foundations

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.

Defined in
Mathlib.ModelTheory.Complexity
Cited by
36 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FirstOrder.Language.BoundedFormula.IsAtomic.isQF · cited by 9IsAtomic.isQFFirstOrder.Language.BoundedFormula.IsQF.isUniversal · cited by 7IsQF.isUniversalFirstOrder.Language.BoundedFormula.IsQF.isPrenex · cited by 6IsQF.isPrenexFirstOrder.Language.BoundedFormula.isQF_bot · cited by 6BoundedFormula.isQF_botFirstOrder.Language.Relations.isQF · cited by 5Relations.isQFFirstOrder.Language.BoundedFormula.IsPrenex.recOn · cited by 4IsPrenex.recOnFirstOrder.Language.BoundedFormula.IsQF.not · cited by 4IsQF.notFirstOrder.Language.BoundedFormula.IsQF.recOn · cited by 4IsQF.recOnFirstOrder.Language.BoundedFormula.IsQF.liftAt · cited by 3IsQF.liftAtFirstOrder.Language.BoundedFormula.IsPrenex.liftAt · cited by 2IsPrenex.liftAtFirstOrder.Language.BoundedFormula.IsQF.casesOn · cited by 2IsQF.casesOnFirstOrder.Language.BoundedFormula.IsQF.realize_embedding · cited by 2IsQF.realize_embeddingFirstOrder.Language.BoundedFormula.IsQF.toPrenexImp · cited by 2IsQF.toPrenexImpFirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight · cited by 2IsQF.toPrenexImpRightFirstOrder.Language.BoundedFormula.realize_toPrenexImp · cited by 1BoundedFormula.realize_to…FirstOrder.Language · cited by 1084FirstOrder.LanguageFirstOrder.Language.BoundedFormula · cited by 207Language.BoundedFormulaBoundedFormula.IsQFCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by49

Results whose statement or proof uses this declaration.