Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.induction_on_all_ex

∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop}
  (φ : L.BoundedFormula α n),
  (∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) →
    (∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) →
      (∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) →
        (∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ

Defined in

Mathlib.ModelTheory.Complexity

Cited by

1 results in Mathlib

Foundations

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