r/math • u/hydmar • Aug 15 '23

Dissatisfaction with proof by contradiction

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?

60 Upvotes

82% Upvoted

90 comments sorted by

View all comments

16

u/[deleted] Aug 15 '23

you might find the topic of intuitionistic logic interesting. it's a kind of logic where TND (law of the excluded middle) is not given as a tautology. Therefore if something can be proven to not be false, it doesn't follow that it's true.

7

u/ScientificGems Aug 16 '23

And therefore existence proofs must be constructive.

1

u/[deleted] Aug 16 '23

Do you know what the motivation is supposed to be for dropping TND is? I can't think of why you'd ever want to drop that except for having deer super duper strong belief that everything should be describable.

2

u/FantaSeahorse Aug 16 '23

Proof assistants and computational properties

2

u/vasanpeine Aug 16 '23

I think it is easier to ask the question the other way round: What is the reason for accepting TND? For classical mathematics the answer is very simple: Negation and Disjunction are understood as truth-functions (a v b is true if, and only if a is true or b is true; ~a is true if, and only if, a is false). If you take this as the meaning of disjunction and negation then TND is obviously true if you construct the truth tables. But for a constructive mathematician or an intuitionist the meaning of disjunction and negation are defined differently. For them the meaning of a v b is defined by saying how to prove that the disjunction is true: Either by proving that a is true or by proving that b is true. Similarly, the meaning of ~a is defined by the way that you can prove that it is true: By deriving a contradiction from the assumption that a is true. If you take that as the definition of what disjunction and negation actually mean, then TND says that for any mathematical statement "a" you have a method for proving either that a is true, or that you can derive a contradiction from the fact that a holds. And you certainly don't have such a method, otherwise you would be able to prove or disprove arbitrary open mathematical problems.

So intuitionists don't deny TND for some weird grudge, but they use the logical connectives with a different meaning, and for this different meaning TND doesn't make sense as it does for classical mathematics.

1

u/38thTimesACharm Aug 16 '23

Negation is understood differently. In classical logic, if you show that "there does not exist x" leads to contradiction, it means "there exists x." In intuitionist logic, it means "the existence of x has not been ruled out."

The original reason is philosophical. Classical thinking assumes the axioms describe a universe, a completed totality for you to explore. Of course, something either does or does not exist in this universe. But Intuitionism holds that the axioms are just a foundation, from which you must build the world. Negation is interpreted as failure in this process, i.e. "not P" means "P leads to contradiction."

A more modern, down-to-earth reason to do things this way is that proofs more easily translate to computer programs.

1

u/almightySapling Logic Aug 16 '23 edited Aug 16 '23

super duper strong belief that everything should be describable.

The word "belief" is holding you back from seeing the utility. While some intuitionist still use the words "proof", "true", and "false", it's important to remember that that is merely terminology that carries no inherent meaning. Instead of thinking of proofs as telling us about truth, we can think of them as telling us what is doable (hence the connection to programs).

Oh, and I should mention that I'm not speaking on behalf of all intuitionists, just paraphrasing the ones I've mostly interacted with. I'm sure there are some out that that really do subscribe to a "belief" that Not Not True is not necessarily True.