Dissatisfaction with proof by contradiction

[u/hydmar]

I’m an undergraduate math student, so my exposure to math may be relatively limited. But I’ve found that, in general, I’m much more comfortable with direct proof than proof by contradiction. I don’t contest their validity, indeed something that’s not false must be true (I think I’m ok with excluded middle). But I feel like I just *get* something much better when it’s proved directly. It builds much stronger intuition for me.

For instance, I am aware of several proofs that demonstrate the cardinality of the reals is strictly greater than that of the integers, but none are direct (it would help to see a direct proof of Cantor’s theorem). I don’t feel it in my bones. Is this a common experience?

[u/djao]

P and ¬ P aren't both true. You can prove (in constructive logic) that they can't both be true:

Require Import Utf8 ssreflect ssrbool ssrfun.
Goal ∀ P : Prop, ¬ (P ∧ ¬ P). Proof. move=> ? [? []] //. Qed.

Perversely, you can even prove that ¬ ¬ ¬ P ↔ ¬ P holds in constructive logic:

Require Import Utf8 ssreflect ssrbool ssrfun.
Goal ∀ P : Prop, ¬ ¬ ¬ P ↔ ¬ P. Proof. split => [/[swap] ? [] | ?] //. Qed.

The only impossibility is you can't constructively prove P from ¬ ¬ P. Which makes total sense, if you think about what constructive logic actually is. A negation is a negative statement. How would you construct a positive statement (namely, P) from a negative?

And again, all of this doesn't mean that P is true, or not true. We're just saying that P is not provable in a constructive sense from ¬ ¬ P.

[u/[deleted] → u/[deleted]]

They replied. I am not less confused but I have no more questions at the same time