Re: intuitionistic vs. classical implication in Prolog code

On 03/12/2024 00:26, Mild Shock wrote:

Its actually easier, you don't need to go
semantical. You need only to show that
Consequentia mirabilis aka Calvius Law
 becomes admissible as an inference rule:
      G, ~A |- A
    ---------------- (MIR)
        G |- A
https://de.wikipedia.org/wiki/Consequentia_mirabilis

(I have too many links already, and you can't even be bothered to link to articles in English?)
DNE and equivalent is not provable in any intuitionistic logic.  So, what does it even mean to prove it "admissible" here?  In the object theory?  Under TNT itself??

Which is a form of contraction.

Which is not allowed in a linear or affine logic.
Also, with reference to another comment of yours: my rules are "directed", and that is a feature... as I have read somewhere.
-Julio