Algorithm for identifying unprovable statements 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?
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.