isPrenex_toPrenexImpRight — Mathlib

English

Realizability is preserved across the prenex-right transformation when φ is QF and ψ is prenex.

Русский

Для φ квантитно-фри и ψ в пренексной форме сохраняется реализация между φ.toPrenexImpRight ψ и φ.imp ψ.

LaTeX

$$$(\varphi.toPrenexImpRight \psi).Realize v xs \leftrightarrow (\varphi.imp \psi).Realize v xs$$$

Lean4

theorem isPrenex_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ) :
    IsPrenex (φ.toPrenexImpRight ψ) := by
  induction hψ with
  | of_isQF hψ => rw [hψ.toPrenexImpRight]; exact (hφ.imp hψ).isPrenex
  | all _ ih1 => exact (ih1 hφ.liftAt).all
  | ex _ ih2 => exact (ih2 hφ.liftAt).ex

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