English
Let L be a language and α a type. The operation sigmaAll takes a bounded formula with bound n+1 and returns the corresponding bounded formula with bound n by universally quantifying over the extra variable; otherwise it is undefined. In particular, sigmaAll(⟨n+1, φ⟩) = ⟨n, φ.all⟩.
Русский
Пусть L — язык, α — множество. Операция sigmaAll переводит ограничённую формулу с числом ограничений n+1 в формулу с ограничением n, получая эквивалентную формулу путем всеобщего квантора по добавленной переменной; иначе функция не определена. В частности, sigmaAll(⟨n+1, φ⟩) = ⟨n, φ.all⟩.
LaTeX
$$$\\sigmaAll: (\\Sigma n, L\\,\\mathrm{BoundedFormula}\\,\\alpha\\, n) \\to (\\Sigma n, L\\,\\mathrm{BoundedFormula}\\,\\alpha\\, n)$, \\\\sigmaAll(\\langle n+1, \\varphi \\rangle) = \\langle n, \\varphi_{all} \\rangle , \\quad \\sigmaAll(\\langle n, \\varphi \\rangle) = \\text{default}.$$$
Lean4
/-- Applies the `forall` quantifier to an element of `(Σ n, L.BoundedFormula α n)`,
or returns `default` if not possible. -/
def sigmaAll : (Σ n, L.BoundedFormula α n) → Σ n, L.BoundedFormula α n
| ⟨n + 1, φ⟩ => ⟨n, φ.all⟩
| _ => default
