undecidable sentences of first-order arithmetic whose truth values are unknown

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.)

-
I would be interested in something which is not of this sort. Anyway, all of Harvey's examples are true in the standard model. (Under appropriate background assumptions on large cardinals.) – Andrés E. Caicedo Dec 22 '11 at 6:52
I do not know about an specific sentence, but it is worth noticing that it is easy to build pair of sentences such that at one of them is of the kind you want. How? Let us consider $\psi$ an undecidable sentence which is true (e.g., $Con(ZFC)$) and let us consider $\varphi$ a sentence whose truth value is unknown (e.g., Riemann Hypthesis). Then, either the sentence $\psi \land \varphi$ or the sentence $\psi \land \neg \varphi$ is of the kind you are interested on. – boumol Dec 22 '11 at 9:39
@Carl: I think the best scenario would be a arithmetic sentence $\phi$ such that both $PA+\phi$ and $PA+\lnot\phi$ are equiconsistent with $PA$, but for which we do not know whether $\phi$ or $\lnot\phi$ holds in ${\mathbb N}$. I doubt any "natural" such examples are known. – Andrés E. Caicedo Dec 22 '11 at 15:58
François, perhaps this is what symplectomorphic means: Say that $X$ is known at time $t$ if and only if someone has, at some time $t'\le t$, exhibited a proof of $X$ from ZFC + some standard large cardinal axiom. Then he seeks an explicit example of arithmetical statement $X$ such that, taking $t$ to be the year 2011, $X$ is not known, but "PA does not prove $X$" is known and "PA does not prove $\neg X$" is known. This seems roughly in line with Koellner's notion of absolute independence, and doesn't trivialize just because arithmetical statements are all either true or false. – Timothy Chow Dec 22 '11 at 17:10
It might also help symplectomorphic if someone explains why we run into silly examples if we draw a bright line at (say) ZFC specifically, or if we allow "unnatural" statements. – Timothy Chow Dec 22 '11 at 17:14

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

• $\text{PA}+\text{Con}(T)$ proves that $\varphi$ and $\psi$ are equivalent.
• $T$ does not prove $\psi$.
• $T$ does not prove $\neg\psi$.

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.

-
There is nothing special about $\mathrm{Con}(T)$. If $\gamma$ is any sentence unprovable in $T$, and $\phi$ any sentence, then there is a $\psi$ such that $\vdash\gamma\to(\phi\leftrightarrow\psi)$, $T\nvdash\psi$, and $T\nvdash\neg\psi$. Proof: By the Gödel–Rosser theorem, there is an $\alpha$ independent of $T+\neg\gamma$. Put $\psi=(\gamma\land\phi)\lor(\neg\gamma\land\alpha)$. – Emil Jeřábek Apr 18 '12 at 15:39
Yes, I agree with that. – Joel David Hamkins Apr 18 '12 at 16:35
The argument presumes that $T$ is computably axiomatizable, so that the Rosser sentence is available. This should be understood as a hypothesis in the theorem. (Vote up this comment if I should edit to say this explicitly.) – Joel David Hamkins Nov 8 '12 at 2:42

What you want is called [first-order] Arithmetical Splitting. I have spoken and written a lot about it in the last few years. Send me a message and I can show you some drafts about the current state of this most important topic.

Yes, we should not be able to form any preference, like in the case of PH, where it is clear that PH is better than \neg \PH.

-
Hi Andrey! I didn't ask the question, but naturally I am very interested in this topic. (Tried to email you but the email address I have for you has been discontinued.) Would you please email me some of those drafts you mentioned? – Andrés E. Caicedo Jan 31 '12 at 2:53

I think there is a little misunderstanding.

Paris and Harrington showed the strengthened finite Ramsey theorem is true but unprovable in first-order arithmetic; I don't know if there's a proof that extends the result to full-on undecidability rather than just unprovability.

Indeed, the Wikipedia page is only talking about unprovability, but the negation of the strengthened finite Ramsey theorem is also unprovable in Peano arithmetic for "trivial" reasons: if you can prove this negation, then second order arithmetic can also prove this negation (because second order arithmetic is stronger than Peano arithmetic), so this would mean that second order arithmetic is inconsistent (because second order arithmetic proves the strengthened finite Ramsey theorem).

So if you take for granted that second order arithmetic is consistent, then your example is actually undecidable in Peano arithmetic. And there are other examples like Goodstein's theorem.

-
Yes, I realize now that undecidability of the Ramsey theorem is trivial, once we have unprovability. But this is not an answer to the question: the Ramsey theorem -- like Goodenstein's theorem -- is, in fact, true on the standard model of arithmetic. I'm interested in undecidable cases where the truth value hasn't been settled. – symplectomorphic Dec 22 '11 at 16:51
Once again, I don't know what you mean by "truth value". An ultrafinitist (someone that does not believe in the infinity) will probably tell you that the truth value of Goodstein's theorem has not been settled at all, and that it's most likely false because experimentally you will never reach 0. On the other hand, someone like Woodin will probably tell you that the truth value of CH is known: it's false because there are strong arguments against it and few arguments for it. And most set theorists will tell you that large cardinal axioms are true because nobody want them to be false. – Guillaume Brunerie Dec 22 '11 at 17:15
(of course this only applies to platonists, people who believe that there is a real mathematical universe somewhere, where every question has an answer) – Guillaume Brunerie Dec 22 '11 at 17:21
Guillaume, these are not the sort of examples the question is after. If it is an issue, work in a metatheory extending ZFC with enough large cardinals. – Andrés E. Caicedo Dec 22 '11 at 17:44
@Andres, I know, I was just clarifying the unprovable/undecidable point. – Guillaume Brunerie Dec 22 '11 at 18:39

I'd say Con(ZF) isn't known to be undecidable--it's only undecidable if it's true. If it's false, that fact is $\Sigma^0_1$ and therefore provable. We want a sentence that's $\Sigma^0_2$ or higher.

This might be an almost-example: http://www.cs.uchicago.edu/~simon/RES/collatz.pdf

It proves that a generalization of the 3n+1 conjecture is $\Pi_2$-complete. But it's not quite what is asked, since it's about a family of problems rather than a single sentence.

-
Regarding the objection of your first paragraph, if Con(ZF) is false, then there are no independent sentences of any complexity. – Joel David Hamkins Jan 5 '12 at 13:18

If you'll settle for an important open question that's independent from some weak fragments of PA, the P vs NP problem is an example.

http://www.scottaaronson.com/papers/pnp.pdf discusses this a little bit.

Or if you'll take a completely artificial problem that's more strongly independent, just generate a very long random proposition in PA's language, by rolling dice. You won't know its truth value, and from Chaitin's theorem it will almost certainly be independent of any reasonable axiom system.

-
P = NP is independent of those weak fragments only if a certain cryptographic hypothesis holds, so this is not really an example. I don't think the second example works either since symplectomorphic wants a specific example of a statement that is known to be undecidable. – Timothy Chow Dec 29 '11 at 15:04

If we omit the qualification "natural" from the question, then, of course, the most obvious examples are the arithmetized versions of metamathematical sentences expressing the (absolute) consistency of ZFC, or any axiom-system of set theory far weaker than ZFC within which arithmetic can be developed. Indeed, e.g. Con(ZF) is a sentence of arithmetic that we obtain by Godel-numbering from the metamathematical sentence "there is no proof of 0=1 from ZF." And if ZF is consistent, then Con(ZF) is undecidable in Peano arithmetic with unknown truth value. Actually, on the one hand, Con(ZF) implies Con(PA), and the arithmetical proof of $\lnot$Con(ZF) would yield a direct proof of the inconsistency of ZF.

As far as the "naturalness" condition is concerned, it seems that there will be no easy way to find "natural" sentences of this kind. Indeed, some natural candidates as e.g. the Goldbach conjecture are excluded, since they should be true, if they turn out to be undecidable. More precisely, any $\Pi_1$ sentence $S$ of arithmetic is true whenever $S$ is undecidable. Indeed, if $S$ is false, then its negation is a true $\Sigma_1$ sentence, and Peano arithmetic proves any true $\Sigma_1$ sentence.

-