Re: intuitionistic vs. classical implication in Prolog code

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