Is this a good expression of the claim using logical notation?

Question

Four Square Theorem: Every positive integer can be written as a sum of four integer squares. Expressed in logical notation : $$\forall n>0 =a_{0}^{2} + a_{1}^{2} + a_{2}^{2} + a_{3}^{2}$$

Answer 1

In natural language: for all integers $n$, if $n > 0$, then there are integers $a_0, a_1, a_2, a_3$ such that $n = a_0^2 + a_1^2 + a_2^2 + a_3^2$. Symbolically: $$\forall n \in {\mathbb Z}: n > 0 \to \exists a_0, a_1, a_2, a_3 \in {\mathbb Z}: n = a_0^2 + a_1^2 + a_2^2 + a_3^2.$$ If the context makes it clear that your talking about integers, you could also say $$\forall n: n > 0 \to \exists a_0, a_1, a_2, a_3: n = a_0^2 + a_1^2 + a_2^2 + a_3^2.$$ While I'm at this, since $0$ can be written as $0^2 + 0^2 + 0^2 + 0^2$ and since negative numbers are definitely not the sum of four squares, I'd quantify over the natural numbers and leave out the $n > 0$ condition. That makes it a different, but equivalent statement. $$\forall n \in {\mathbb N} \exists a_0, a_1, a_2, a_3 \in {\mathbb N}: n = a_0^2 + a_1^2 + a_2^2 + a_3^2.$$

Answer 2

I'd write it as $$\forall n >0, \quad n = a_0^2+a_1^2+a_2^2+a_3^2$$