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: Counter Example by Troelstra & Schwichtenberg (Was: Still on
 negative translation for substructural logics)
Date: Wed, 4 Dec 2024 10:43:52 +0100
Organization: A noiseless patient Spider
Lines: 16
Message-ID: <vip88o$p469$1@dont-email.me>
References: <vihumn$2eqeg$3@dont-email.me> <vip1eu$pniu$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 04 Dec 2024 10:43:53 +0100 (CET)
Injection-Info: dont-email.me; posting-host="610effb79350f409cea8729717185534";
	logging-data="823497"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+8zULNn/KQz4QRutvjcQsFrrs0ytUbKgI="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:fbDbpNnMYs9ZUSgCX095TKTssm4=
In-Reply-To: <vip1eu$pniu$1@solani.org>
Content-Language: en-GB
Bytes: 1617

On 04/12/2024 08:47, Mild Shock wrote:

> Now I tried an example by Troelstra & Schwichtenberg:
> 
> solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
> solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
> 
> At least the second case shouldn't give false, as is seen here:

It fails if you do (the equivalent of) the intros before the TNT: I had 
a doubt about that, thanks for the test case.  This works as expected:

?- solve([]=>tnt((((((p->q)->q)->p)->q)/\(q->p))->q)).

-Julio