12 ms·
Proof of negation and proof by contradiction (2010)
- Kenji 10y agoI 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.
- aisofteng 10y ago>very very deep level It's not a deep level at all.
- Kenji 10y agoIf you write a paper that contains mathematical proofs, it is extremely unlikely that this distinction will play any role whatsoever.
- rocqua 10y agoConstructive 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.
- tel 10y agoFor 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.
- rocqua 10y agoWhat 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.
- tel 10y agoDefinitely, 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.
- pflats 10y agoIt'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.
- mcguire 10y agoThe 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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [2] https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic [3] https://en.wikipedia.org/wiki/Natural_deduction 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 https://en.wikipedia.org/wiki/Closed-world_assumption
- tel 10y ago"... 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.
- maweki 10y agoOne shouldn't take the rule of the excluded middle for granted. That is not applicable in many theories.
- naasking 10y agoExactly, OP doesn't seem to understand that classical logic is the only logic out there.
- The_suffocated 10y agoWould you please elaborate? I think almost all mathematicians use classical logic rather than intuitionistic logic.
- rottingtree 10y agoThe mathematicians using intuitionistic logic usually call themselves "computer scientists" or even just "programmers."
- jfoutz 10y agoAnd 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?
- ajarmst 10y agoBut 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.
- jfoutz 10y ago
- deleted 10y ago[deleted]
- rocqua 10y agoThere 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.
- ajarmst 10y agoI don't get it. Do they feel that ¬¬ϕ = ϕ is invalid or contingent? Or is it just a matter of taste?
- ajarmst 10y agoReplying 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.
- tel 10y agoThey 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.
- kmill 10y agoYes, 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.
- tel 10y agoFwiw, 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%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
- vilhelm_s 10y agoSo 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-constructive-mathematics/ http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...
- glomph 10y agoThis was a lot more informative / interesting to me! I didn't really get the motivation at all reading just the blog post.
- mafribe 10y agoIf 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.
- tel 10y agoQuite 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.
- ajarmst 10y agoI 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.
- chaoxu 10y ago"intuitionistically" refers to the intuitionistic logic.
- mcguire 10y agoWhich is one of the reasons I prefer the term "constructive logic"; "intuitionistic" doesn't tell me anything.
- tel 10y agoIntuitionistic logic is a subtype of constructive logic, though, so it's more specific. That said, a lot of people don't make the distinction!
- ajarmst 10y agoAh, 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).
- throwaway729 10y agoIntuitionism is a philosophy of mathematics that is deeply related to but not the same thing as constructivism.
- tel 10y ago"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".