Deutsch   English   Français   Italiano  
<vimpql$vkn$1@dont-email.me>

View for Bookmarking (what is this?)
Look up another Usenet article

Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Still on negative translation for substructural logics
Date: Tue, 3 Dec 2024 12:25:09 +0100
Organization: A noiseless patient Spider
Lines: 19
Message-ID: <vimpql$vkn$1@dont-email.me>
References: <vihumn$2eqeg$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 03 Dec 2024 12:25:10 +0100 (CET)
Injection-Info: dont-email.me; posting-host="908b13ceb23b80a0fcd06b4db7988bd6";
	logging-data="32407"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19wI8AvJbNTBsnTHUOcqaN8GNHapmGlL+E="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:U1EylYU+wP/m03eZsi1LF6WGviU=
Content-Language: en-GB
In-Reply-To: <vihumn$2eqeg$3@dont-email.me>
Bytes: 1599

On 01/12/2024 16:17, Julio Di Egidio wrote:

> Here is an interesting new case, which I had thought should be 
> *unsolvable*:
> 
> ```
> ?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !.  % DNE<->LEM
> ```
<snip>
> Yet with my `dnt`, my solver proves even that one (but I still have to 
> inspect the proof tree, what I actually get).  Indeed, I am rather 
> worried that it just solves everything I throw at it, though not the 
> falsities...

I am an idiot: that statement is not true intuitionistically, but it is 
true classically, so in fact nothing strange there.

-Julio