Path: ...!news.mixmin.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: =?UTF-8?Q?I_am_busy_with_other_stuff_=28Was:_can_=ce=bb-prolog_do_i?=
 =?UTF-8?B?dD8p?=
Date: Sun, 1 Dec 2024 15:32:43 +0100
Message-ID: <vihs2a$lt4v$2@solani.org>
References: <vhgdq0$19evr$1@dont-email.me> <vhgemi$ca9e$1@solani.org>
 <vhgg23$19evr$2@dont-email.me> <vhhsit$d108$1@solani.org>
 <vhhuuf$1qic1$1@dont-email.me> <vhi5ch$d5rb$1@solani.org>
 <vhqemf$16mc2$1@dont-email.me> <vi8bgs$42ft$1@solani.org>
 <vihp9r$2eqeg$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 Dec 2024 14:32:42 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="717983"; 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:hjs4niWKA/GQTzUI2LzeayZnj9Y=
X-User-ID: eJwNyMERACEIA8CWDohBykGN/Zdwzv52BI07wUGM+3BOXwHkZYhMm+7VrTdwE/qcZZDqorZF+QnXt1VJfb1+LTYVDw==
In-Reply-To: <vihp9r$2eqeg$2@dont-email.me>
Bytes: 2383
Lines: 47


I am busy with other stuff. I have
decided to postpone logic for a while.

So although it was very temping to download
you software, and then replace these line:

notation(dnt(X), ~X->(~(~X)))
solve_t__sel(neg, C=>X) :-
    solve(C=>dnt(X)).

https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11

By these line:

notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
    solve(C=>gliv(X)).

I am afraid I have no time for that. You
could do it by yourself. Or what

until somebody else does it. What will be
the results?

Julio Di Egidio schrieb:
> On 28/11/2024 00:55, Mild Shock wrote:
>> This is Peirce law:
>>
>> ((p->q)->p)->p
>> Peirce law is not provable in minimal logic.
>>
>> But I guess this is not Glivenko:
>> notation(dnt(X), ~X->(~(~X)))
>>
>> https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic 
>>
>>
>> Glivenko would be simply:
>> notation(gliv(X), (~(~X)))
>>
> 
> We have gone over that already.  Either you have memory problems or you 
> are purposely flooding the channel at this point.
> 
> -Julio
>