Lagmental Vicfred

Łoś's Theorem Evaluates Formulas Coordinatewise in an Ultraproduct by Vicfred

tags: mathematics, mathematical logic, model theory, compactness

A first-order formula holds in an ultraproduct exactly when it holds on an ultrafilter-large set of coordinates. The point is to make the formal expression readable enough to audit line by line.

Set-up

A first-order language \(\mathcal L\) supplies symbols, formulas, and structures. Semantic consequence \(T\models\varphi\) is truth in every model, while provability \(T\vdash\varphi\) is a finite formal derivation.

$$ \prod_{i\in I}\mathcal M_i/\mathcal U $$

I read the first line as input and the second as output. The symbols \(\forall\) and \(\exists\) are not interchangeable, and neither may be upgraded silently to \(\Longleftrightarrow\).

$$ \prod_i\mathcal M_i/\mathcal U\models\varphi([\bar a_i])\Longleftrightarrow\{i:\mathcal M_i\models\varphi(\bar a_i)\}\in\mathcal U $$

The calculation

The following line is the smallest calculation that still exercises the mechanism. It keeps nested delimiters and the order of operations explicit.

$$ (a_i)\sim_{\mathcal U}(b_i)\Longleftrightarrow\{i\in I:a_i=b_i\}\in\mathcal U $$

What survives abstraction

A good test for understanding is to change the presentation while keeping the invariant fixed. The aligned form makes that comparison unusually easy.

$$ \begin{aligned} \mathsf{D}\;&:\quad \prod_{i\in I}\mathcal M_i/\mathcal U,\\[5pt] \mathsf{C}\;&:\quad \prod_i\mathcal M_i/\mathcal U\models\varphi([\bar a_i])\Longleftrightarrow\{i:\mathcal M_i\models\varphi(\bar a_i)\}\in\mathcal U. \end{aligned} $$

The boundary

First-order compactness does not apply to arbitrary second-order properties. Finiteness and categorical characterization of the natural numbers lie beyond its direct reach.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] \prod_i\mathcal M_i/\mathcal U\models\varphi([\bar a_i])\Longleftrightarrow\{i:\mathcal M_i\models\varphi(\bar a_i)\}\in\mathcal U \end{gathered}} $$

This is enough machinery for one note: an exact object, a worked case, a structural law, and a clearly marked boundary. Each layer can now be tested independently.

This article was posted on Mon 29 August 2011. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.