43 ms·
You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.
by naasking 2y ago
You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.
- zozbot234 2y agoIntuitionistic logic also allows for negative statements, which then are entirely non-constructive. From a proofs-as-programs POV, this is just the observation that a proof is not just a program, but rather a program plus an explanation of why that program works correctly within its constraints, e.g. why it never ever tries to divide by zero. (This can be rephrased by saying that the program is both requesting and providing abstract "capabilities", i.e. information-free tokens, to its environment. Classical logic is then the logic of these capabilities, in the sense that providing a weak capability as output is essentially the same as asking for a strong capability from your environment as input.)