Re: intuitionistic vs. classical implication in Prolog code

On 12/02/2024 03:54 PM, Mild Shock wrote:

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
>

>

>

>

Yeah I suppose that's "e-lie-mentiens".
"You need to not go semantical
or rather that's what I need ..."
When you say "classical" logic,
and that means "quasi-modal" logic,
it's not modal any-more.
Suppose someone takes your argument,
hides it behind a screen, and says
they changed one stipulation which
you'd agree would have no material
bearing. Would you be willing to
accept it?
What if it's that you do or don't?
See, modality is relevant and
"quasi-modal" is for some, _un_-classical,
and where the classical _always_
includes _all_ of De Morgan's laws.
(And any of Chrysippus' relevant moods.)