Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not

∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n},
  φ.IsQF →
    P ⊥ →
      (∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) →
        (∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) →
          (∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) →
            (∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ

Defined in

Mathlib.ModelTheory.Complexity

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound