English
Let P be a property of bounded formulas with a fixed bound n. If φ is quantifier-free, then P φ holds provided: P holds for the bottom formula ⊥; P holds for every atomic formula ψ; P is closed under the supremum (join) operation, and under negation; and P is preserved under equivalence with respect to the empty theory (if φ1 ⇔[∅] φ2 then P φ1 ⇔ P φ2). Consequently, P φ holds for every φ with IsQF φ.
Русский
Пусть P — свойство, определённое для ограниченных формул фиксированной высоты n. Если φ — это формула без кванторов, то выполняется: P(⊥); P(ψ) для любой атомарной формулы ψ; P замкнутое относительно операции наибольшего (⊔); P замкнутое относительно отрицания; и P сохраняется при эквивалентности при пустой теории (если φ1 ⇔[∅] φ2, то P φ1 ⇔ P φ2). Тогда P φ верно для любой φ с IsQF φ.
LaTeX
$$$\forall L\, \forall \alpha\, \forall n\, \forall P:\ L.BoundedFormula\alpha\,n \to \Prop, \forall \varphi:\ L.BoundedFormula\alpha\,n, \varphi.IsQF \to P(\bot) \to (\forall \psi:\ L.BoundedFormula\alpha\,n, \psi.IsAtomic \to P\psi) \to (\forall {\phi_1 \phi_2}, P\phi_1 \to P\phi_2 \to P(\phi_1 \sqcup \phi_2)) \to (\forall {\phi}, P\phi \to P(\phi.not)) \to (\forall {\phi_1 \phi_2}, (\phi_1 \iff[∅] \phi_2) \to (P\phi_1 \leftrightarrow P\phi_2)) \to P\varphi$$
Lean4
theorem induction_on_sup_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : IsQF φ)
(hf : P (⊥ : L.BoundedFormula α n)) (ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
(hsup : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
(hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, (φ₁ ⇔[∅] φ₂) → (P φ₁ ↔ P φ₂)) : P φ :=
IsQF.recOn h hf @(ha) fun {φ₁ φ₂} _ _ h1 h2 => (hse (φ₁.imp_iff_not_sup φ₂)).2 (hsup (hnot h1) h2)
