Expressing "at most" in predicate logic I need to translate to predicate logic: "Every natural number is the sum of at most four squared natural numbers". The word that causes problems for me is the word "at most".
Here is what I have right: $ ∀ n {\in}\mathbb N \; ∃ a,b,c,d {\in} \mathbb N\quad a^2 +b^2+c^2+d^2 = n^2$. How do I integrate the restriction "at most four numbers"?
 A: Let's say "at most four" means "one or two or three or four".  Then you can translate the statement as
\begin{align*}
\forall n\in \mathbb{N},(&(\exists a\in\mathbb{N}, n = a^2) \\
& \vee(\exists a,b\in\mathbb{N}, n = a^2+b^2) \\
& \vee(\exists a,b,c\in\mathbb{N}, n = a^2+b^2+c^2) \\
& \vee(\exists a,b,c,d\in\mathbb{N}, n = a^2+b^2+c^2+d^2))
\end{align*}
First-order predicate logic doesn't have a way to quantify over the number of quantifiers, so, without pulling tricks (like using the fact that $0^2$ is an additive unit) you need to translate each possibility independently and form their disjunction.
A: 
"Every natural number is the sum of at most four squared natural numbers".


*

*Disambiguate:
“Every natural number is expressible as a sum of squared natural numbers, requiring at most four.”


*Rephrase equivalently for easier translation:
“Every natural number is expressible as the sum of exactly four squared integers.”


*Translate:
$$\forall n{\in}\mathbb N\:\: \exists a,b,c,d{\in}\mathbb Z\quad
   n=a^2+b^2+c^2+d^2.$$
(This is actually Lagrange's Four-Square Theorem.)
