English
Let P be a property on bounded formulas with a fixed arity. If φ satisfies a base quantifier-free case, if P is closed under negation and under the existential operator, and if P respects equivalence under the empty theory, then P φ holds for any φ.
Русский
Пусть P — свойство на ограниченные формулы с фиксированной аритметикой; если φ удовлетворяет базовому кванторовому случаю безкванторности, если P замкнуто относительно отрицания и оператора существования, и P сохраняет эквивалентность при пустой теории, то P φ верно для любой φ.
LaTeX
$$$\forall L\, \forall \alpha\, \forall n\, \forall P:\, (P)\, \,:\ L.BoundedFormula\alpha\,n \to \Prop, \forall \varphi:\ L.BoundedFormula\alpha\,n, \varphi.IsPrenex → (P\varphi.not) \,\to \, (P\varphi.ex) \,\to \, P\varphi$$
Lean4
theorem induction_on_exists_not {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ) (hnot : ∀ {m} {φ : L.BoundedFormula α m}, P φ → P φ.not)
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m}, (φ₁ ⇔[∅] φ₂) → (P φ₁ ↔ P φ₂)) : P φ :=
φ.induction_on_all_ex (fun {_ _} => hqf) (fun {_ φ} hφ => (hse φ.all_iff_not_ex_not).2 (hnot (hex (hnot hφ))))
(fun {_ _} => hex) fun {_ _ _} => hse
