Godel's undecidable sentences in first-order arithmetic were guaranteed to be true, by construction. But are there examples of specific sentences known to be undecidable in first-order arithmetic whose truth values aren't known? I'm thinking, by contrast, of the situation in set theory: CH is undecidable in ZFC, but its truth value is, in some sense, unknown.
Paris and Harrington showed the strengthened finite Ramsey theorem is true (in the sense of provable in second-order arithmetic) but undecidable in first-order arithmetic. I'm asking for "natural" examples in this general vein — but whose truth values haven't yet been settled.
EDIT. Let me clarify my interest in the question, which is more philosophical than mathematical. I asked it on the basis of the following passage in Peter Koellner's paper "On the Question of Absolute Undecidability":
The above statements of analysis [i.e. all projective sets of reals are Lebesgue measurable] and set theory [i.e. CH] differ from the early arithmetical instances of incompleteness in that their independence does not imply their truth. Moreover, it is not immediately clear whether they are settled at any level of the hierarchy. They are much more serious cases of independence.
What I'm asking is whether there are "much more serious cases" of independence even in first-order arithmetic — and not in the trivial case of full-on ZFC, like V=L, etc. By a sentence with "unknown truth value," I just mean a sentence that hasn't been proved in a theory stronger than first-order arithmetic. (For example, Paris and Harrington proved the strengthened finite Ramsey theorem in second-order arithmetic.)
Best Answer
Update. I've improved the argument to use only the consistency of $T$. (2/7/12): I corrected some over-statements previously made about Robinson's Q.
I claim that for every statement $\varphi$, there is a variant way to express it, $\psi$, which is equivalent to the original statement $\varphi$, but which is formally independent of any particular desired consistent theory $T$.
In particular, if $\varphi$ is your favorite natural open question, whose truth value is unknown, then there is an equivalent formulation of that question which exhibits formal independence in the way you had requested. In this sense, every open question is equivalent to an assertion with the property you have requested. I take this to reveal certain difficult subtleties with your project.
Theorem. Suppose that $\varphi$ is any sentence and $T$ is any consistent theory containing weak arithmetic. Then there is another sentence $\psi$ such that
Proof. Let $R$ be the Rosser sentence for $T$, the self-referential assertion that for any proof of $R$ in $T$, there is a smaller proof of $\neg R$. The Gödel-Rosser theorem establishes that if $T$ is consistent, then $T$ proves neither $R$ nor $\neg R$. Formalizing the first part of this argument shows that $\text{PA}+\text{Con}(T)$ proves that $R$ is not provable in $T$ and hence that $R$ is vacuously true. Formalizing the second part of this argument shows that $\text{Con}(T)$ implies $\text{Con}(T+R)$, and hence by the incompleteness theorem applied to $T+R$, we deduce that $T+R$ does not prove $\text{Con}(T)$. Thus, $T+R$ is a strictly intermediate theory between $T$ and $T+\text{Con}(T)$.
Now, let $\psi$ be the assertion $R\to (\text{Con}(T)\wedge \varphi)$. Since $\text{PA}+\text{Con}(T)$ proves $R$, it is easy to see by elementary logic that $\text{PA}+\text{Con}(T)$ proves that $\varphi$ and $\psi$ are equivalent.
The statement $\psi$, however, is not provable in $T$, since if it were, then $T+R$ would prove $\text{Con}(T)$, which it does not by our observations above.
Conversely, $\psi$ is not refutable in $T$, since any such refutation would mean that $T$ proves that the hypothesis of $\psi$ is true and the conclusion false; in particular, it would require $T$ to prove the Rosser sentence $R$, which it does not by the Gödel-Rosser theorem. QED
Note that any instance of non-provability from $T$ will require the consistency of $T$, and so one cannot provide a solution to the problem without assuming the theory is consistent.
The observation of the theorem has arisen in some of the philosophical literature you may have in mind, based on what you said in the question. For example, the claim of the theorem is mentioned in Haim Gaifman's new paper "On ontology and realism in mathematics," which we read in my course last semester on the philosophy of set theory; see the discussion on page 24 of Gaifman's paper and specifically footnote 35, where he credits a fixed-point argument to Torkel Franzen, and an independent construction to Harvey Friedman.
My original argument (see edit history) used the sentence $\text{Con}(T)\to(\text{Con}^2(T)\wedge\varphi)$, where $\text{Con}^2(T)$ is the assertion $\text{Con}(T+\text{Con}(T))$, and worked under the assumption that $\text{Con}^2(T)$ is true, relying on the fact that $T+\text{Con}(T)$ is strictly between $T$ and this stronger theory. The current argument uses the essentially similarly idea that $T+R$ is strictly between $T$ and $T+\text{Con}(T)$, thereby reducing the consistency assumption.