Theorems · Definition · logic and foundations
FirstOrder.Language.BoundedFormula.Realize
{L : FirstOrder.Language} →
{M : Type w} → [L.Structure M] → {α : Type u'} → {l : ℕ} → L.BoundedFormula α l → (α → M) → (Fin l → M) → PropA bounded formula can be evaluated as true or false by giving values to each free and bound variable.
- Defined in
- Mathlib.ModelTheory.Semantics
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 20 from the axioms, rests on 140 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.BoundedFormulastatement and proof · cited by 207
- FirstOrder.Language.BoundedFormula.brecOnproof · cited by 1
Cited by108
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Formula.Realizeproof · cited by 81
- FirstOrder.Language.Theory.ModelsBoundedFormulaproof · cited by 30
- FirstOrder.Language.BoundedFormula.realize_iffstatement and proof · cited by 7
- FirstOrder.Language.BoundedFormula.realize_rel₂statement and proof · cited by 6
- FirstOrder.Language.ElementaryEmbedding.map_formulaproof · cited by 5
- FirstOrder.Language.Theory.Iff.realize_bd_iffstatement · cited by 5
- FirstOrder.Language.Formula.realize_equivSentence_symm_conproof · cited by 4
- FirstOrder.Language.BoundedFormula.realize_mapTermRel_idstatement and proof · cited by 4
- FirstOrder.Language.BoundedFormula.realize_restrictFreeVarstatement and proof · cited by 4
- FirstOrder.Language.BoundedFormula.realize_allstatement · cited by 3
- FirstOrder.Language.BoundedFormula.realize_impstatement and proof · cited by 3
- FirstOrder.Language.BoundedFormula.realize_relstatement · cited by 3