Path: ...!npeer.as286.net!npeer-ng0.as286.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: intuitionistic vs. classical implication in Prolog code
Date: Tue, 3 Dec 2024 00:33:07 +0100
Message-ID: <vilg3i$b8ch$1@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vihvl9$9568$1@solani.org>
 <vii0l0$m02t$1@solani.org> <vii1jv$2eqeg$4@dont-email.me>
 <vii2qb$97ao$1@solani.org> <vii9vv$2eqeg$5@dont-email.me>
 <vijpj3$a69e$2@solani.org> <vijr25$a72h$1@solani.org>
 <vijr94$a72h$2@solani.org> <vik7bi$39c73$2@dont-email.me>
 <vilfmi$b855$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 Dec 2024 23:33:06 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="369041"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:OqY8TH8aYp1SofiWZAGk8/4jsLc=
In-Reply-To: <vilfmi$b855$1@solani.org>
X-User-ID: eJwFwQkBACAIA8BKUx4lDgzpH8E7E1/Oo26uNjYeT0mIxO5Cg5fribGmA36izAVMam6pwTU0ta/MZmJNfl2jFgY=
Bytes: 3412
Lines: 85

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
>>
>