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