Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.IsUniversal.casesOn

∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} {n : ℕ}
  {a : L.BoundedFormula α n} (t : a.IsUniversal),
  (∀ {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF), motive φ ⋯) →
    (∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsUniversal), motive φ.all ⋯) → motive a t

Defined in

Mathlib.ModelTheory.Complexity

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms