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: Re: Advent of Logic 2024: Specification and Deadline (Was: Advent of
 Logic 2024: Weekend 1)
Date: Fri, 20 Dec 2024 02:48:55 +0100
Message-ID: <vk2ie7$1h00a$1@solani.org>
References: <vjks2t$sghb$1@solani.org> <vk2i2c$1gvoe$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 01:48:55 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1605642"; 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:d1PINzKU40ORciUOANnPqDDeMzY=
In-Reply-To: <vk2i2c$1gvoe$1@solani.org>
X-User-ID: eJwNwoERwCAIBLCVRJ5HxgHB/UdoLzGl8DpohL0fAutwvDzS34tKZRu3yAwmZ1KqtS5tQrHzUnvhFLrU1D9aPhXI
Bytes: 2774
Lines: 55

Its quite intersting that Affine Logic can
be measured by the realization of this output:

 > - Output = Variable         % Repetition

Its seems to me that in Affine Logic a variable
is only allowed to occur in a Repetition at most
once, it seems also to me that each variable

must be also repeated at least once. So that
variables are repreated exactly once.

Here is a counter example with too many repetitions,
this would not be a valid output for weekend 3,
since it cannot be converted into the output of weekend 2:

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

And her is a counter example with too few repetitions,
equally well it cannot be converted to a BCI expression.

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

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.

Mild Shock schrieb:
> Specification:
> 
> 
> Weekend 2:
> -----------
> - Input = Atom            % Propositional variable
>          | Input -> Input  % Implication
> 
> - Output = B               % B Axiom Schema
>           | C               % C Axiom Schema
>           | I               % I Axiom Schema
>           | (Output Output) % Modus Ponens
> 
> Weekend 3:
> -----------
> - Input = Atom            % Propositional variable
>          | Input -> Input  % Implication
> 
> - Output = Variable         % Repetition
>           | λVariable.Output % Assumption & Detachment
>           | (Output Output)  % Modus Ponens
> 
> 
> Deadline:
> 
> 24. December 2024
>