English
Let P be a property of bounded formulas with bound n. If φ is quantifier-free, then P φ holds provided: P(⊥); P on atomic ψ; P is closed under infimum (⊓); and negation; and P respects equivalence under the empty theory (φ1 ⇔[∅] φ2 implies P φ1 ⇔ P φ2). Consequently, P φ holds for all QF φ.
Русский
Пусть P — свойство на ограниченных формулах с ограничителем n. Если φ — формула без кванторов, то выполнено P φ при условии: P(⊥); P на атомарной ψ; P замкнуто относительно инфима (⊓); и отрицания; и P сохраняет эквивалентность при пустой теории (φ1 ⇔[∅] φ2 тогда P φ1 ⇔ P φ2). Тогда P φ верно для всех QF φ.
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 {\varphi_1 \varphi_2}, P\varphi_1 \to P\varphi_2 \to P(\varphi_1 \sqcap \varphi_2)) \to (\forall {\varphi}, P\varphi \to P(\varphi.not)) \to (\forall {\varphi_1 \varphi_2}, (\varphi_1 \iff[∅] \varphi_2) \to (P\varphi_1 \leftrightarrow P\varphi_2)) \to P\varphi$$
Lean4
theorem induction_on_inf_not {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : IsQF φ)
(hf : P (⊥ : L.BoundedFormula α n)) (ha : ∀ ψ : L.BoundedFormula α n, IsAtomic ψ → P ψ)
(hinf : ∀ {φ₁ φ₂}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) (hnot : ∀ {φ}, P φ → P φ.not)
(hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, (φ₁ ⇔[∅] φ₂) → (P φ₁ ↔ P φ₂)) : P φ :=
h.induction_on_sup_not hf ha
(fun {φ₁ φ₂} h1 h2 => (hse (φ₁.sup_iff_not_inf_not φ₂)).2 (hnot (hinf (hnot h1) (hnot h2)))) (fun {_} => hnot)
fun {_ _} => hse
