Path: ...!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: Happy Now? (Was: Please be patient)
Date: Fri, 20 Dec 2024 19:31:36 +0100
Message-ID: <vk4d67$1i1iv$1@solani.org>
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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 20 Dec 2024 18:31:35 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1640031"; 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:Uv71WjQhOcWpJhtZdchWX6JmQ4Q=
X-User-ID: eJwFwQkBwDAIA0BLUEg65PAU/xJ2B6OyrxN0LLbsSdTZB76WaFLPjAnYlYjsKJ8Qbh5YetwQzHNV9dFPvh9fchUs
In-Reply-To: <vk4cd3$1i15s$1@solani.org>
Bytes: 3062
Lines: 71

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p

/* 3 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .

/* 2 negative test case */

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Mild Shock schrieb:
> Hi,
> 
> Ok, Ok, nobody cares. I will put different
> labels on the bottles. And use this naming:
> 
> BCI: Linear Logic
> BCK: Affine Logic
> SK: Minimal Logic
> 
> You will see a further file linear.p in this
> gist in a blink. Please be patient.
> 
> https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72 
> 
> 
> Bye
> 
> P.S.: The logics concerning derivable
> sentences show this inclusion:
> 
> Linear ⊂ Affine ⊂ Minimal
> 
> 
> Julio Di Egidio schrieb:
>> On 20/12/2024 18:46, Mild Shock wrote:
>>> Julio Di Egidio schrieb:
>>>> On 20/12/2024 02:48, Mild Shock wrote:
>>
>>>>> I tried it heuristically, Affine Logic can indeed not
>>>>> prove (A -> (B -> A)). Don't know yet how to show it
>>>>> rigorously, this would need some model theory.
>>>>
>>>> That is simply wrong, affine logic can of course prove a statement 
>>>> where, after the intros, hypothesis 1 is used once and hypothesis 2 
>>>> is not used at all.  That wouldn't be valid for linear logic (in the 
>>>> sense still of a substructural logic), as we are not using all 
>>>> hypothesis.
>>>
>>> If it were a tautology of Affine Logic,
>>> it would have a BCI combinator expression.
>>
>> Indeed, BCI gives linear logic (in the substructural sense), not 
>> affine...
>>
>> <https://ncatlab.org/nlab/show/combinatory+logic>
>>
>> -Julio
>>
>