Can proof by contradiction 'fail'?

Question

I am familiar with the mechanism of proof by contradiction: we want to prove $P$, so we assume $¬P$ and prove that this is false; hence $P$ must be true.

I have the following devil's advocate question, which might seem to be more philosophy than mathematics, but I would prefer answers from a mathematician's point of view:

When we prove that $¬P$ is "false", what we are really showing is that it is inconsistent with our underlying set of axioms. Could there ever be a case were, for some $P$ and some set of axioms, $P$ and $¬P$ are both inconsistent with those axioms (or both consistent, for that matter)?

Answer 1

The situation you ask about, where $P$ is inconsistent with our axioms and $\neg P$ is also inconsistent with our axioms, would mean that the axioms themselves are inconsistent. Specifically, the inconsistency of $P$ with the axioms would mean that $\neg P$ is provable from those axioms. If, in addition, $\neg P$ is inconsistent with the axioms, then the axioms themselves are inconsistent --- they imply $\neg P$ and then they contradict that. (I have phrased this answer so that it remains correct even if the underlying logic of the axiom system is intuitionistic rather than classical.)

Answer 2

It is possible for both $P$ and $ \neg P $ to be consistent with a set of axioms. If this is the case, then $P$ is called independent. There are a few things known to be independent, such as the Continuum Hypothesis being independent of ZFC.

It is also possible for both $P$ and $ \neg P $ to be inconsistent with a set of axioms. In this case the axioms are considered inconsistent. Inconsistent axioms result in systems which don't work in a way that is useful for engaging in mathematics.

Proof by contradiction depends on the law of the excluded middle. Constructivist mathematics, which uses intuitionistic logic, rejects the use of the law of the excluded middle, and this results in a different type of mathematics. However, this doesn't protect them from the problems resulting from inconsistent axioms.

There are logical systems called paraconsistent logic which can withstand inconsistent axioms. However, they are more difficult to work with than standard logic and are not as widely studied.