How is reductio ad absurdum unintuitive?

Question

I am not asking about opinions here, I'm asking for the reasoning behind the decision of certain logics/frameworks, like e.g. Intuitionism, to not contain RAA as a valid rule of inference. There is an assumption behind my assertion that there even is such a reasoning; some things are self-evident and thus do not have any reasoning beyond (universal) opinion. Other statements simply seem intuitively true, but the assertion of their truth may produce sufficiently counter-intuitive implications that cancel out, in a way, the intuitiveness of the original statement.

As such, my understanding is this:

The difference between logics and frameworks allowing RAA, and those that don't, is not that they disagree on RAA being intuitive in and of itself. Rather, accepting RAA as valid produces results that some peope find too counter-intuitive. Shortly put, the disagreement lies in the implications of RAA.

Question:

What counter-intuitive implications is it that motivates the removal of RAA as a rule of inference?

Meta:

I understand if this Q is too philosophical for Math.SE, and I will move it if its reception indicates this is true.

Answer 1

I disagree with the premise that intuitionists reject RAA because of counter-intuitive consequences, not because RAA itself is unintuitive. I think most people who are philosophically committed to intuitionism would claim that RAA is unintuitive on its face.

I want to clarify something first. The following form of RAA is perfectly acceptable to the intuitionist: If we assume $P$ and derive a contradiction, then we conclude $\lnot P$. In fact, in intuitionistic logic, $\lnot P$ is usually taken to be an abbreviation for $P\to \bot$, and the canonical way to prove $P\to \bot$ is to assume $P$ and derive $\bot$.

Similarly, the following is acceptable to the intuitionist: If we assume $\lnot P$ and derive a contradiction, then we conclude $\lnot \lnot P$. This is just an instance of the version of RAA from the last paragraph.

What the intuitionist rejects is the following form of RAA: If we assume $\lnot P$ and derive a contradiction, then we conclude $P$. As you can see, the issue comes down to double negation elimination: in intuitionistic logic, we cannot conclude $P$ from $\lnot\lnot P$.

To understand why, it's helpful to interpret the assertion $P$ as meaning not "$P$ is true", but rather something like "I have a proof of $P$", or "I have verified $P$". In this reading, $\lnot P$ means "I have ruled out that I could every verify $P$", and $\lnot\lnot P$ means "I have ruled out that I could rule out verifying $P$".

If I assume $\lnot P$ and derive a contradiction, then I have ruled out the possibility that I could rule out verifying $P$. This is not the same as actually having a verification of $P$ in hand. And that's why intuitionists find RAA unintuitive.

Answer 2

Without the use of the falsum $\bot$, following the textbook 'Foundations of logic and mathematics' by Nievergelt as a reference, especially Sections 1.1 and 4.1., there are two different laws.

Law of Reductio Ad Absurdum: $$(P \to Q) \to ((P \to \neg Q) \to \neg P),$$

Converse Law of Contraposition: $$(\neg P \to \neg Q) \to (Q \to P),$$

The Law of Reductio Ad Absurdum, as stated above, is valid in Intuitionistic Logic. What However, the Converse Law of Contraposition is not provable over Intuitionistic Logic.

---

Appendix:

For the convenience of the reader, I write down the axioms of Intuitionistic Logic, as taken from Nievergelt's book. In his book, the axioms of Intuitionistic Logic are stated completely over the language $\{\neg, \to, \vee, \wedge\}$, with the symbol $\neg$ for negation, the symbol $\to$ for implication, the symbol $\vee$ for disjunction and the symbol $\wedge$ for conjunction. In this language, the use of a constant symbol $\bot$ for the falsum is avoided.

To give the details, let $CL^-$ be the system consists of the following two axiom schemas:

1. $P \to (Q \to P)$
2. $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$

Let $T$ denote $CL^{-}$ together with the additional five axiom schemas:

3. $(P \wedge Q) \to P$
4. $(P \wedge Q) \to Q$
5. $P \to (Q \to (P \wedge Q)$
6. $P \to (P \vee Q)$
7. $Q \to (P \vee Q)$
8. $(P \to R) \to ((Q \to R) \to ((P\vee Q) \to R))$

Intuitionistic Logic (IL) is $T$ plus the Special Law of Reductio Ad Absurdum -- $$(P \to \neg P) \to \neg P$$ and also plus the Law of Denial Of the Antecedent $$\neg P \to (P \to Q).$$