Re: intuitionistic vs. classical implication in Prolog code

It could be that your TNT translation
does something like MIR. But didn't spend
much time with your TNT yet.
Glivenko validity is basically induced by
classical double negation elimination:
(~(~A)) -> A
Your TNT would be this:
(~A -> (~(~A))) -> A
Which is close to MIR:
(~A -> A) -> A
Mild Shock schrieb:

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
>

>