Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.IsUniversal.below.casesOn

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

Defined in

Mathlib.ModelTheory.Complexity

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms