Hilbert Style proof system (Was: Proofs as programs)

Nope your work doesn't qualify for Weekend 2.
Why, because your proof system is not a Hilbert Style
proof system. BCK and BCI Logics are Hilbert Style
proof system. You don't deal with your G=>Z.
Hibert Style proof systems don't have a context G.
They are context free. All that is prove are |- Z.
A Hilbert Style proof system is easy to define.
Definition: Hilbert Style proof system
-----------------------------------------
a) A proof is a sequence of formulas A1, .., An
b) Aj is either an application of modus ponense
   of two formulas Ai, Ak with i<j, k<j
c) Or Aj is an instantiation of an axiom schema.
d) What gets proved is the last formula An.
See also:
https://en.wikipedia.org/wiki/Hilbert_system
Example of a Hilbert Style Proof system in
Prolog with a combinator proof extraction:
Combinatory Logic in Prolog
https://swi-prolog.discourse.group/t/combinatory-logic-in-prolog/7536/6
Maybe your work qualifies for Weekend 3.
I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?
Mild Shock schrieb:

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
>