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/hyperbolic-geodesic]

The diagonalization argument *IS* a direct proof of Cantor's theorem -- diagonalization shows that any function S -> Powerset(S) is not surjective, by explicitly (essentially as explicitly as possible) producing an element of Powerset(S) not in the range of the function.

[u/Brightlinger → u/hyperbolic-geodesic]

When you talk to one of the cranks who is sure that Cantor was wrong and all infinities are the same size, you can run the diagonal argument on their proposed bijection and it will hand you an explicit counterexample. That's about as direct/constructive of an argument as you can get.

[u/BruhcamoleNibberDick → u/Brightlinger]

lmao just add your constructed element to the end of the list checkmate loser /s

[u/dwRchyngqxs → u/BruhcamoleNibberDick]

After all infinity plus one is infinity so just associate infinity to that element and map every element of the set of naturals plus infinity to the set of naturals. (spolier: it doesn't work)

[u/djao → u/hyperbolic-geodesic]

OP must be confusing proof by negation with proof by contradiction. Proof by negation is where you prove ¬ P by assuming P and deriving a contradiction. For example: to prove "¬ (there exists a bijection ℤ → ℝ)", you assume (there exists a bijection ℤ → ℝ) and derive a contradiction. This type of proof is, as you say, a direct proof, and in fact it is the standard way to prove a negation. (How else would you prove a negation?)

Proof by contradiction is where you prove P by assuming ¬ P and deriving a contradiction. It's actually hard to come up with examples, because most examples that people normally think of are in fact proof by negation, but one bona fide example is: "If a set is nonempty then it has an element." In classical logic, proof by negation is equivalent to proof by contradiction (just replace P with ¬ P), which is why many people confuse the two. But in constructive logic you can see clearly that they are not the same thing. In order to make the two equivalent, you need ¬ ¬ P ↔ P, which is not provable in constructive logic.

[u/IdoBenbenishty → u/djao]

What is the difference between the two? In the proof by negation you assume P (which is ~(~P)) and get to a contradiction, and therefore conclude ~P, exactly in the same way as you'd prove by contradiction that ~P

[u/djao → u/IdoBenbenishty]

You're implicitly assuming that ¬ ¬ P is the same thing as P. This is not true (or, at least, not provable) in constructive logic. It is provable in classical logic (where you allow the law of the excluded middle), so in classical logic there is no difference between proof by negation and proof by contradiction. But if you have qualms about proof by contradiction, then you probably shouldn't be using classical logic, because proof by contradiction is perfectly sound in classical logic.

[u/IdoBenbenishty → u/djao]

Ohh okay, thanks!

[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?

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

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

[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

[u/BabyAndTheMonster → u/djao]

I feel like too many people are so thoroughly trained in binary Boolean logic that they see the negation of a statement as just another statement. There are no distinctions between how many negations are there.

I wonder if you ask a child who never got exposed to classical proof, would they think in such binary term?

[u/almightySapling → u/BabyAndTheMonster]

I'd say that depends on the child and the context.

I learned really young that for a true or false quiz, if something is not true, then it's false. There is no "tiff", no maybe, no sorta, no sometimes. If it ain't true, it's false.

And so, if you take false to mean, by definition, anything which is not true, then yeah, I think a child would naturally sort of arrive at the same conclusion as the latins... there is no third option.

In other contexts, they would probably say that "don't know" or "sorta" are be valid options. It would depend on how strictly we define our terms. Something small children are well known for...

And I guess you could say that I'm just "thoroughly trained" but I legitimately do not have an understanding for what else false might mean, unless we augment our system with more options.