Expressing "at most" in predicate logic

Question

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"?

Answer 1

"Every natural number is the sum of at most four squared natural numbers".

1. Disambiguate:

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

2. Rephrase equivalently for easier translation:

   “Every natural number is expressible as the sum of exactly four squared integers.”

3. 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.)

Answer 2

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.