5 ms·

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

• rottingtree 10y ago
  The mathematicians using intuitionistic logic usually call themselves "computer scientists" or even just "programmers."
  • jfoutz 10y ago
    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?
    • ajarmst 10y ago
      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.
      • jfoutz 10y ago
        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.
        • ajarmst 10y ago
          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.
      • deleted 10y ago
        [deleted]
• tel 10y ago
  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.