English
Let P be a property on all bounded formulas with varying arity. If for every m, all bounded formulas at level m+1 that are quantifier-free satisfy P, and if formulas built with all (∀) and with (∃) propagate P to their subformulas, and P is preserved under equivalence with the empty theory, then P holds for all bounded formulas.
Русский
Пусть P — свойство на формулах с ограничением arity, где для каждого m все формулы уровня m+1 без кванторов удовлетворяют P; а также если операции all и ex сохраняют P в подпοформула, и P сохраняется под эквивалентностью относительно пустой теории, тогда P выполняется для всех ограниченных формул.
LaTeX
$$$\forall L\, \forall \alpha\, \forall n\, \forall P:\ {m:\mathbb{N}} \to L.BoundedFormula\alpha\,m \to \Prop, \forall \varphi:\ L.BoundedFormula\alpha\,n, \varphi.IsPrenex → P(\varphi)\Rightarrow P(\varphi)$$$
Lean4
theorem induction_on_all_ex {P : ∀ {m}, L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n)
(hqf : ∀ {m} {ψ : L.BoundedFormula α m}, IsQF ψ → P ψ)
(hall : ∀ {m} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all)
(hex : ∀ {m} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex)
(hse : ∀ {m} {φ₁ φ₂ : L.BoundedFormula α m}, (φ₁ ⇔[∅] φ₂) → (P φ₁ ↔ P φ₂)) : P φ :=
by
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ from (hse φ.iff_toPrenex).2 (h' φ.toPrenex_isPrenex)
intro m φ hφ
induction hφ with
| of_isQF hφ => exact hqf hφ
| all _ hφ => exact hall hφ
| ex _ hφ => exact hex hφ
