Proof of the Löwenheim-Skolem theorem

Question

For each first-order $\sigma \,$-formula $\varphi(y,x_1, \ldots, x_n) \,,$ the axiom of choice implies the existence of a function $f_\varphi: M^n\to M$ such that, for all $a_1, \ldots, a_n \in M$, either $M\models\varphi(f_\varphi (a_1, \dots, a_n), a_1, \dots, a_n)$ or $M\models\neg\exists y \, \varphi(y, a_1, \dots, a_n) \,.$

This is a quote from the Wikipedia page on the Löwenheim–Skolem theorem.

What I am confused about is the last part of the quote — starting from $$M\models\varphi(f_\varphi (a_1, \dots, a_n), a_1, \dots, a_n)\,.$$ Specifically, $$M\models\neg\exists y \, \varphi(y, a_1, \dots, a_n) \,.$$ What does it mean? There does not exist $y$ that satisfies the predicate and what? How does it relate to a model - what is a model satisfying?

Thanks.

Answer 1

The claim says that given a formula $\varphi(y,x_1,\ldots,x_n)$ then for every $n$ parameters $a_1,\ldots,a_n$ exactly one of the following happens:

1. There exists some $y\in M$ such that $M\models\varphi(y,a_1,\ldots,a_n)$.
2. For all $y\in M$ the above is false, therefore $M\models\lnot\exists y\varphi(y,a_1,\ldots,a_n)$. This is because in classical logic the model thinks that there is no $y$ such that $\varphi(y,a_1,\ldots,a_n)$ is true if and only if it things that $\lnot\exists y\varphi(y,a_1,\ldots,a_n)$ is true.

Using the axiom of choice we can define a function $f_\varphi$ that for every $n$-tuple, $(a_1,\ldots,a_n)$ for which the first thing holds, $f(a_1,\ldots,a_n)$ returns such $y$.