Proof of negation and proof by contradiction (2010) | Hacker News Reader

Proof of negation and proof by contradiction (2010)

math.andrej.com

40 pointsslbenfica37 comments

I kept getting pushed out of flow by words like "intuitionistically" and constructions like "derive absurdity" (as opposed to 'derive an absurd conclusion'). 'Intuitive' is a perfectly functional word, no need to make new ones up to sound formal.

"intuitionistically" refers to the intuitionistic logic.

Which is one of the reasons I prefer the term "constructive logic"; "intuitionistic" doesn't tell me anything.

Intuitionistic logic is a subtype of constructive logic, though, so it's more specific. That said, a lot of people don't make the distinction!

Ah, not the author's fault then. Just unnecessarily opague terminology in the canon. I'll redirect my irritation to his predecessors (Constructive Logic seems a much better term that doesn't do any violence to the rules of English).

Intuitionism is a philosophy of mathematics that is deeply related to but not the same thing as constructivism.

"Derive absurdity" comes from the fact that in these logics there is only one statement which is "Absurdity"—capitalized perhaps. It's a unique thing to talk about and "an absurd conclusion" is actually shorthand for "a statement from which you could derive Absurdity".

I read it, but I still don't comprehend why anyone would stress the difference between

To prove ¬ϕ, assume ϕ and derive absurdity.

and

To prove ϕ, assume ¬ϕ and derive absurdity.

It just seems exactly the same, given that ¬¬ϕ = ϕ.

"Yes indeed, but the cancellation of double negation is precisely the reasoning principle we are trying to get."

You have to go to a very very deep level of maths if this is what you want to get.

>very very deep level

It's not a deep level at all.

If you write a paper that contains mathematical proofs, it is extremely unlikely that this distinction will play any role whatsoever.

Constructive proofs are better in the sense that they explain how a thing is true.

Consider the intermediate value theorem. The normal proof is by contradiction. However, it doesn't tell you anything about where the intermediate value is reached. One can constructively proof the theorem by bisection. This proof has the added benefit of showing you how to compute where the intermediate value is reached. Or rather, it shows that you can compute the intermediate value.

Meanwhile, the proof by contradiction doesn't tell us if we can ever compute where the intermediate value is reached. Having made the switch to CS from maths, it has struck me how useless some theorems proven by contradiction are.

You can view the issue as viewing math as truth finding in a world of platonic ideals, or math as a the study of computation.

For finite proofs, proof by contradiction can be interpreted as continuation passing and then results in an algorithm. On the other hand, this algorithm may be no better than exhaustive search.

What do you mean by 'finite proofs'?

In cases where the set of all possible examples is finite, I can see this trick working. Maybe a similar approach still works when all possible examples are enumerable or even recursively enumerable.

None of these hold for the intermediate value theorem on the real number line though.

Definitely, it's super weak but at the same time constructive. The issue is that it essentially ends up becoming a search algorithm where contradiction is backtracking. If the search algorithm doesn't stumble upon the solution (at least in principle) in finite time then it's a bit tough to consider it constructive.

It's not as helpful, but I like to teach my high school students: Say you're planning to rob a jewelry store. You can rob it constructively or by contradiction.

You could case the joint, figure out the guards and the employees, their schedules, their uniforms, the jewels on display, the layout of the place, and so on. You can make a plan, an appropriate scenario, disguises, make a copy of keys, some costume jewelry, some fake uniforms. Really know the place inside and out, Oceans-11 the whole thing. And if you do it right, you can make it out with the jewels before anyone even knows they were stolen.

Or you can get some masks and some baseball bats, steal a semi truck, and drive it through the front window of the jewelry store. If the jewel cases aren't open from the impact, or if someone gets in your way, well, refer back to the baseball bats.

Both accomplish what you set out to do, but the first is clearly more elegant and often takes more work and study, requiring/granting a greater understanding of the system. And future thieves would learn a lot more studying Danny Ocean than they would Johnny Smash-and-Grab.

The Curry-Howard isomorphism[1] is usually described as a correspondence between computer programs and mathematical proofs. What they usually mean, but don't usually say, is that the actual correspondence is between computer programs and proofs in intuitionistic or constructive logic[2]. (Natural deduction is a lovely example[3].) The important difference between constructive and "classical" logic is that in the former you cannot use the law of the excluded middle or double-negation-elimination.

One way this difference shows itself is in proofs of existence: rather than just demonstrating that something exists (by virtue of it not-not-existing), you have to create an example of it. This is similar to a program, where you cannot demonstrate that 2+2 has some value and then print "4"; instead you have to calculate 4 before you can print it.

Another weird place it shows up[4] is in Prolog, which uses classical first order logic by the closed-world assumption[5]: anything you cannot prove is false.

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[2] https://en.wikipedia.org/wiki/Intuitionistic_logic

[3] https://en.wikipedia.org/wiki/Natural_deduction

[4] At least I thought so, one morning in the shower.

[5] https://en.wikipedia.org/wiki/Closed-world_assumption

"... in many practical branches of pure and applied mathematics"

On the other hand, there have been many mathematical papers written there this distinction was key. It all depends upon your topic, really, and how many times you have to invoke the hobgoblins of mathematical foundations.

One shouldn't take the rule of the excluded middle for granted. That is not applicable in many theories.

Exactly, OP doesn't seem to understand that classical logic is the only logic out there.

Would you please elaborate? I think almost all mathematicians use classical logic rather than intuitionistic logic.

The mathematicians using intuitionistic logic usually call themselves "computer scientists" or even just "programmers."

And the common example

    int a = 5;
    a = !!a;
    printf("%i", a); // -> 1

my handwavy approach, negation is either information preserving, or not. If operations destroy data, you have to be extra careful. I think classical logic runs into some subtlety switching from reals to integers and back to reals - how are you rounding or truncating those values?

But surely no one believes that that particular case says anything about logical negation? It depends on the convention that "if it's not 0, it's true", which isn't even true of many computer languages, much less systems of formal logic. E.g. 5 == True is, in most systems, an absurdity not a axiom.

Well, you can set up whatever goofy rules you want. I'd expect !!a to be back to 5, not true.

Information erasure is a handy thing to keep track of.

Yeah, but the information erasure didn't happen when you applied double negation. It happened when you accepted a surjective convention where 5 mapped to True (and so did every non-zero value). The erasure wasn't accidental---it was a feature of the axiom set you chose. You can't complain that a system of logic is behaving the way you specified it should behave. If you apply --a, you don't lose any information because now you've applied a different axiom set: one that is algebraic and bijective.

At a very broad philosophical level---which is something one must assume if you're going to talk foundations of mathematics---"formalistic" logic makes a really unbelievable assumption:

All facts are either true or false.

Gödel of course blew this idea up quite elegantly, but the thrust of the idea is encoded directly into classical logic: (P \/ not P) is saying exactly that.

Intuitionistic logic is a development of constructive logic which takes seriously the idea that many statements are at least presently unknown and possibly unknowble. Taking this very seriously we find that we cannot even use three-valued logic like "True | False | Uncertain", but instead require a logical valuation with infinitely many states.

In practice, it's super convenient to use classical logic. You can use proof by contradiction, e.g. On the other hand, you have to deal with some idealogical uneasiness when you think really hard about graphs, real numbers, or the Axiom of Choice. In practice, we cannot imagine the world bereft of some of the theorems which require these uneasy choices. Simultaneously, AoC, for instance, allows bizarre obviously alien results like Banach-Tarski.

Constructive logics and especially intuitionistic logics are an attempt to get past this and use a language which has the same force without the aliens and misfits. Unfortunately, the result is something that is more complex to wield.

There is an entire movement within maths called 'intuitonist logic' that does not want to use ¬¬ϕ = ϕ.

The point behind it is to only use 'constructive' proofs. Or rather, to avoid proofs that show a counter-example is impossible.

I don't get it. Do they feel that ¬¬ϕ = ϕ is invalid or contingent? Or is it just a matter of taste?

Replying to myself. Roqua has a nice description of the motivation elsewhere in this thread, with regard to how a constructive proof can offer more insight into the thing being proven than a mere 'yes, it's true'. I can see their point.

They feel that there are some sorts of statements ϕ for which ¬¬ϕ = ϕ is invalid. Or, more interestingly, that if we force it to be such that all statements have that property then we lose the ability to talk about certain interesting things where it is not available.

Yes, they are the same assuming ¬¬ϕ = ϕ. But, one interpretation of mathematical truth is something like this:

1. A proposition is the name of a set/type whose elements are proofs of the proposition.

2. A proposition is provable if its set/type is nonempty/inhabited.

3. Implication can be modeled as a function space X → Y. There is some restriction on the kinds of functions allowed, but "continuous" seems to be kind of the idea, in particular only compositions of known continuous functions.

4. The set for "contradiction" is ⊥, which ought to be empty.

5. For negation, we take ¬ϕ to mean ϕ → ⊥, that is, with the truth of ϕ we may construct a contradiction.

6. It is not hard to prove that ϕ → ¬¬ϕ, which is ϕ → ((ϕ → ⊥) → ⊥). In fact, rewriting this as ϕ → (ϕ → ⊥) → ⊥, we can just use "flip ($)" in Haskell, so to speak.

7. But, ¬¬ϕ → ϕ can't be proved directly. The double negation (ϕ → ⊥) → ⊥ as a function space is empty if ϕ is false and has exactly one element if ϕ is provable, so ¬¬ϕ → ϕ would mean that if ϕ is not false then one could obtain one of the proofs of ϕ. You can prove ¬¬(¬¬ϕ → ϕ) directly, though. ("It is not false that ϕ follows from ϕ being not false.")

7.5. I personally find that it is easier to think of ⊥ as an indeterminate set you don't know the elements of rather than just assuming it is empty, for the purpose of understanding the function space interpretation of implication.

8. If you care about classical logic, you can prove that double negation is a monad. It actually turns out that ¬¬¬¬ϕ → ¬¬ϕ, so you only ever need to have a single level of double negation. Double negation from the point of view of function spaces takes empty/nonempty sets to empty/singleton sets.

Here's an answer to why stress the difference: sometimes you want to know if the best you can say about a proposition is that it isn't false. That way, you know whether its proof suggests an algorithm for calculating whatever the theorem was about. But if you don't care about the difference, then you can stay inside the double negation monad to get classical logic.

As an aside, one of my greatest embarrassments as a computer scientist is that I never memorized the Greek alphabet. Instead, when I run across a Greek letter that I don't immediately recognize, like ϕ, I call it "smegma".

I'm not sure how this information is supposed to help you, but I hope it improves your life somehow.

Fwiw, this is called the BHK or Brouwer–Heyting–Kolmogorov interpretation. It's a way of providing a model of intuitionistic logic in the same way that "sets" provide a model of classical logic. Intuitionistic logic this should hold some kind of meaning independent of BHK, but BHK can help in your examination of Intuitionistic logic.

https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...

So if you want a more general motivation for constructive mathematics, I recommend another paper by Andrej Bauer: Five stages of accepting constructive mathematics.

http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...

This was a lot more informative / interesting to me! I didn't really get the motivation at all reading just the blog post.

If you use ¬¬ϕ = ϕ in your proof, you loose constructivity.

Why would you care about this?

Simplifying a bit, in a constructive proof, every existential statement ∃x.ϕ comes with a witness c such that ϕ is true when x is replaced by c. Likewise, in a logical disjunction ϕ \/ Ψ comes with information whether ϕ is true or Ψ.

If your proof is not constructive, you may not be able to get this information from the proof. In other words, a constructive proof is nicer than a non-constructive proof.

OTOH, non-constructive proofs tend to be easier to find, indeed some theorems have only non-constructive proofs. Moreover, non-constructive can sometimes be shorter than constructive proofs of the same statement.

Quite apart from the proof theoretic advantages others have mentioned, it's sort of a big leap of faith to believe LEM = (for all propositions P, P or not P).

For instance, the continuum hypothesis: unproven and still controversial. We can state it in whatever ambient logic, say ZFC, you like, but then it's independent. It therefore flies directly in the face of LEM. We have to work metamathematically to even survive such a blow (as Gödel already began the trend of, ruining Hilbert's Formalist hopes).

As it turns out, we're generally quite fine exploring the consequences of logical systems even when they're flawed. It's still interesting, pays the bills, and is generally helpful. Some things might be shown "false" by some stickler's particulars of what truth means while others need modification to satisfy everyone, but we're still doing the right things "usually".

But it's still a really good question Hilbert posed: what is the ultimate underlying language that we're using to discuss and drive the mechanism of mathematics? For that, you really have to look critically at things like LEM.

Reply on news.ycombinator.com