Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!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: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please
 be patient))
Date: Sat, 21 Dec 2024 01:58:17 +0100
Organization: A noiseless patient Spider
Lines: 23
Message-ID: <vk53r9$3f87m$4@dont-email.me>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$1@solani.org>
 <vk2ie7$1h00a$1@solani.org> <vk49vq$3f87m$1@dont-email.me>
 <vk4ah4$14gh0$1@solani.org> <vk4bi2$3f87m$2@dont-email.me>
 <vk4cd3$1i15s$1@solani.org> <vk4d67$1i1iv$1@solani.org>
 <vk4e8a$3f87m$3@dont-email.me> <vk527m$1ibbn$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 21 Dec 2024 01:58:18 +0100 (CET)
Injection-Info: dont-email.me; posting-host="753862d9528b1832f19ea3b611748cc9";
	logging-data="3645686"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+k01EZxQsYGxsPMOAISzvg8C8rGoh4Edo="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:aW3EpMJ9MrmxtopYB0C1LCfDrBw=
Content-Language: en-GB
In-Reply-To: <vk527m$1ibbn$1@solani.org>
Bytes: 1863

On 21/12/2024 01:30, Mild Shock wrote:
> Hi,
> 
> Could you define what you mean by "gentzen"?

Really?? This is what I mean by "gentzen" (lowercase):

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

Code is law!  All else failing...

> Can you convert this proof:
> 
>  > ?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
>  > Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
>  > false
> 
> Into a BCK expression?

I'll see if I can figure it out.

-Julio