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?
 A: Yes, but there is a broader class of formulas with the same property, which is the class that is usually considered. The class $\Sigma^0_1$ consists of formulas that use the same relations and operations in the question, any of the usual logical operations (including NOT and IMPLIES), and which can be put into the form
$$
(\exists x_1)\cdots(\exists x_n)\,\phi(x_1\ldots,x_n)
$$
where $\phi$ has no unbounded quantifiers ($\phi$ may have bounded universal quantifiers and may have bounded existential quantifiers). 
Like the class of formulas in the question, these formulas can be proved by giving finitely many examples (values for $x_1,\ldots,x_n$) and then verifying that a formula with only bounded quantifiers is true, which can be done algorithmically. 
The class $\Sigma^0_1$ is well known and significant in mathematical logic for several reasons:


*

*A set of natural numbers is recursively enumerable if and only if it is definable by a $\Sigma^0_1$ formula. This relationship leads to applications of $\Sigma^0_1$ formulas in computability theory. 

*The proposition that a fixed effective formal theory is inconsistent can be written as a $\Sigma^0_1$ statement. This leads to applications of $\Sigma^0_1$ formulas in the proof theory of arithmetic, such as Gödel's incompleteness theorem. 

*A negation of a $\Sigma^0_1$ formula is called a $\Pi^0_1$ formula; $\Pi^0_1$ formulas can be disproved by giving finitely many examples and checking those examples. The classes $\Sigma^0_1$ and $\Pi^0_1$ sit close to the bottom of an infinite hierarchy of formulas known as the arithmetical hierarchy, and many properties of classes higher in the hierarchy follow from corresponding properties of the classes $\Sigma^0_1$ and $\Pi^0_1$. 
A: 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.
