I am looking for statements $P$ of Peano Arithmetic ($\textsf{PA}$) that have the following properties:
- They are as concrete and simple as possible.
- It is provable by finitistic means that neither $P$ nor $\neg P$ can be proved within $\textsf{PA}$, in the sense that a proof of either of both can be turned into an inconsistency of $\textsf{PA}$.
- Ideally, I'd like $P$ to be true in the standard natural numbers of $\textsf{ZFC}$, say.
The third point implies the unprovability of $\neg P$ in $\textsf{PA}$ assuming the consistency of $\textsf{ZFC}$ (i.e., there is a way of turning a proof of $\neg P$ in $\textsf{PA}$ into an inconsistency of $\textsf{ZFC}$). However, this is not as strong as the finitistic argument I am looking for in the second point.
To clarify: The whole point of the question is that I don't want to rely on a strong ambient set theory like $\textsf{ZFC}$ for the proof of undecidability of $P$, but rather have an algorithm turning a hypothetical proof of $P$ or $\neg P$ into an inconsistency of $\textsf{PA}$.
The example $P = \text{Con}\ \textsf{PA}$ that DanulG mentioned actually does meet half of the requirements, since as far as I understand Goedel's argument is, in principle, of the desired algorithmic nature. With the Rosser trick, one can indeed get a statement $P$ such that also a proof of $\neg P$ can be turned into an inconsistency of $\text{Con}\ \textsf{PA}$. However, I'd be a bit happier with non metamathematical statements. Goodstein's Theorem or Kirby-Paris' "Hydra" would be fine, for example.
2nd edit: The Paris-Harrington Theorem (http://www.karlin.mff.cuni.cz/~krajicek/ph.pdf) meets at least half of the requirements, as Paris and Harrington show that the combinatorial principle $Q$ they consider implies $\text{Con}\ \textsf{PA}$ within $\textsf{PA}$, i.e. they prove $\textsf{PA} \vdash (Q\Rightarrow \text{Con}\ \textsf{PA})$. What about $\neg Q$? Surely we cannot have $\textsf{PA}\vdash (\neg Q\Rightarrow\text{Con}\ \textsf{PA})$ as well, but is there still some finitistic means to deduce from a proof of $\neg Q$ an inconsistency of $\textsf{PA}$, and not only of $\textsf{ZFC}$ or whatever stronger set theory one has to use to prove $Q$? Any ideas here?
Thank you!