Theorems · Definition · logic and foundations

FirstOrder.Language.Formula.iAlls

{L : FirstOrder.Language} → {α : Type u'} → (β : Type v') → [Finite β] → L.Formula (α ⊕ β) → L.Formula α

iAlls f φ transforms a L.Formula (α ⊕ β) into a L.Formula α by universally quantifying over all variables Sum.inr _.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

6 results in Mathlib

Foundations

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

Assumes

Finite