Do arithmetical statements of this form have any mathematical significance? Begin with four binary relations


*

*$=, \neq,\leq,\geq$


and two binary operations


*

*$+,\times$


Now consider the sentences over this signature that only involve the following:


*

*Logical AND

*Logical OR

*"There exists $n$ such that..."

*"For all $n \leq m$ it holds that..."


Intuitively speaking, such sentences are very special, because if they're true, then we can prove them simply by giving example(s) and/or checking finitely many cases.
Do such sentences have any mathematical significance?

These are known as $\Sigma_1$ sentences (in fact the definition of $\Sigma_1$ is a bit different, but it works out the same). They have the nice property that whenever $\phi$ is a true $\Sigma_1$ sentence, it is also provable in Peano arithemetic. Also, for basically the reason that you said, if $(\exists n)\phi(n)$ is a true $\Sigma_1$ sentence, then it is possible to compute a witness $n$ such that $\phi(n)$ is true.
As far as I know, there aren't many examples of "natural" mathematical theorems that are $\Sigma_1$. However, $\Pi_1$ sentences, which are the negations of $\Sigma_1$ sentences do turn up sometimes. For example, Goldbach's conjecture is a $\Pi_1$ sentence.
