Path: ...!3.eu.feeder.erje.net!2.eu.feeder.erje.net!feeder.erje.net!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: Re: What are Simple Types (Was: Proofs as programs)
Date: Thu, 19 Dec 2024 02:55:29 +0100
Message-ID: <vjvueg$1fflm$1@solani.org>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org> <vjs63g$1m603$1@dont-email.me>
 <vjsl6t$1dmbi$1@solani.org> <vjt8up$1m603$3@dont-email.me>
 <vjttuv$10v9c$1@solani.org> <vjtueg$10vjo$1@solani.org>
 <vju67k$1m603$4@dont-email.me> <vjulf8$1er6n$1@solani.org>
 <vjumaf$1erpp$1@solani.org> <vjuptb$1m602$1@dont-email.me>
 <vjvluk$1fc4q$1@solani.org> <vjvsu1$2epso$1@dont-email.me>
 <vjvtc9$1ffc1$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 19 Dec 2024 01:55:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1556150"; 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:pD0hBHfcVYqNzcrIaG0aMYehuw8=
X-User-ID: eJwNysEBwCAIA8CVAEnUcUTM/iO09z4MOu9MgglB1WPKnVScF4KNupWlvU2IFf/pG/uRTesFD7gyDG8eZvoHWQ4VAQ==
In-Reply-To: <vjvtc9$1ffc1$1@solani.org>
Bytes: 3582
Lines: 65

This is also not in the scope of advent of logic:

From: Mild Shock <janburse@fastmail.fm>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural 
deduction?
 > 0: P -> (Q -> R) (Premisse)
 > 1: P /\ Q        (Assumption)
 > 2: P             (/\E,1)
 > 3: Q -> R        (->E,0,2)
 > 4: Q             (/\E,1)
 > 5: R             (->E,3,4)
 > 6: P /\ Q -> R   (Discharge,1)

The advent of logic has only implication (->)/2
and no conjunction (/\)/2:

 > Advent of Logic 2024: Weekend 2
 > [...]
 > The propositional logic can do with
 > *implication only*, and it should be Linear Logic.
 > French logician Jean-Yves Girard is credited
 > [...]

It says implication only. Just like here, implication
only is sometimes called positive logic:

Meredith, D. (1978). Positive logic and λ-constants.
Studia Logica, 37(3), 269–285. doi:10.1007/bf02124728

I think the example I gave is on page 288. The
lambda expression would need an additional combinator
W, it cannot be modelled with BCI alone:

λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))

Meredith, D. gives the combinator expression BCWI.
Didn't verify. The combinator W is left contraction,
and since affine logic has no contraction, the

combinator W is not part of affine logic:

W: ((A -> (A ->B)) -> (A -> B))

Mild Shock schrieb:
> Julio Di Egidio schrieb:
>> On 19/12/2024 00:30, Mild Shock wrote:
>>> It cannot be a proof term of Affine Logic, since x occurs twice.
>> That is not what affine logic means.
> 
> Well it does. It is based on the combinators B and C.
> You cannot translate a lambda expression where x occurs twice
> with B and C. You would need S.
> 
> Rule 7 and 8
> https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C
> 
> With B and C, you can only translate λx.(E1 E2) if x
> occurs in E1 or E2 or none, but not in both E1 and E2.
> 
> Basically the implied requirement to have an equivalence
> between the natural deduction and the hilbert style proofs,
> that every lambda express can be translated to BCI.
> 
> Bye