English
Restricting the free variables of a bounded formula preserves realization up to a corresponding change of the evaluation function.
Русский
Ограничение свободных переменных в ограниченной формуле сохраняет реализацию при соответствующем изменении функции оценки.
LaTeX
$$$ (\phi.restrictFreeVar f).Realize v xs \iff \phi.Realize v' xs $$$
Lean4
theorem realize_restrictFreeVar [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n} {f : φ.freeVarFinset → β} {v : β → M}
{xs : Fin n → M} (v' : α → M) (hv' : ∀ a, v (f a) = v' a) : (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs :=
by
induction φ with
| falsum => rfl
| equal =>
simp only [Realize, restrictFreeVar, freeVarFinset.eq_2]
rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
simp
| rel =>
simp only [Realize, freeVarFinset.eq_3, Finset.biUnion_val, restrictFreeVar]
congr!
rw [realize_restrictVarLeft v' (by simp [hv'])]
simp
| imp _ _ ih1 ih2 =>
simp only [Realize, restrictFreeVar, freeVarFinset.eq_4]
rw [ih1, ih2] <;> simp [hv']
| all _ ih3 =>
simp only [restrictFreeVar, Realize]
refine forall_congr' (fun _ => ?_)
rw [ih3]; simp [hv']
