Re: intuitionistic vs. classical implication in Prolog code

Glivenko is a basically RAA, reductio ad
absurdum shifted to the root. This is another
way to proof Glivenkos theorem.
I highly confused Joseph Vidal-Rosset on
SWI-Prolog discourse when I showed him
a intuitionistic prover that sometimes
also includes RAA, and then produces a classical
proof. RAA, reductio ad absurdum is this
inference rule:
    G, ~A |- f
   ------------- (RAA)
      G |- A
Compare this to Glivenko, basically double
negation elimiantion at the root:
         ???
   ---------------
      G |- ~(~A)
   --------------- (GLI)
      G |- A
But what happens above G |- ~(~A), i.e. the
???? . By Gentzen inversion lemma, above
G |- ~(~A) we must find, G, ~A |- f,
and we are back to RAA:
      G, ~A |- f
   --------------- (R->) Gentzen inversion lemma
      G |- ~(~A)
   --------------- (GLI)
      G |- A
So as much as Glivenko appears as a new alien
ivention, it has much to do with they age old
idea of "indirect proof".
Mild Shock schrieb:

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
 Which is a form of contraction. See also
 Lectures on the Curry-Howard Isomorphism
6.6 The pure impicational fragment
https://shop.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7   The reason is that if you add MIR to
intuitionistic logic you get classical logic.
MIR is a very funny inference rule,
 when you show it as an axiom schema:
 ((A -> f) -> A) -> A
 Its a specialization of Peirce Law.
 ((P -> Q) -> P) -> P
 Just set Q = f.
 Julio Di Egidio schrieb:

On 02/12/2024 09:31, Mild Shock wrote:
>

How does one usually demonstrate
Glivenkos theorem?

>
Usually with a semantics: we have already said that up-thread...
>
-Julio
>