Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.IsUniversal.brecOn

∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} {n : ℕ}
  {a : L.BoundedFormula α n} (t : a.IsUniversal),
  (∀ {n : ℕ} (a : L.BoundedFormula α n) (t : a.IsUniversal),
      FirstOrder.Language.BoundedFormula.IsUniversal.below t → motive a t) →
    motive a t

Defined in

Mathlib.ModelTheory.Complexity

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms