<p>I don't know much about complexity theory, but I can answer your first questions.</p>

<ul>
<li>If the set of axioms is strong enough to encode Peano arithmetic, then you can construct unprovable statements by Gödel's first incompleteness theorem. You can easily construct infinitely many such statements, or equivalently, "detect" statements that are constructed like this. However…</li>
<li>Some statements are unprovable, but you cannot prove that they are unprovable. Using the same basic diagonalization as in the proof of Gödel's incompleteness theorems, you can e.g. consider a statement P that says "P is unprovable or false". P can't be proven true (otherwise it is false), nor proven false (otherwise it is true), nor proven unprovable (otherwise it is proven true). So, it is unprovable, but you can't prove it.</li>
<li>You can enumerate all provable statements, but not all unprovable ones — otherwise, you could just run both enumerators in parallel for long enough and that would give you a way to test whether a statement is true or provable, for any statement. I don't think there's a way to do strictly better than this "naive" enumeration.</li>
<li>Your last question is a bit vague — you're asking whether you could show that a proof of a statement exists in some non-constructive way; but what is "show" here? If you prove that the proof of a statement exists in the language of whatever axiomatic system you're using, then it "counts" as a valid proof within this system, so you actually constructed a proof…</li>
</ul>

<p>I don't think you will spontaneously find statements like the ones described in this answer in complexity theory. <a href="https://cstheory.stackexchange.com/questions/10044/implications-of-unprovability-of-p-neq-np">This other question</a> seems to indicate that this would require "radically new ideas". You might be able to fit weird provability theory statements into the language of complexity theory somehow, but it would probably be more of an artificial curiosity rather than a natural way of doing things.</p>

CC BY-SA 4.0
2018-09-30T21:45:23.957Z
Thanks for the answer. I updated the question according to "Your last question is a bit vague" -  Could we have proven that this can be proved (i.e. prove that either IP=PSPACE or IP not equal to PSPACE actually have a proof) without having a proof either way? --> This is exactly what I wanted to understand. If we could know that the relation between IP and PSPACE has a proof whichever way it turned out (equal or not), or we could prove that it is undecidable if a proof exists for some complexity class relations.
Avi Tal
CC BY-SA 4.0
2018-09-30T21:58:10.010Z
Also, can you please elaborate (or point me to where I can read) on why the unprovable statements are not enumerable?
Avi Tal
CC BY-SA 4.0
2018-10-01T08:05:01.110Z
@AviTal https://en.wikipedia.org/wiki/Entscheidungsproblem
Emil Jeřábek
CC BY-SA 4.0
2018-10-01T08:58:38.940Z
@AviTal I added a bit more detail in the question itself, Emil's link has a lot more detail about this problem space. I now understand your last question better, but I really don't know enough about complexity theory to have an answer to that.
Ted
CC BY-SA 4.0
2018-09-30T20:38:53.277Z
2018-10-01T08:56:06.657Z
2018-10-01T08:56:06.657Z
Ted
<p>Regarding your specific case of testing relationships between complexity classes, I don't see a lot of hope. It brings to mind, e.g., (<a href="https://www.sciencedirect.com/science/article/pii/030439757990046X" rel="nofollow noreferrer">Petr Hájek 1979</a>), wherein it was shown that a number of natural complexity-theoretic questions you could ask are actually strictly harder than the halting problem.</p>

<p>A very specific problem I see is, to state comparisons between reasonably richly-defined complexity classes in your formulation, you're probably going to permit (to improvise some notation) the class <span class="math-container">$\mathbf{Karp}(V)$</span>, of problems Karp-reducible to <span class="math-container">$L(V)$</span> for arbitrary NP-verifier <span class="math-container">$V$</span>, to be defined, which allows the statement <span class="math-container">$\mathbf{NP} \subseteq \mathbf{Karp}(V)$</span> to be posed as an instance of your provability problem.</p>

<p>But the decision problem for statements of this form is computationally equivalent to the language
<span class="math-container">$$\text{NPC} = \{V \mid \text{$V$ is a poly-time verifier and SAT $\le_P$ $L(V)$} \}$$</span>
and, assuming <span class="math-container">$\mathbf{P} \ne \mathbf{NP}$</span>, NPC is actually <span class="math-container">$\mathbf{\Sigma_2}$</span>-complete, i.e. one level up <span class="math-container">$\mathbf{AH}$</span> from the halting problem.*</p>

<p>Since you're concerned about automatically discovering independence of the statements in particular, it should be noted that as soon as a logical theory is known to be undecidable, it's always the independent statements that cause the trouble. If you restrict your attention to the statements which are provably true or false in your proof system, you can solve your problem just by enumerating proofs. Since the decision problem you care about is probably going to be undecidable (as per the remarks above), independent statements are guaranteed to exist if your proof system has a bare minimum of desirable properties (i.e. computably verifiable proofs).</p>

<p>Of course, none of this precludes the possibility that specific conjectures of interest about complexity class inclusions or separations will one day be directly shown to be independent. I think other responders are able to canvass the current state of the art on that possibility better than I.</p>

<hr>

<p>*If you're interested in showing that NPC is actually <span class="math-container">$\mathbf{\Sigma_2}$</span>-complete, you can reduce from FIN defined in Hájek's paper, first to a promise variant of FIN where only the first k inputs of the input machine can be halting if any are, and as far as I can tell you'll need to construct <span class="math-container">$V$</span> using a delayed diagonal argument a la Ladner's theorem. If anyone knows of a more succinct approach I'd be very curious.</p>

CC BY-SA 4.0
2018-10-01T08:00:52.673Z
2018-10-01T08:00:52.673Z
gdmclellan
<p>I understand that this may depend on the specific set of axioms, but is there a general way (algorithm) for <strong>automatically</strong> detecting unprovable statements within a set of axioms?</p>

<p>For example: If there is some conjecture that I am trying to prove, but might not be provable, can I know it in advance by some <strong>automatic</strong> method?</p>

<p>If this is generally undecidable, can 'some' (maybe not all) conjectures be ruled out <strong>automatically</strong>? Can this be done at least partially?</p>

<p>I am mainly concerned about complexity class relations. Are there any known unprovable relations in this field? If there are, how where they achieved?</p>

<p>In addition, can the "undecidability of proof existence" for some complexity class relation conjectures be proved?</p>

<p>A more specific example: It was proved that IP = PSPACE. Could we have proven that this can be proved (i.e. prove that either IP=PSPACE or IP not equal to PSPACE actually have a proof) without having a proof either way? Or at least, could we decide that a proof exists?</p>

CC BY-SA 4.0
2018-10-01T06:09:02.747Z
Isn't this almost exactly Hilbert's Entscheidungsproblem? It's well-known that you can enumerate all of the statements of, say, ZFC, for which there exists a proof of the statement. (Just enumerate strings forever until you discover one that validates as a proof of the statement you want.) If the set of unprovable statements was enumerable (let alone decidable), you could just alternate between enumerating provable statements and unprovable statements until your statement showed up, which would solve the Entscheidungsproblem, contradicting the famous results of Church and Turing.
gdmclellan
<ds.algorithms><computability>
Algorithm for identifying unprovable statements
Avi Tal
# Algorithm for identifying unprovable statements

(Asked by: username_0 on 2018-09-30)

I understand that this may depend on the specific set of axioms, but is there a general way (algorithm) for **automatically** detecting unprovable statements within a set of axioms?

For example: If there is some conjecture that I am trying to prove, but might not be provable, can I know it in advance by some **automatic** method?

If this is generally undecidable, can 'some' (maybe not all) conjectures be ruled out **automatically**? Can this be done at least partially?

I am mainly concerned about complexity class relations. Are there any known unprovable relations in this field? If there are, how where they achieved?

In addition, can the "undecidability of proof existence" for some complexity class relation conjectures be proved?

A more specific example: It was proved that IP = PSPACE. Could we have proven that this can be proved (i.e. prove that either IP=PSPACE or IP not equal to PSPACE actually have a proof) without having a proof either way? Or at least, could we decide that a proof exists?

**Tags:** ds.algorithms, computability
> **Comments:**
> **username_1**: Isn't this almost exactly Hilbert's Entscheidungsproblem? It's well-known that you can enumerate all of the statements of, say, ZFC, for which there exists a proof of the statement. (Just enumerate strings forever until you discover one that validates as a proof of the statement you want.) If the set of unprovable statements was enumerable (let alone decidable), you could just alternate between enumerating provable statements and unprovable statements until your statement showed up, which would solve the Entscheidungsproblem, contradicting the famous results of Church and Turing.  

---

## 2 answers

### Answer by username_2 on 2018-09-30. Score: 5

I don't know much about complexity theory, but I can answer your first questions.

* If the set of axioms is strong enough to encode Peano arithmetic, then you can construct unprovable statements by Gödel's first incompleteness theorem. You can easily construct infinitely many such statements, or equivalently, "detect" statements that are constructed like this. However…
* Some statements are unprovable, but you cannot prove that they are unprovable. Using the same basic diagonalization as in the proof of Gödel's incompleteness theorems, you can e.g. consider a statement P that says "P is unprovable or false". P can't be proven true (otherwise it is false), nor proven false (otherwise it is true), nor proven unprovable (otherwise it is proven true). So, it is unprovable, but you can't prove it.
* You can enumerate all provable statements, but not all unprovable ones — otherwise, you could just run both enumerators in parallel for long enough and that would give you a way to test whether a statement is true or provable, for any statement. I don't think there's a way to do strictly better than this "naive" enumeration.
* Your last question is a bit vague — you're asking whether you could show that a proof of a statement exists in some non-constructive way; but what is "show" here? If you prove that the proof of a statement exists in the language of whatever axiomatic system you're using, then it "counts" as a valid proof within this system, so you actually constructed a proof…

I don't think you will spontaneously find statements like the ones described in this answer in complexity theory. [This other question](https://cstheory.stackexchange.com/questions/10044/implications-of-unprovability-of-p-neq-np) seems to indicate that this would require "radically new ideas". You might be able to fit weird provability theory statements into the language of complexity theory somehow, but it would probably be more of an artificial curiosity rather than a natural way of doing things.

> **Comments:**
> **username_0**: Thanks for the answer. I updated the question according to "Your last question is a bit vague" -  Could we have proven that this can be proved (i.e. prove that either IP=PSPACE or IP not equal to PSPACE actually have a proof) without having a proof either way? --> This is exactly what I wanted to understand. If we could know that the relation between IP and PSPACE has a proof whichever way it turned out (equal or not), or we could prove that it is undecidable if a proof exists for some complexity class relations.  
> **username_0**: Also, can you please elaborate (or point me to where I can read) on why the unprovable statements are not enumerable?  
> **username_3**: @AviTal https://en.wikipedia.org/wiki/Entscheidungsproblem  
> **username_2**: @AviTal I added a bit more detail in the question itself, Emil's link has a lot more detail about this problem space. I now understand your last question better, but I really don't know enough about complexity theory to have an answer to that.  

---

### Answer by username_1 on 2018-10-01. Score: 2

Regarding your specific case of testing relationships between complexity classes, I don't see a lot of hope. It brings to mind, e.g., ([Petr Hájek 1979](https://www.sciencedirect.com/science/article/pii/030439757990046X)), wherein it was shown that a number of natural complexity-theoretic questions you could ask are actually strictly harder than the halting problem.

A very specific problem I see is, to state comparisons between reasonably richly-defined complexity classes in your formulation, you're probably going to permit (to improvise some notation) the class $\mathbf{Karp}(V)$, of problems Karp-reducible to $L(V)$ for arbitrary NP-verifier $V$, to be defined, which allows the statement $\mathbf{NP} \subseteq \mathbf{Karp}(V)$ to be posed as an instance of your provability problem.

But the decision problem for statements of this form is computationally equivalent to the language
$$\text{NPC} = \{V \mid \text{$V$ is a poly-time verifier and SAT $\le\_P$ $L(V)$} \}$$
and, assuming $\mathbf{P} \ne \mathbf{NP}$, NPC is actually $\mathbf{\Sigma\_2}$-complete, i.e. one level up $\mathbf{AH}$ from the halting problem.\*

Since you're concerned about automatically discovering independence of the statements in particular, it should be noted that as soon as a logical theory is known to be undecidable, it's always the independent statements that cause the trouble. If you restrict your attention to the statements which are provably true or false in your proof system, you can solve your problem just by enumerating proofs. Since the decision problem you care about is probably going to be undecidable (as per the remarks above), independent statements are guaranteed to exist if your proof system has a bare minimum of desirable properties (i.e. computably verifiable proofs).

Of course, none of this precludes the possibility that specific conjectures of interest about complexity class inclusions or separations will one day be directly shown to be independent. I think other responders are able to canvass the current state of the art on that possibility better than I.

---

\*If you're interested in showing that NPC is actually $\mathbf{\Sigma\_2}$-complete, you can reduce from FIN defined in Hájek's paper, first to a promise variant of FIN where only the first k inputs of the input machine can be halting if any are, and as far as I can tell you'll need to construct $V$ using a delayed diagonal argument a la Ladner's theorem. If anyone knows of a more succinct approach I'd be very curious.


---

