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: Proofs as programs
Date: Wed, 18 Dec 2024 15:16:08 +0100
Message-ID: <vjulf8$1er6n$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 18 Dec 2024 14:16:08 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1535191"; 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:bMsaTj5A1bk+Z8fqsUsbGwb/2l0=
X-User-ID: eJwNy8ERwDAIA7CVSiGmGccQvP8IzVun5TB0BhZiaclqzi6yJjVuOm4dzY7MDJOD+vaweFexHzCei5oXrRj8lzEXMw==
In-Reply-To: <vju67k$1m603$4@dont-email.me>
Bytes: 3059
Lines: 53

The challenge is this here:

Mild Shock schrieb:
 > Advent of Logic 2024: Weekend 2
 > Create a *proof search* in Combinatory Logic,
 > that finds a Combinator Expression as proof
 > for a given formula in propositional logic.
 >
 > The propositional logic can do with
 > implication only, and it should be *Linear Logic*.
 > French logician Jean-Yves Girard is credited
 >
 > with Linear Logic, and since we have implication
 > logic only, the Logic will be also *affine*, i.e.
 > it will have no contraction, which makes
 >
 > it special towards certain paradoxes.

As a test case, you could show for example a proof of:

(a -> ((a -> b) -> b))

But you find more formulas as test cases here:

BCK and BCI Logics, Condensed Detachment and the 2-Property
J. ROGER HINDLEY -  Notre Dame Journal of Formal Logic
Volume 34, Number 2, Spring 1993
https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-34/issue-2/BCK-and-BCI-logics-condensed-detachment-and-the-2-property/10.1305/ndjfl/1093634655.pdf

Section 3.6.1 and 3.6.2 are test cases.

Julio Di Egidio schrieb:
> On 18/12/2024 08:43, Mild Shock wrote:
> 
>> The advent of logic tasks are not philosophical,
>> they directly ask for a calculus aka proof search
>> in Prolog. You could add some philosophical notes
>> to the resulting Prolog code.
> 
> "Philosophy" as in not being a vacuous dumb fuck?  I hope.
> 
> I was asking if my work would qualify for your challenge, in fact what 
> the challenge even is, since you cannot write a problem statement that 
> is one.
> 
> When you have missed that point, I have pointed out that accessorized 
> system variant 1765234 is utterly uninteresting when pure system 0 is 
> already a difficult foundational then coding problem otherwise a cheat.
> 
> But don't take my word for it.
> 
> -Julio
>