Re: Proofs as programs

Hi,
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.
 > 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.
I have such a Prolog code already. Its relatively
easy to program. But I am hesitant to publish it,
still looking for BCI logic test cases.
Actually this paper could come handy:
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
It has a section with a few test cases, such
as proving this formula:
a -> ((a -> b) -> b)
Bye
Mild Shock schrieb:

Hi,
 In the below * is modus ponens, not composition.
 For example B and B' are interchangeable.
 B' = C*B
 B = C*B'
 What are C, B and B':
 C: ((a->(b->c))->(b->(a->c))))
 B: ((b->c)->((a->b)->(a->c))))
 B': ((a->b)->((b->c)->(a->c)))
 So there is not only the calculus based on BCI,
producing hilbert style proofs in affine logic.
but there is also the calculus based on B'CI.
 Bye
 P.S.: The Lafont & Girard paper shows a calculus
using B', B' is the composition operator of
categorical logics.
 Julio Di Egidio schrieb:

On 17/12/2024 20:59, Mild Shock wrote:

Julio Di Egidio schrieb:

Sounds good?  Anything else? :)

5. Linear (BCI) and affine (BCK) combinatory logic
But I guess there are other ones as well?

>
The RISK guy doesn't care about the million variants and inflorescences and accessories: to begin with, try and give some actual *substance* to your system.
>
Here is some historical intro to the problem I am hinting at:
<https://plato.stanford.edu/entries/intuitionistic-logic-development/objections.html> >
>
-Julio
>