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?"
 A: 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.
