Timeline for Intuitionistic logic as quantization of classical logic?
Current License: CC BY-SA 3.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 25, 2013 at 16:09 | comment | added | Paul Taylor | Margaret, I was trying hard not to preach to the choir, but I look forward to hearing from you. | |
| Apr 25, 2013 at 15:47 | comment | added | Margaret Friedland | @Paul: Since this is Mikhail Katz's question, and the discussion is developing between the two of us, I agree it is better to move it to email (I will write you). Anyway, it seems you are preaching to the choir (I did not downvote). | |
| Apr 25, 2013 at 14:53 | comment | added | Paul Taylor | Margaret, before I rewrote my answer it occurred to me that you were its intended audience, so I tried unsuccessfully to find an email address for you so that I could discuss it with you. I was trying to explain that I use intuitionistic logic on a day-to-day basis where you use classical, just as I use pounds where you use dollars. I was also trying to explain the things that computer science students learn and which are needed as background for Dan's answer. However, it seems that this has earned me down-votes. | |
| Apr 25, 2013 at 14:42 | comment | added | Margaret Friedland | Here is a concrete model (due to Tarski?): variables=OPEN subsets of Euclidean plane, partially ordered by inclusion; alternative= standard union; negation=interior of the complement. A formula is true (resp. false) if it corresponds to the whole plane (resp. empty set). | |
| Apr 25, 2013 at 14:32 | comment | added | Margaret Friedland | @Paul: it is possible to formulate classical propositional logic so that the only deduction rule is modus ponens, and excluded middle and double negation appear as axioms (I am not talking about first-order logic here). These propositions are not axioms in intuitionistic logic, and are not provable there. I do not see anything misleading in using semantics, especially knowing that both calculi are complete. In a nice model of intuitionistic logic, one can see that excluded middle is not true, but also that it is not false. | |
| Apr 25, 2013 at 12:19 | history | edited | Paul Taylor | CC BY-SA 3.0 |
more complete story
|
| Apr 24, 2013 at 18:36 | comment | added | Asaf Karagila♦ | Etienne Matheron, I knew that someone would write that. When cooking there is some amount of salt required for the chemical process to go through properly, but beyond that point it becomes a flavor issue. I clearly meant that the chemical requirement has been matched, and now we add it for benefit of our taste. But yes, the flavor that you can end up with added some spices during the preparation vs. after is there. For some it's better and for some it's worse (some = some people, and some spices). | |
| Apr 24, 2013 at 17:47 | comment | added | Etienne | @Margaret and Asaf : quite often, the food is much better if you add the salt while cooking. Just think about the water of the spaghetti! | |
| Apr 23, 2013 at 19:18 | comment | added | Ryan Reich | Okay, one more comment. The activity you say classical mathematicians refuse to acknowledge is what I mean by identifying what we find important: suppose we tried to prove the existence of bases constructively. We'd find we need something to work with, and that would lead us to finitely-generated vector spaces, where the theorem is constructed. We might then ask "so what are infinite-dimensional vector spaces?" and in learning the difference, decide whether the concept is fundamentally cool or merely abstract nonsense. I posit that no one works in a field they honestly think is the latter. | |
| Apr 23, 2013 at 19:10 | comment | added | Ryan Reich | @Paul: It's just a philosophical observation. Non-commutative algebra differs from commutative by rejecting certain constraints on the structure of the theory. Some reject non-commutative rings since comm. rings have a geometric side, as per their personal mathematics. Likewise some reject non-associative "groups" because of the rep.-theoretic connection to regular groups. Some (you?) specialize in constructivizing classical results. Non-EM math has a constraint: directness; and a connection: plausible intuition. Thus, it is like commutative algebra. | |
| Apr 23, 2013 at 19:06 | comment | added | Paul Taylor | Margaret, a good concrete counterexample (ie a detailed example of A and not B) is a fine thing, as Imre Lakatos illustrated in Proofs and Refutations. On the other hand, proof by contradiction uses putative counterexamples. I can see that doing this is heuristically very useful: if we had something that satisfied all of the hypotheses of our conjecture, but failed the conclusion, what would it have to look like? Constructive mathematics does not regard such arguments as wrong, just as drafts of the ultimate constructive proof. | |
| Apr 23, 2013 at 19:00 | comment | added | Paul Taylor | Ryan, it would be interesting if you could find some way of substantiating your last sentence (or on the other hand if someone could give a positive answer to the original question). | |
| Apr 23, 2013 at 18:53 | comment | added | Paul Taylor | I am glad to hear that Asaf avoids arguments by contradiction wherever possible, even in a classical setting. That is part of the hygiene of writing clear proofs. Unfortunately, many mathematicians routinely start an argument by saying "suppose not", as in "are you calling me a liar?". | |
| Apr 23, 2013 at 18:50 | comment | added | Ryan Reich | Of course, the proof style " Thm: P; Proof: Suppose $\lnot P$; proves P ; Contradiction" is inane and stems from laziness. And the prevalence of EM obscures the constructive truth of those propositions that may be demonstrated as in Bishop-Bridges. Because of it we may miss that some non-constructive theorems (existence of bases) have constructive weakenings (when finitely generated). Analyzing the difference helps identify what we find important in our personal math; perhaps non-constructive math is the real analogy to non-commutative algebra, not the reverse. | |
| Apr 23, 2013 at 17:56 | comment | added | Margaret Friedland | As a classically trained mathematician, I like a good counterexample now and then. But as an occasional cook, I can attest it is more complicated to remove the salt that was added during cooking :) – Margaret Friedland 0 secs ago | |
| Apr 23, 2013 at 17:53 | comment | added | Asaf Karagila♦ | Luckily, not everyone who is not a constructivist insists on doing everything by contradiction. Mathematicians are lazy by nature, and if a direct proof is easier and more natural there is no need to insist on going backwards. I don't recall any of my teachers doing something like that, except in cases where they missed the direct way when preparing the lecture for one reason or another. In which case insisting may or may not would have helped them. As for the swimming analogy, I suppose it shows I didn't quite get it. | |
| Apr 23, 2013 at 17:39 | comment | added | Paul Taylor | What you say about your nephews fits with what I wrote. The proof is backwards (CBA) as I explained. If this is part of a bigger proof that naturally goes in a particular order (unfortunately I didn't allow myself enough space in the alphabet) then presenting some of it in a contradictory way spoils that natural order. | |
| Apr 23, 2013 at 16:44 | comment | added | Asaf Karagila♦ | I don't see the comparison between 'fear of water' and LEM. Furthermore, observing my nephews I can witness that infants can swim instinctively during their first couple of months, but then they don't have this ability anymore and they need to relearn it. This regardless to whether or not they were introduced to the pool as little kids. I also don't understand why working backwards by contradiction is more complicated. Does adding salt to your food after it was cooked more complicated than adding it while cooking it? | |
| Apr 23, 2013 at 15:03 | comment | added | Paul Taylor | It was a reference to the discussion on another question in which someone claimed authority on the grounds of having won a gold medal in the International Mathematical Olympiad. My point is that the IMO is about problems that are technically difficult but depend only on school maths and therefore no conceptual or philosophical consideration. | |
| Apr 23, 2013 at 14:43 | comment | added | Michael Bächtold | @katz: probably imo-official.org | |
| Apr 23, 2013 at 14:02 | history | answered | Paul Taylor | CC BY-SA 3.0 |