Let's hope it spreads as well :p
138 karma · joined January 3, 2023
contradiction: a proof of ⊥. The definition of ⊥ does not matter (it just means false), thanks to the ex falso quodlibet principle.
A proof by contradiction: proving P by showing that (¬P -> ⊥).
Notice that I haven't defined the ¬ operator. This is due to the fact that its definition differs between classical logic and intuitionistic logic. Since the intuitionistic definition of ¬, i.e. "¬P" is a short-hand for "P -> ⊥", is classically equivalent to the definition of ¬ in the classical context (¬P is the statement "P does not hold"), it makes sense to adopt this definition. The astute reader will notice that, with this definition of ¬, a proof by contradiction is exactly a proof of ¬¬P, and it happens that ¬¬P -> P is an equivalent formulation of the excluded middle.
Now, back to Euclid's proof. Let P = "√2 is rational". We want to show Q = ¬P. We can do so by contradiction: assume ¬Q, and derive a contradiction. It *happens* that, when using the scheme of proof by contradiction on a property of the form ¬A, you can simply rearrange the negations to get rid of the use of the excluded middle.
So, going back to your statement,
>Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.
Well, whether Euclid's proof is intuitionistically valid is a question of point of view. Historically? I doubt it. I doubt that Euclid gave any kind of thought to whether he used the excluded middle, and probably used it pervasively, as all "classical" mathematicians today. However, I agree that it can be made intuitionistically valid using a purely syntactic rewriting. Said differently, Euclid's proof does not rely on the excluded middle. This does not mean you cannot use it because that's how you think or because you prefer it that way. When you see the blow-up of sizes of certain proofs in the non-classical context, you understand why many mathematicians would rather not give a thought to their use of the excluded middle. The same way many people in this thread used the PTA to show that √2 is irrational: that's overkill, but they prefer it that way !
To me, the only formal distinction you can make between the two lies in the use of the excluded middle. However, this distinction has not standardised in mathematics, as many mathematicians simply do not care for intuitionistic logic.
Such a mathematician could see the above proof as: I want to show ¬P by contradiction. Therefore I assume ¬(¬P) which is just P to me (the unintuitionistic mathematician has just used the excluded middle, without really caring). I derive a contradiction. Therefore ¬P holds.
While I personally enjoy the kind of subtleties that can be thought of about mathematical reasoning, I also think the rant-train on contradiction vs negation must stop. You are expecting a consensus from the wrong community.
A society where we have open, legal access to all the cultural pieces of the last century is very different from our own. And it seems difficult to know how it would affect both the consumption, but also the creation of media.
Sometimes, when I argue about this IRL, I'm told that we are practically there because of piracy. But this is a debate of tech enthusiasts, we know how to download, we now how not to get caught. The majority does not