toPrenexImp — Mathlib

English

Equality of realizations holds under the toPrenexImpRight construction when φ is QF and ψ is prenex.

Русский

Сохранение реализации при конструировании toPrenexImpRight держится в случае φ QF и ψ prenex.

LaTeX

$$$\forall v xs\; ( (φ.toPrenexImpRight ψ).Realize v xs) = (φ.imp ψ).Realize v xs$$$

Lean4

/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
  If `φ` and `ψ` are in prenex normal form, then `φ.toPrenexImp ψ`
  is a prenex normal form for `φ.imp ψ`. -/
def toPrenexImp : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
  | n, BoundedFormula.ex φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).all
  | n, all φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).ex
  | _, φ, ψ => φ.toPrenexImpRight ψ

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