# Is it always possible to decide if either a statement or its negation is provable in a given axiomatic system?

The question is essentially in the title. Given an axiomatic system of unspecified power (it could be set theory or it could be propositional logic) and a statement A, can I always decide if either A or its negation is provable in the axiomatic system? I know that if I specify one of the above, it is not possible, but what if I ask for "A is provable or the negation of A is provable?"

-
While I'm not sure if this is an exact duplicate or not, the question was answered in either math.stackexchange.com/questions/65248 or one of the links in the body; or one of the links in the links in the body; or one of the links in one of the links in one of the links in the body of the linked question. – Asaf Karagila Oct 2 '11 at 23:37
Any reasonable response to your question depends on what you mean by "can I decide". What are you allowing yourself to use in your decision? If you use the axiomatic system only, for example, then the answer is "no" by Godel's incompleteness theorem (as I suspect you know since you're asking this question). – Greg Martin Oct 2 '11 at 23:37
I hope you mean "can I decide" as in, "is there a terminating algorithm which determines," in which case it's pretty obvious that the answer is no. – JeremyKun Oct 2 '11 at 23:41

You already know that "Is $A$ provable?" is undecidable.
This entails that "Is one of $A$ and $\neg A$ provable?" is also undecidable.
Suppose, to the contrary, that you had a machine that decided "Is one of $A$ and $\neg A$ provable?" I can use that to decide "Is $A$ provable?". Namely, given any $A$ I first feed it into your machine. If that answers "no", then I'm done because if neither $A$ nor $\neg A$ is provable, then certainly $A$ is not provable.
Otherwise, I start enumerating all valid formal proofs until I reach one that proves either of $A$ and $\neg A$ -- your machine has promised me that I'll find one sooner or later. If I find a proof of $A$, then I'm done. If I find a proof of $\neg A$, then I know that $A$ is not provable (for if it was, the axiomatic system would be inconsistent, and then "Is $A$ provable?" is trivially decidable, contrary to assumptions).
But that means I have a procedure for finding out whether an arbitrary $A$ can be proved. Since this is known to be impossible, your machine cannot exist.