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: Hilbert Style proof system (Was: Proofs as programs)
Date: Wed, 18 Dec 2024 15:30:40 +0100
Message-ID: <vjumaf$1erpp$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 18 Dec 2024 14:30:39 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1535801"; 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:AeaU+cLOsKakigTQIoWhAu4K0uQ=
In-Reply-To: <vjulf8$1er6n$1@solani.org>
X-User-ID: eJwNy8kBwCAIBMCW5FjWlCMg/ZcQ/zOwkCh6IByDqT1EkYuaK8TPHtxv6h5lrm6y5dHrHi+ZQXtnFUNxBJo/TQkVDQ==
Bytes: 4327
Lines: 90

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
>>
>