>>14397463If you're aware of the split between classical and constructive mathematics, it can be summarized that constructive logic extends classical logic with a constructive disjunction and existential quantifier, for which excluded middle is not a law, but have more concrete meaning
This guarantees for an existential proof, you get a concrete example element. You can recover classical logic by double negation, i.e. ¬¬A, weaker than A. This breaks de Morgan duality, and is the price you pay for more meaningful (i.e., that postulates more from its interpretations) connectives
Linear logic further concretizes constructive logic
It is common knowledge in computer science, that constructive logic is equivalent to classical logic by what is called a continuation-passing-style (CPS) transformation, which is equivalent to double-negation-transformation, and that constructive logic corresponds to CPS terms in which continuations are passed linearly, that is they are used once and only once.
It turns out that what allows double negation in constructive logic to recover classical logic, is that these linearly-passed continuations are reified as constructive-logical objects that can be duplicated and discarded, and that that is the origin of non-constructivity in classical logic
So, constructive logic is plagued by a sort of dual non-constructivity, born from the unchecked duplicability of hypotheses (objects) in the logic, in that refutations are not constructive
Linear logic, by strictly controlling duplication and dismissal of hypotheses, not only recovers de Morgan duality, but also gives new concrete meaning to classical disjunction
Indeed, classical disjunction was only non-constructive insofar that you had to construct a candidate for each disjunct, depending on the falsity of the other disjunct. Thus, in order to use the hypothesis ¬A and derive a contradiction, you had to construct an A and only one A, therefore having an A, and viceversa, and that proves Av¬A
