Algorithm for identifying unprovable statements

Question

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?

Answer 1

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

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