Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?"

share|cite|improve this question
While I'm not sure if this is an exact duplicate or not, the question was answered in either 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
up vote 5 down vote accepted

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.