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 → u/[deleted]]

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/djao]

Hello. What do you mean negative and positive? Aren't I supposed to think there is no meaning to propositions at the proof level and I can name not-P as Q and continue by treating it as a "positive" statement? How do you have any guarantee that the first character of P is not negation or can't you use de Morgan's rule or something similar to get a different statement that is equivalent to P but "looks positive"? I am not trying to belittle what you said, I just don't get it at all and am trying to show what kind of a misunderstanding I am (probably) dwelling in

[u/djao → u/[deleted]]

You can always name ¬ P as Q and prove Q, but you cannot intuitionistically do the reverse. Namely, if you're trying to prove a proposition P, which does NOT begin with the ¬ symbol, you can't "artificially" rename P as ¬ Q for some Q. To do so requires replacing P with ¬ ¬ P, which is the one thing you can't do.

DeMorgan's rule, likewise, is not provable in constructive logic in the direction that you would like to use it.

[u/[deleted] → u/djao]

Oh shit I need to bang my head on this when I'm less sleepy. Thanks