isExistential

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.IsQF.isExistential

English

If φ is quantifier-free, then φ is existential.

Русский

Если φ безкванторная, то φ существует.

LaTeX

$$$\forall \varphi:\ L.BoundedFormula\alpha\,n, \varphi.IsQF \to \varphi.IsExistential$$

Lean4

theorem isExistential {φ : L.BoundedFormula α n} : IsQF φ → IsExistential φ :=
  IsExistential.of_isQF

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru