English
Realizability is preserved under the toPrenexImpRight with a one-step lift.
Русский
Реализация сохраняется при переходе к toPrenexImpRight с одноступенным поднятием.
LaTeX
$$$(\theta.all.Realize v xs) = (\forall a:\, M, \theta.Realize v (\text{snoc } xs a))$$$
Lean4
theorem realize_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ) {v : α → M}
{xs : Fin n → M} : (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs := by
induction hψ with
| of_isQF hψ => rw [hψ.toPrenexImpRight]
| all _ ih =>
refine _root_.trans (forall_congr' fun _ => ih hφ.liftAt) ?_
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
| ex _ ih =>
unfold toPrenexImpRight
rw [realize_ex]
refine _root_.trans (exists_congr fun _ => ih hφ.liftAt) ?_
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_ex]
refine ⟨?_, fun h' => ?_⟩
· rintro ⟨a, ha⟩ h
exact ⟨a, ha h⟩
· by_cases h : φ.Realize v xs
· obtain ⟨a, ha⟩ := h' h
exact ⟨a, fun _ => ha⟩
· inhabit M
exact ⟨default, fun h'' => (h h'').elim⟩
