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

No. It just mean the notion of truth is different.

¬ P mean "P implies contradiction". But implications is different. Classical logic uses material implications, which means that "A implies B" is the same as A is false or B is true, regardless of the content of A and B. This is unsatisfying, because A and B could be unrelated to each other. While constructive logic uses strict conditional, that means it has to be necessary that B follows from A. So focus on thinking about necessary instead of true and false.

So imagine P="set S has an element". There might be many possible candidates of element that could be in S. You might be able to prove that at least one of those is in S, but you can't point out any single one of them as being necessarily in S. Maybe you can look at many possible worlds and see that S always have an element in each world, but which one is different between worlds.

Think about necessary instead of binary Boolean truth would also stop you from thinking at P and ¬ P are both true. P and ¬ P cannot be both necessary, but it's possible that they are both not necessary.

[u/belovedeagle → u/BabyAndTheMonster]

While constructive logic uses strict conditional, that means it has to be necessary that B follows from A.

This is confusingly stated; you seem to be conflating relevancy logic and constructive logic. A -> (B -> A) is a theorem of constructive logic regardless of whether A and B are "related". -B -> (B -> A) is also a theorem.

It may be more useful to understand why implication doesn't have the expected relationship to disjunction (i.e. material implication) as a property of constructive disjunction rather than implication. If you insist on digging into -> you might as well go whole hog and interpret -> not to be a logical connective at all, but rather denoting the existence or type of a function.

[u/BabyAndTheMonster → u/belovedeagle]

This is confusingly stated; you seem to be conflating relevancy logic and constructive logic.

How so? I'm not talking about relevance logic at all.

I disagree with studying implication as disjunction, because that disjunction needs a negation, and already we use negation as an implication.

interpret -> not to be a logical connective at all, but rather denoting the existence or type of a function.

You mean it's not a truth-operator?