<p>Your question might better be phrased, "How would complexity theory be affected by the discovery of a proof that P = NP is formally independent of some strong axiomatic system?"</p>

<p>It's a little hard to answer this question in the abstract, i.e., in the absence of seeing the details of the proof.  As Aaronson mentions in his paper, proving the independence of P = NP would require radically new ideas, not just about complexity theory, but about how to prove independence statements.  How can we predict the consequences of a radical breakthrough whose shape we currently can't even guess at?</p>

<p>Still, there are a couple of observations we can make.  In the wake of the proof of the independence of the continuum hypothesis from ZFC (and later from ZFC + large cardinals), a sizable number of people have come around to the point of view that the continuum hypothesis is <i>neither true nor false</i>.  We could ask whether people will similarly come to the conclusion that P = NP is "neither true nor false" in the wake of an independence proof (for the sake of argument, let's suppose that P = NP is proved independent of ZFC + any large cardinal axiom).  My guess is not.  Aaronson basically says that he wouldn't.  Goedel's 2nd incompleteness theorem hasn't led anyone that I know of to argue that "ZFC is consistent" is neither true nor false.  P = NP is essentially an <i>arithmetical</i> statement, and most people have strong intuitions that arithmetical statements&mdash;or at least arithmetical statements as simple as "P = NP" is&mdash;must be either true or false.  An independence proof would just be interpreted as saying that we have no way of <i>determining</i> which of P = NP and P $\ne$ NP is the case.</p>

<p>One can also ask whether people would interpret this state of affairs as telling us that there is something "wrong" with our definitions of P and NP.  Perhaps we should then redo the foundations of complexity theory with new definitions that are more tractable to work with?  At this point I think we are in the realm of wild and unfruitful speculation, where we're trying to cross bridges that we haven't gotten to and trying to fix things that ain't broke yet.  Furthermore, it's not even clear that anything <i>would</i> be "broken" in this scenario.  Set theorists are perfectly happy assuming any large cardinal axioms that they find convenient.  Similarly, complexity theorists might also, in this hypothetical future world, be perfectly happy assuming any separation axioms that they believe are true, even though they're provably unprovable.</p>

<p>In short, nothing much follows <i>logically</i> from an independence proof of P = NP.  The face of complexity theory <i>might</i> change radically in the light of such a fantastic breakthrough, but we'll just have to wait and see what the breakthrough looks like.</p>

CC BY-SA 3.0
2012-02-06T21:31:28.817Z
"P = NP is essentially an arithmetical statement". arguably diophantine equations are also "arithmetical statements"-- proven undecidable by matijasevich et al (surprised nobody's mentioned it here so far). arguably even Godels thm constructs an "arithmetical statement".
vzn
CC BY-SA 3.0
2012-02-07T05:45:11.013Z
@vzn : Are you implying something like... the question P=NP, itself  can be 'undecidable'? Please clarify.
karthik
CC BY-SA 3.0
2012-02-07T05:47:40.080Z
@Timothy Chow : Many Thanks for the answer. I should have phrased it as you have stated, but wasnt bold enough. Though, I guess, given the perceived robustness (over time, efforts and results) of most of the notions and foundations of computational complexity, it would seem very surprising, if all these were to be redone again; if the question is so far ahead of us, then, of course I agree we should not be inferring anything right now.
karthik
CC BY-SA 3.0
2012-02-07T15:13:52.867Z
@vzn: Your examples aren't just "arguably" arithmetical; they're *unquestionably* arithmetical.  But I'm not sure what your point is.  Take some diophantine equation $E$ with the property that "$E$ has no solutions" is undecidable in ZFC.  My point is that everyone I know believes that either $E$ has solutions or it doesn't, and that we just can't prove it one way or the other.  Do you believe that there is no fact of the matter about whether $E$ has solutions—that $E$ neither has nor doesn't have solutions?
Timothy Chow
CC BY-SA 3.0
2012-02-07T16:02:19.200Z
the point is theres really no apriori way to look at any statement and say "this is or is not undecidable" (say because it "looks essentially like an arithmetical statement") because historically, statements that were thought to be decidable turned out not to be and vice versa. the intuition that diophantine equations were decidable was by one of the greatest mathematicians of all time, hilbert.  I suggest anyone wanting to understand if P=?NP is decidable study aaronsens excellent ref & just look at the history of all decidable vs undecidable statements-- lots to choose from.
vzn
CC BY-SA 3.0
2012-02-07T16:15:22.343Z
further comment. it would be very interesting if someone made a list of undecidable problems & others that seem "similar"  or "nearby" that are decidable. the boundary gets very subtle. consider with automata language theory. just noticed in 2002 geraud senizergues won godel prize for proving equivalence of DPDAs is decidable. but there are close problems to this that are undecidable. lots of other examples like this. as for TCs question, can something that is undecidable _really_ have some solution? seems like an unanswerable metaphysical question at this point, there is no example of that.
vzn
CC BY-SA 3.0
2012-02-08T01:11:20.943Z
@vzn: I think you completely miss the point. The question is not whether a particular statement is *undecidable*, but whether it is *neither true nor false*.  The two concepts are entirely distinct. Would you say, for example, that ZFC is neither consistent nor inconsistent?  Everyone (else) that I know believes that either ZFC is consistent, or it isn't, even though we may have no way of determining which is the case.
Timothy Chow
CC BY-SA 3.0
2012-02-08T01:38:05.070Z
belief? this sounds like religion to me and not mathematics. you are entitled to your beliefs. there are beliefs about P=?NP in gasarchs poll if anyone wants to find out about others beliefs. last I heard it was running about 5% feeling/believing P=?NP is undecidable. its also highly apt that the best survey on the subj is written by aaronson who is the closest to a philosopher of anyone in complexity theory...
vzn
CC BY-SA 3.0
2012-02-09T13:02:45.407Z
"this sounds like religion to me and not mathematics" — Welcome to metamathematics.  Perhaps a less objectionable way of saying "X is neither true nor false" is that we have no _a priori_ reason to prefer an axiomatic system in which X is true over an axiomatic system in which X is false.  We have an (almost) universally agreed standard model of arithmetic; as a social convention, we accept arithmetic statements that hold in that model as being _really, actually_ true.  The same cannot be said for set theory.
Jeffε
CC BY-SA 3.0
2012-02-09T13:06:12.313Z
See also http://consc.net/notes/continuum.html and http://mathoverflow.net/questions/14338/what-is-the-general-opinion-on-the-generalized-continuum-hypothesis — Each mathematician's personal mix of formalism, platonism, and intuitionism is essentially a religious conviction.
Jeffε
CC BY-SA 3.0
2012-02-13T18:03:06.553Z
@vzn: You still miss the point.  Even if we grant you your personal religious beliefs, all you're saying is that you wouldn't join Aaronson and the rest of the world in declaring arithmetical sentences to be either true or false. We all agree that there's no way to tell from the *form* of a statement whether it's *undecidable*, but that's not the claim. The claim is that almost everyone except you *does* have strong intuitions that arithmetical statements are *either true or false*. Just because you don't share that conviction doesn't mean that others don't have it.
Timothy Chow
CC BY-SA 3.0
2012-02-06T18:57:43.023Z
2012-02-06T21:22:20.067Z
2012-02-06T21:22:20.067Z
Timothy Chow
<p>This is a valid question, even though perhaps a little unfortunately phrased. The best answer I can give is this reference:</p>

<blockquote>
  <p>Scott Aaronson: <a href="http://www.scottaaronson.com/papers/pnp.pdf">Is P versus NP formally independent</a>. Bulletin of the European Association for Theoretical Computer Science, 2003, vol. 81, pages 109-136.</p>
</blockquote>

<p><strong>Abstract:</strong> This is a survey about the title question, written for people who (like the author) see logic as forbidding, esoteric, and remote from their usual concerns. Beginning with a crash course on Zermelo Fraenkel set theory, it discusses oracle independence; natural proofs; independence results of Razborov,
Raz, DeMillo-Lipton, Sazanov, and others; and obstacles to proving P vs. NP independent of strong logical theories. It ends with some philosophical musings on when one should expect a mathematical question to have a deﬁnite answer.</p>

CC BY-SA 3.0
2012-02-04T15:18:28.397Z
Uh, I totally missed the fact that Aaronson's paper was already mentioned in the comments. My apologies.
Andrej Bauer
CC BY-SA 3.0
2012-02-04T09:47:13.397Z
2012-02-04T09:47:13.397Z
Andrej Bauer
<p>As proved in the <a href="https://web.archive.org/web/20221224145635/https://cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/1991/CS/CS0699.revised.pdf" rel="nofollow noreferrer">paper</a> &quot;On The Independence of P Versus NP&quot; by S. Ben-David and S. Halevi:</p>
<p>If <span class="math-container">$P \neq NP$</span> can be shown to be independent
of Peano Arithmetic, then NP has extremely-close-to-polynomial deterministic time upper bounds. In particular, in such a case, there is a <span class="math-container">$DTIME(n^{log^*(n)})$</span> algorithm
that computes SAT correctly on infinitely many huge intervals of input lengths.</p>

CC BY-SA 4.0
2019-11-27T01:30:38.153Z
2023-04-08T21:13:34.477Z
2023-04-08T21:13:34.477Z
Avi Tal
<p>As Timothy Chow explains, just knowing that a theorem is independent from a theory doesn't say much about the truth/falsity of that statement. Most non-experts confuse formal unprovability in a fixed theory (like $[ZFC][1]$) with impossibility of knowing that answer to the truth/falsity of the statement (or sometimes meaninglessness of the statement). Independence and formal unprovability always means independence/unprovability in a <em>theory</em>. It simply means that the theory can prove neither the statement nor its negation. It doesn't mean that the statement does not have a truth value, it doesn't mean that we cannot know the truth value of the statement, we might be able to add new reasonable axioms that will make the theory strong enough to be able to prove the statements or its negation. At the end, provability in a theory is a formal abstract concept. It is related to our real world experience only as a model.</p>

<p>Same applies to the <em>thesis</em> that efficient computation is captured by complexity class $\mathsf{P}$. See <a href="https://cstheory.stackexchange.com/a/2804/186">this post</a>.</p>

<p>Now you can ask if it is possible for a formal statement to not have a truth value. Generally in practice in principle, we can affirm $\Sigma_1$ (a.k.a. r.e.) properties and refute $\Pi_1$ (a.k.a. co-r.e.) properties by observations. Any statement more complex than this is not directly observable, i.e. no (finite) observation will allow you to affirm or refute the statement. However we can look at the observable logical consequences of these statements and try to use them to decide whether a statement is true or false. (For more on finitely observable properties see <a href="http://www.cs.ox.ac.uk/samson.abramsky/" rel="nofollow noreferrer">Samson Abramsky</a>'s Ph.D. thesis "<a href="http://www.cs.ox.ac.uk/files/350/thesis.pdf" rel="nofollow noreferrer">Domain Theory and the Logic of Observable Properties</a>", 1987 and <a href="http://www.cs.bham.ac.uk/~sjv/" rel="nofollow noreferrer">Steven Vickers</a>' "<a href="http://books.google.ca/books/about/Topology_via_logic.html?id=VvCKDnCrZCgC" rel="nofollow noreferrer">Topology via Logic</a>", 1996.)</p>

<p>For most mathematicians statements of higher logical complexity are also meaningful and have a truth value, but this goes into the philosophical issues in mathematics. Almost all mathematicians believe that statements in the <a href="http://en.wikipedia.org/wiki/Arithmetical_hierarchy" rel="nofollow noreferrer">arithmetical hierarchy</a> are meaningful and have definite truth values, and in some sense they view the truth value of these statements to be more definite than statements of higher logical complexity (like <a href="http://en.wikipedia.org/wiki/Continuum_hypothesis" rel="nofollow noreferrer">CH</a>). The statement $\mathsf{P} \neq \mathsf{NP}$ can be stated as a $\Sigma_2$ statement and therefore is an arithmetical statement. As such, almost all mathematicians would believe that it is meaningful and has a definite truth value. You may want have a look at <a href="https://mathoverflow.net/questions/34710/succinctly-naming-big-numbers-zfc-versus-busy-beaver">this MO question</a>, and search the posts on <a href="http://www.cs.nyu.edu/mailman/listinfo/fom" rel="nofollow noreferrer">FOM mailing list</a>. </p>

CC BY-SA 3.0
2012-02-08T18:56:03.620Z
2012-02-08T18:56:03.620Z
2017-04-13T12:57:54.530Z
Kaveh
<p>I was reading &quot;<a href="http://www.scottaaronson.com/papers/pnp.pdf" rel="noreferrer">Is P Versus NP Formally Independent?</a>&quot; but I got puzzled.</p>
<p>It is widely believed in complexity theory that <span class="math-container">$\mathsf{P} \neq \mathsf{NP}$</span>. My question is about what if this is not provable (say in <span class="math-container">$ZFC$</span>). (Let's assume that we only find out that <span class="math-container">$\mathsf{P} \neq \mathsf{NP}$</span> is independent from <span class="math-container">$ZFC$</span> but no further information about how this is proven.)</p>
<p>What will be the implications of this statement? More specifically,</p>
<h3>hardness</h3>
<p>Assuming that <span class="math-container">$\mathsf{P}$</span> capture the efficient algorithms (<a href="http://en.wikipedia.org/wiki/Cobham%27s_thesis" rel="noreferrer">Cobham–Edmonds thesis</a>) and <span class="math-container">$\mathsf{P} \neq \mathsf{NP}$</span>, we prove <span class="math-container">$\mathsf{NP\text{-}hardness }$</span> results to imply that they are beyond the present reach of our efficient algorithms. If we prove the separation, <span class="math-container">$\mathsf{NP\text{-}hardness}$</span> means that there is no polynomial time algorithm. But what does an <span class="math-container">$\mathsf{NP\text{-}hardness }$</span> result mean if the separation is not provable? What will happen to these results?</p>
<h3>efficient algorithms</h3>
<p>Does unprovability of the separation mean that we need to change our definition of efficient algorithms?</p>

CC BY-SA 3.0
2012-02-02T15:38:53.843Z
The first thing you need to ask is: formally independent of what? In mathematical logic, there are many sets of axioms people have considered. The default one is ZFC, or Zermelo-Fraenkel set theory with the Axiom of Choice. What it means to be independent of ZFC is that neither P=NP or P!=NP can be proved from these axioms.
Peter Shor 
CC BY-SA 3.0
2012-02-02T16:01:28.773Z
If you want to know what a proof for a statement of the form “whether X or not is independent of axiomatic system Y” looks like, why don’t you just read some examples?  The independence of the Axiom of Choice from the Zermelo-Fraenkel set theory is a famous example.  I voted to close as not a real question by mistake, but I meant to vote to close as off topic.
Tsuyoshi Ito
CC BY-SA 3.0
2012-02-02T16:02:40.240Z
Did you to read the very good and freely available Scott Aaronson's paper; "Is P Versus NP Formally Independent?" (http://www.scottaaronson.com/papers/pnp.pdf)
Marzio De Biasi
CC BY-SA 3.0
2012-02-02T16:03:30.497Z
there are some examples of this "independence" in math mainly wrt axiom of choice that can be looked at but so far apparently not in CS (depending on who you ask). see [what thms in CS rely on axiom of choice](http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively). in math it means roughly "the proof of the statement depends on what axioms you choose". as for hardness independence would seem to "imply" that known axiomatic systems are insufficient to capture or resolve the concept.
vzn
CC BY-SA 3.0
2012-02-02T21:16:01.787Z
Note that the question $P = NP$ is arithmetical. Hence most of the usual set-theoretic independence proofs do not apply. (E.g. forcing). In particular, there are not any known instances of natural arithmetical problems independent of ZFC.
David Harris
CC BY-SA 3.0
2012-02-02T23:40:59.593Z
I think the following question would answer this one also: [Axioms necessary for theoretical computer science](http://cstheory.stackexchange.com/questions/4816/axioms-necessary-for-theoretical-computer-science), in which case I suggest closing this question as a duplicate.
Kaveh
CC BY-SA 3.0
2012-02-02T23:43:24.473Z
ps: please also check the [FAQ] to understand the scope of cstheory.
Kaveh
CC BY-SA 3.0
2012-02-04T08:21:02.357Z
I understand I should have been more clear about what I am looking for. I have edited the question.
karthik
CC BY-SA 3.0
2012-02-07T10:15:45.447Z
The question "if X is proved independent of ZFC, and we have some theorems of the form X $\rightarrow$ Y, what happens to these theorems?" seems well-posed, and is the question that I believe the OP is asking.  The answer would seem to be: in some axiom systems, such as ZFC + X, we then have Y holding, while in ZFC + $\lnot$X we have no information about Y.  As such, these conditional theorems would still have some value.  In fact, they would have more value in this situation than if $\lnot$X were to be proved to be a theorem.
András Salamon
CC BY-SA 3.0
2012-02-08T18:17:39.847Z
@karthik, I edited the post to clarify the questions while trying to keep the original intentions. Feel free to role back or do further edits.
Kaveh
CC BY-SA 3.0
2012-02-08T20:21:50.110Z
The ZFC unprovability of P vs NP would probably have a lot more implication for Set Theory than Complexity Theory.
David Harris
CC BY-SA 3.0
2012-02-08T22:27:00.727Z
Maybe I am just confused or saying something that's too obvious to need being stated, but I suppose that if we prove formal independence, then no NP-hard problem has an algorithm whose running time can be proven to be polynomial in ZFC
Sasho Nikolov
CC BY-SA 3.0
2012-02-09T11:55:11.223Z
@Kaveh, The edits were appropriate and required. Thanks.
karthik
<cc.complexity-theory><np-hardness><big-picture><proofs><p-vs-np>
Implications of unprovability of $P\neq NP$
karthik
# Implications of unprovability of $P\neq NP$

(Asked by: username_0 on 2012-02-02)

I was reading "[Is P Versus NP Formally Independent?](http://www.scottaaronson.com/papers/pnp.pdf)" but I got puzzled.

It is widely believed in complexity theory that $\mathsf{P} \neq \mathsf{NP}$. My question is about what if this is not provable (say in $ZFC$). (Let's assume that we only find out that $\mathsf{P} \neq \mathsf{NP}$ is independent from $ZFC$ but no further information about how this is proven.)

What will be the implications of this statement? More specifically,

### hardness

Assuming that $\mathsf{P}$ capture the efficient algorithms ([Cobham–Edmonds thesis](http://en.wikipedia.org/wiki/Cobham%27s_thesis)) and $\mathsf{P} \neq \mathsf{NP}$, we prove $\mathsf{NP\text{-}hardness }$ results to imply that they are beyond the present reach of our efficient algorithms. If we prove the separation, $\mathsf{NP\text{-}hardness}$ means that there is no polynomial time algorithm. But what does an $\mathsf{NP\text{-}hardness }$ result mean if the separation is not provable? What will happen to these results?

### efficient algorithms

Does unprovability of the separation mean that we need to change our definition of efficient algorithms?

**Tags:** cc.complexity-theory, np-hardness, big-picture, proofs, p-vs-np
> **Comments:**
> **username_1**: The first thing you need to ask is: formally independent of what? In mathematical logic, there are many sets of axioms people have considered. The default one is ZFC, or Zermelo-Fraenkel set theory with the Axiom of Choice. What it means to be independent of ZFC is that neither P=NP or P!=NP can be proved from these axioms.  
> **username_2**: If you want to know what a proof for a statement of the form “whether X or not is independent of axiomatic system Y” looks like, why don’t you just read some examples?  The independence of the Axiom of Choice from the Zermelo-Fraenkel set theory is a famous example.  I voted to close as not a real question by mistake, but I meant to vote to close as off topic.  
> **username_3**: Did you to read the very good and freely available Scott Aaronson's paper; "Is P Versus NP Formally Independent?" (http://www.scottaaronson.com/papers/pnp.pdf)  
> **username_4**: there are some examples of this "independence" in math mainly wrt axiom of choice that can be looked at but so far apparently not in CS (depending on who you ask). see [what thms in CS rely on axiom of choice](http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively). in math it means roughly "the proof of the statement depends on what axioms you choose". as for hardness independence would seem to "imply" that known axiomatic systems are insufficient to capture or resolve the concept.  
> **username_5**: Note that the question $P = NP$ is arithmetical. Hence most of the usual set-theoretic independence proofs do not apply. (E.g. forcing). In particular, there are not any known instances of natural arithmetical problems independent of ZFC.  
> **username_6**: I think the following question would answer this one also: [Axioms necessary for theoretical computer science](http://cstheory.stackexchange.com/questions/4816/axioms-necessary-for-theoretical-computer-science), in which case I suggest closing this question as a duplicate.  
> **username_6**: ps: please also check the [FAQ] to understand the scope of cstheory.  
> **username_0**: I understand I should have been more clear about what I am looking for. I have edited the question.  
> **username_7**: The question "if X is proved independent of ZFC, and we have some theorems of the form X $\rightarrow$ Y, what happens to these theorems?" seems well-posed, and is the question that I believe the OP is asking.  The answer would seem to be: in some axiom systems, such as ZFC + X, we then have Y holding, while in ZFC + $\lnot$X we have no information about Y.  As such, these conditional theorems would still have some value.  In fact, they would have more value in this situation than if $\lnot$X were to be proved to be a theorem.  
> **username_6**: @karthik, I edited the post to clarify the questions while trying to keep the original intentions. Feel free to role back or do further edits.  
> **username_5**: The ZFC unprovability of P vs NP would probably have a lot more implication for Set Theory than Complexity Theory.  
> **username_8**: Maybe I am just confused or saying something that's too obvious to need being stated, but I suppose that if we prove formal independence, then no NP-hard problem has an algorithm whose running time can be proven to be polynomial in ZFC  
> **username_0**: @Kaveh, The edits were appropriate and required. Thanks.  

---

## 4 answers

### Answer by username_9 on 2012-02-06. Score: 24

Your question might better be phrased, "How would complexity theory be affected by the discovery of a proof that P = NP is formally independent of some strong axiomatic system?"

It's a little hard to answer this question in the abstract, i.e., in the absence of seeing the details of the proof. As Aaronson mentions in his paper, proving the independence of P = NP would require radically new ideas, not just about complexity theory, but about how to prove independence statements. How can we predict the consequences of a radical breakthrough whose shape we currently can't even guess at?

Still, there are a couple of observations we can make. In the wake of the proof of the independence of the continuum hypothesis from ZFC (and later from ZFC + large cardinals), a sizable number of people have come around to the point of view that the continuum hypothesis is *neither true nor false*. We could ask whether people will similarly come to the conclusion that P = NP is "neither true nor false" in the wake of an independence proof (for the sake of argument, let's suppose that P = NP is proved independent of ZFC + any large cardinal axiom). My guess is not. Aaronson basically says that he wouldn't. Goedel's 2nd incompleteness theorem hasn't led anyone that I know of to argue that "ZFC is consistent" is neither true nor false. P = NP is essentially an *arithmetical* statement, and most people have strong intuitions that arithmetical statements—or at least arithmetical statements as simple as "P = NP" is—must be either true or false. An independence proof would just be interpreted as saying that we have no way of *determining* which of P = NP and P $\ne$ NP is the case.

One can also ask whether people would interpret this state of affairs as telling us that there is something "wrong" with our definitions of P and NP. Perhaps we should then redo the foundations of complexity theory with new definitions that are more tractable to work with? At this point I think we are in the realm of wild and unfruitful speculation, where we're trying to cross bridges that we haven't gotten to and trying to fix things that ain't broke yet. Furthermore, it's not even clear that anything *would* be "broken" in this scenario. Set theorists are perfectly happy assuming any large cardinal axioms that they find convenient. Similarly, complexity theorists might also, in this hypothetical future world, be perfectly happy assuming any separation axioms that they believe are true, even though they're provably unprovable.

In short, nothing much follows *logically* from an independence proof of P = NP. The face of complexity theory *might* change radically in the light of such a fantastic breakthrough, but we'll just have to wait and see what the breakthrough looks like.

> **Comments:**
> **username_4**: "P = NP is essentially an arithmetical statement". arguably diophantine equations are also "arithmetical statements"-- proven undecidable by matijasevich et al (surprised nobody's mentioned it here so far). arguably even Godels thm constructs an "arithmetical statement".  
> **username_0**: @vzn : Are you implying something like... the question P=NP, itself  can be 'undecidable'? Please clarify.  
> **username_0**: @Timothy Chow : Many Thanks for the answer. I should have phrased it as you have stated, but wasnt bold enough. Though, I guess, given the perceived robustness (over time, efforts and results) of most of the notions and foundations of computational complexity, it would seem very surprising, if all these were to be redone again; if the question is so far ahead of us, then, of course I agree we should not be inferring anything right now.  
> **username_9**: @vzn: Your examples aren't just "arguably" arithmetical; they're *unquestionably* arithmetical.  But I'm not sure what your point is.  Take some diophantine equation $E$ with the property that "$E$ has no solutions" is undecidable in ZFC.  My point is that everyone I know believes that either $E$ has solutions or it doesn't, and that we just can't prove it one way or the other.  Do you believe that there is no fact of the matter about whether $E$ has solutions—that $E$ neither has nor doesn't have solutions?  
> **username_4**: the point is theres really no apriori way to look at any statement and say "this is or is not undecidable" (say because it "looks essentially like an arithmetical statement") because historically, statements that were thought to be decidable turned out not to be and vice versa. the intuition that diophantine equations were decidable was by one of the greatest mathematicians of all time, hilbert.  I suggest anyone wanting to understand if P=?NP is decidable study aaronsens excellent ref & just look at the history of all decidable vs undecidable statements-- lots to choose from.  
> **username_4**: further comment. it would be very interesting if someone made a list of undecidable problems & others that seem "similar"  or "nearby" that are decidable. the boundary gets very subtle. consider with automata language theory. just noticed in 2002 geraud senizergues won godel prize for proving equivalence of DPDAs is decidable. but there are close problems to this that are undecidable. lots of other examples like this. as for TCs question, can something that is undecidable _really_ have some solution? seems like an unanswerable metaphysical question at this point, there is no example of that.  
> **username_9**: @vzn: I think you completely miss the point. The question is not whether a particular statement is *undecidable*, but whether it is *neither true nor false*.  The two concepts are entirely distinct. Would you say, for example, that ZFC is neither consistent nor inconsistent?  Everyone (else) that I know believes that either ZFC is consistent, or it isn't, even though we may have no way of determining which is the case.  
> **username_4**: belief? this sounds like religion to me and not mathematics. you are entitled to your beliefs. there are beliefs about P=?NP in gasarchs poll if anyone wants to find out about others beliefs. last I heard it was running about 5% feeling/believing P=?NP is undecidable. its also highly apt that the best survey on the subj is written by aaronson who is the closest to a philosopher of anyone in complexity theory...  
> **username_10**: "this sounds like religion to me and not mathematics" — Welcome to metamathematics.  Perhaps a less objectionable way of saying "X is neither true nor false" is that we have no _a priori_ reason to prefer an axiomatic system in which X is true over an axiomatic system in which X is false.  We have an (almost) universally agreed standard model of arithmetic; as a social convention, we accept arithmetic statements that hold in that model as being _really, actually_ true.  The same cannot be said for set theory.  
> **username_10**: See also http://consc.net/notes/continuum.html and http://mathoverflow.net/questions/14338/what-is-the-general-opinion-on-the-generalized-continuum-hypothesis — Each mathematician's personal mix of formalism, platonism, and intuitionism is essentially a religious conviction.  
> **username_9**: @vzn: You still miss the point.  Even if we grant you your personal religious beliefs, all you're saying is that you wouldn't join Aaronson and the rest of the world in declaring arithmetical sentences to be either true or false. We all agree that there's no way to tell from the *form* of a statement whether it's *undecidable*, but that's not the claim. The claim is that almost everyone except you *does* have strong intuitions that arithmetical statements are *either true or false*. Just because you don't share that conviction doesn't mean that others don't have it.  

---

### Answer by username_11 on 2012-02-04. Score: 13

This is a valid question, even though perhaps a little unfortunately phrased. The best answer I can give is this reference:

> Scott Aaronson: [Is P versus NP formally independent](http://www.scottaaronson.com/papers/pnp.pdf). Bulletin of the European Association for Theoretical Computer Science, 2003, vol. 81, pages 109-136.

**Abstract:** This is a survey about the title question, written for people who (like the author) see logic as forbidding, esoteric, and remote from their usual concerns. Beginning with a crash course on Zermelo Fraenkel set theory, it discusses oracle independence; natural proofs; independence results of Razborov,
Raz, DeMillo-Lipton, Sazanov, and others; and obstacles to proving P vs. NP independent of strong logical theories. It ends with some philosophical musings on when one should expect a mathematical question to have a deﬁnite answer.

> **Comments:**
> **username_11**: Uh, I totally missed the fact that Aaronson's paper was already mentioned in the comments. My apologies.  

---

### Answer by username_12 on 2019-11-27. Score: 12

As proved in the [paper](https://web.archive.org/web/20221224145635/https://cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/1991/CS/CS0699.revised.pdf) "On The Independence of P Versus NP" by S. Ben-David and S. Halevi:

If $P \neq NP$ can be shown to be independent
of Peano Arithmetic, then NP has extremely-close-to-polynomial deterministic time upper bounds. In particular, in such a case, there is a $DTIME(n^{log^\*(n)})$ algorithm
that computes SAT correctly on infinitely many huge intervals of input lengths.


---

### Answer by username_6 on 2012-02-08. Score: 7

As Timothy Chow explains, just knowing that a theorem is independent from a theory doesn't say much about the truth/falsity of that statement. Most non-experts confuse formal unprovability in a fixed theory (like $[ZFC][1]$) with impossibility of knowing that answer to the truth/falsity of the statement (or sometimes meaninglessness of the statement). Independence and formal unprovability always means independence/unprovability in a *theory*. It simply means that the theory can prove neither the statement nor its negation. It doesn't mean that the statement does not have a truth value, it doesn't mean that we cannot know the truth value of the statement, we might be able to add new reasonable axioms that will make the theory strong enough to be able to prove the statements or its negation. At the end, provability in a theory is a formal abstract concept. It is related to our real world experience only as a model.

Same applies to the *thesis* that efficient computation is captured by complexity class $\mathsf{P}$. See [this post](https://cstheory.stackexchange.com/a/2804/186).

Now you can ask if it is possible for a formal statement to not have a truth value. Generally in practice in principle, we can affirm $\Sigma\_1$ (a.k.a. r.e.) properties and refute $\Pi\_1$ (a.k.a. co-r.e.) properties by observations. Any statement more complex than this is not directly observable, i.e. no (finite) observation will allow you to affirm or refute the statement. However we can look at the observable logical consequences of these statements and try to use them to decide whether a statement is true or false. (For more on finitely observable properties see [Samson Abramsky](http://www.cs.ox.ac.uk/samson.abramsky/)'s Ph.D. thesis "[Domain Theory and the Logic of Observable Properties](http://www.cs.ox.ac.uk/files/350/thesis.pdf)", 1987 and [Steven Vickers](http://www.cs.bham.ac.uk/~sjv/)' "[Topology via Logic](http://books.google.ca/books/about/Topology_via_logic.html?id=VvCKDnCrZCgC)", 1996.)

For most mathematicians statements of higher logical complexity are also meaningful and have a truth value, but this goes into the philosophical issues in mathematics. Almost all mathematicians believe that statements in the [arithmetical hierarchy](http://en.wikipedia.org/wiki/Arithmetical_hierarchy) are meaningful and have definite truth values, and in some sense they view the truth value of these statements to be more definite than statements of higher logical complexity (like [CH](http://en.wikipedia.org/wiki/Continuum_hypothesis)). The statement $\mathsf{P} \neq \mathsf{NP}$ can be stated as a $\Sigma\_2$ statement and therefore is an arithmetical statement. As such, almost all mathematicians would believe that it is meaningful and has a definite truth value. You may want have a look at [this MO question](https://mathoverflow.net/questions/34710/succinctly-naming-big-numbers-zfc-versus-busy-beaver), and search the posts on [FOM mailing list](http://www.cs.nyu.edu/mailman/listinfo/fom).


---

