Re: Proofs as programs

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