Is there any natural* statement S about the natural integers such that if PA contains no contradictions then neither PA+S nor PA+not S contains a contradiction?
If unknown, where can I read about the philosophical views on it?
*By natural I mean not a logical trick or non-constructive existence proof such as Rosser's sentence, but a clear statement such as the Collatz conjecture.
As noted in the comments, the Paris–Harrington Theorem is a natural example of a true statement that is not provable in Peano Arithmetic. In fact, the Paris–Harrington Theorem is equivalent over PA to $\Sigma_1$-Reflection:
If $\phi$ is a $\Sigma_1$ sentence and $\mathrm{PA} \vdash \phi$, then $\phi$ is true.
(To be completely accurate, this statement must be internalized. The first two occurrences of $\phi$ are actually Gödel codes, $\vdash$ refers to the internal notion of provability, and the third occurrence of $\phi$ needs to be decoded using the appropriate universal $\Sigma_1$-formula. The end result is an actual sentence in the language of arithmetic.)
Now PA + $\Sigma_1$-reflection easily proves Con(PA) (use $0 = 1$ for $\phi$) and so, by Gödel's Second Incompleteness Theorem, the Paris–Harrington Theorem cannot be proved from PA, unless PA is inconsistent.
As pointed out by Andreas Blass, whether the negation of the Paris–Harrington Theorem cannot be proved from PA is a more subtle question. For example, if PA is not $\Sigma_1$-sound (i.e. PA proves a false $\Sigma_1$ statement) then PA + $\Sigma_1$-reflection is inconsistent, and therefore PA proves the negation of the Paris–Harrington Theorem.
That said, most believe that PA is $\Sigma_1$-sound (and even arithmetically sound) so it is widely believed that PA does not prove the negation of the Paris–Harrington Theorem. However, the statement that PA is $\Sigma_1$-sound is much stronger than Con(PA). Therefore, the Paris–Harrington Theorem does not answer your question as stated.
Let $A$ be any set of natural numbers that is computably enumerable, but not decidable. There are numerous natural instances of such sets, such as the set of all finite presentations of the trivial group, the set of all finite tile families that cannot tile the plane, and so on.
Every such set $A$ is saturated with infinitely many instances of the type you request. That is, there must be infinitely many candidates $a$, which are not in $A$, but such that this assertion is neither provable nor refutable in PA, or in whichever fixed background theory you wish to work, such as ZFC or ZFC + large cardinals. The reason is that otherwise, we would be able to decide membership in $A$ as follows: given a candidate $a$, wait for $a$ to show up in the enumeration of elements of $A$ and simultaneously search for a proof that $a$ is not in $A$. If non-membership was always provable for large candidates, then this would show that $A$ is decidable, contrary to assumption.
Thus, for every such $A$, there must be infinitely many particular non-members $a$ such that $a$ is not in $A$, but this is neither provable nor refutable from the fixed axioms.
To anticipate an objection, let me say that when $A$ is a "naturally" defined set, and $a$ is a particular candidate instance, then the assertion that $a$ is not in $A$ would seem to be a perfectly clear statement, not directly involving any logical "tricks". For example, we would have the assertion that a particular finite group presentation is not a presentation of the trivial group, or the assertion that a particular finite set of tiles does not tile the plane.
The logical trickery magic comes into play, of course, in the details of the explanation that a particular set $A$ is not decidable, where one might show a reduction from the halting problem or something similar. My opinion, however, is that consistency statements themselves are highly natural, and should not be considered a form of trickery. There is a sense in which every $\Pi^0_1$ statement is a consistency statement.
There's a natural example that comes up in computer programming all the time. Whether it's "about integers" is a matter of perception but it's pretty obvious that any character string straightforwardly encodes to an integer (say as ascii codes concatenated together), so it's at least pretty close.
So you've got a C program (or some other language) in the form of a disk file, that you can encode as an integer N, and you want to compile it. The compiler can be seen as a function that takes an integer (the C code) as input and produces another integer (assembly code) as output.
Most compilers have a phase that does something like this: parse the functions and expressions in the input program into a syntax tree, then run an algorithm that converts the syntax tree into code. The tree's exterior nodes (leaves) are things like constants and memory locations and the internal nodes are operations like "+", "if/else", etc. The conversion works by recursively descending the tree to emit code for the leaves (e.g. push stuff to a stack) and the interior nodes (do operations on the stack). So "(2+3)*5" could become "push 2, push 3, add, push 5, multiply".
Its intuitively obvious to any programmer that this recursive descent procedure terminates (and is in fact fairly efficient). But what is the formal proof of termination? It's structural induction on the trees, i.e. it says that the trees have a well-founded ordering. But we all know that finite rooted trees have order type epsilon-0, which by Gentzen's theorem cannot be proved well-founded in PA. So there's a fact that we use all the time, that's independent of PA, Q.E.D.
Someone please let me know if I've totally derped this.
