4 ms·

> Constructionism is based on the fact that every proof is a construction, which corresponds to a program I don't think this is correct, even in constructive l

> Constructionism is based on the fact that every proof is a construction, which corresponds to a program I don't think this is correct, even in constructive logic. Negative statements do not correspond to a construction, and in fact are the only statements in constructive logic that may be proven "by contradiction". But this means that every statement of non-constructive logic can be understood "constructively", if in a rather trivial sense, as a negative statement. Linear logics may be a good way of exploring these issues in depth, since these allow for explicit "constructions" while preserving the sort of 'duality of negation' (i.e. flipping the direction of implications, or exchanging conjunctions w/ disjunctions) that's quite familiar within classical logic. Somewhat relatedly, there's also an interesting question of how much "construction" really is involved in typical constructive proofs, and whether that can be cleanly separated out from the more purely "logical" parts of the proof.

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 ago
  Intuitionistic 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.)

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 ago
Intuitionistic 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.)