[rottingtree]

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

[jfoutz]

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]

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]

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]

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.