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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

The requirement for week 3 is explicitly lambda expressions:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

For Affine Logic the lambda expressions should have a funny property:

- A variable occurs only once unbound in the bound scope.

For example this here, although it has a simple type:

λ y:A λ x:A->A. x (x y)

It cannot be a proof term of Affine Logic, since x occurs twice.

Some testing showed you don't produce lambda expressions:

You produce:

But I am not familiar with this proof display:

[
impI((p->0))
impI((p->0))
[
impE1(1:(p->q))
impI(p)
[
impE1(1:p)
unif(2:p)
]
[
impE2(1:0)
botE(3:0)
]
]
[
impE2(1:p)
[
impE1(1:p)
unif(2:p)
]
[
impE2(1:0)
unif(3:0)
]
]
]

Julio Di Egidio schrieb:

On 18/12/2024 15:30, Mild Shock wrote:

Maybe your work qualifies for Weekend 3.

In fact, I have replied to the WE3 announcement.

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

It implements "affine intuitionistic propositional logic", and I am
getting to evaluation/compilation which is the functional side (more
details in my initial reply): so, sure, I even classify my reduction
rules as intros vs elims...

What is the deadline?  I don't know what WE is 3.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

The typing rules for WE3 are similar to WE2.
The changes are:

- WE2 doesn't require a context
- WE3 requires a context
- WE2 has only modus ponense and constants
- WE3 has additionally deduction theorem and variables

See also here what WE3 requires:

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules

Bye

Mild Shock schrieb:

The requirement for week 3 is explicitly lambda expressions:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

For Affine Logic the lambda expressions should have a funny property:

- A variable occurs only once unbound in the bound scope.

For example this here, although it has a simple type:

λ y:A λ x:A->A. x (x y)

It cannot be a proof term of Affine Logic, since x occurs twice.

Some testing showed you don't produce lambda expressions:

You produce:

But I am not familiar with this proof display:

[
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]

Julio Di Egidio schrieb:

On 18/12/2024 15:30, Mild Shock wrote:

Maybe your work qualifies for Weekend 3.

In fact, I have replied to the WE3 announcement.

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

It implements "affine intuitionistic propositional logic", and I am
getting to evaluation/compilation which is the functional side (more
details in my initial reply): so, sure, I even classify my reduction
rules as intros vs elims...

What is the deadline?  I don't know what WE is 3.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

What I don't know yet, is how to assure that
the context is used affine. Non-affine modus ponens

can be seen as, where E is what is common in both
contexts, and the comma is disjoint union:

G, E |- A -> B E, D |- A
--------------------------------
G, E, D |- B

In linear logic the linear implication uses
a splitting context:

G |- A -o B D |- A
--------------------------------
G, D |- B

This is unlike intuitionistic logic, which uses the
Non-affine modus ponense. But the affine modus

ponens uses a splitting context. How implement
proof search efficiently for splitting context?

I have some idea based on DCG. But I didn't find
a paper yet showing such a DCG based search

for linear logic.

Bye

Mild Shock schrieb:

Hi,

The typing rules for WE3 are similar to WE2.
The changes are:

- WE2 doesn't require a context
- WE3 requires a context
- WE2 has only modus ponense and constants
- WE3 has additionally deduction theorem and variables

See also here what WE3 requires:

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules

Bye

Mild Shock schrieb:

The requirement for week 3 is explicitly lambda expressions:

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

For Affine Logic the lambda expressions should have a funny property:

- A variable occurs only once unbound in the bound scope.

For example this here, although it has a simple type:

λ y:A λ x:A->A. x (x y)

It cannot be a proof term of Affine Logic, since x occurs twice.

Some testing showed you don't produce lambda expressions:

You produce:

But I am not familiar with this proof display:

[
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]

Julio Di Egidio schrieb:

On 18/12/2024 15:30, Mild Shock wrote:

Maybe your work qualifies for Weekend 3.

In fact, I have replied to the WE3 announcement.

I don't know yet. You have to tell us. Do
you think it implements a Natural Deduction
with Simple Types proof extraction?

It implements "affine intuitionistic propositional logic", and I am
getting to evaluation/compilation which is the functional side (more
details in my initial reply): so, sure, I even classify my reduction
rules as intros vs elims...

What is the deadline?  I don't know what WE is 3.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Julio Di Egidio schrieb:

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Well it does. It is based on the combinators B and C.
You cannot translate a lambda expression where x occurs twice
with B and C. You would need S.

Rule 7 and 8
https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C

With B and C, you can only translate λx.(E1 E2) if x
occurs in E1 or E2 or none, but not in both E1 and E2.

Basically the implied requirement to have an equivalence
between the natural deduction and the hilbert style proofs,
that every lambda express can be translated to BCI.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Some testing showed you don't produce lambda expressions:

A proof tree is not a lambda expression.

You produce:

I produced: a month has passed and I am at version 30.

But I am not familiar with this proof display:

From: Mild Shock <[email protected]>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural
deduction?

0: P -> (Q -> R) (Premisse)
1: P /\ Q (Assumption)
2: P (/\E,1)
3: Q -> R (->E,0,2)
4: Q (/\E,1)
5: R (->E,3,4)
6: P /\ Q -> R (Discharge,1)

Confront with this one:

?- prove([p->q->r]=>p/\q->r, Ps), print_ps(Ps).
[
impI
andE(0)
impE(2)
[
init(1)
]
[
impE(0)
[
init(0)
]
[
init(0)
]
]
]

Modulo finer technical details, it's the same.

What is the deadline?  I don't know what WE is 3.

You haven't answered that one.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 19/12/2024 02:37, Mild Shock wrote:

Julio Di Egidio schrieb:

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Well it does. It is based on the combinators B and C.
You cannot translate a lambda expression where x occurs twice
with B and C. You would need S.

Rule 7 and 8
https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C

With B and C, you can only translate λx.(E1 E2) if x
occurs in E1 or E2 or none, but not in both E1 and E2.

Basically the implied requirement to have an equivalence
between the natural deduction and the hilbert style proofs,
that every lambda express can be translated to BCI.

<< Affine logic is a *substructural logic* whose proof theory rejects
the structural rule of contraction. It can also be characterized as
linear logic with weakening. >>
<https://en.wikipedia.org/wiki/Affine_logic> <https://en.wikipedia.org/wiki/Substructural_type_system>

HTH.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

This is also not in the scope of advent of logic:

From: Mild Shock <[email protected]>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural
deduction?

0: P -> (Q -> R) (Premisse)
1: P /\ Q (Assumption)
2: P (/\E,1)
3: Q -> R (->E,0,2)
4: Q (/\E,1)
5: R (->E,3,4)
6: P /\ Q -> R (Discharge,1)

The advent of logic has only implication (->)/2
and no conjunction (/\)/2:

Advent of Logic 2024: Weekend 2
[...]
The propositional logic can do with
*implication only*, and it should be Linear Logic.
French logician Jean-Yves Girard is credited
[...]

It says implication only. Just like here, implication
only is sometimes called positive logic:

Meredith, D. (1978). Positive logic and λ-constants.
Studia Logica, 37(3), 269–285. doi:10.1007/bf02124728

I think the example I gave is on page 288. The
lambda expression would need an additional combinator
W, it cannot be modelled with BCI alone:

λx:A->A.λy:A.(x (x y)) : ((A -> A) -> (A -> A))

Meredith, D. gives the combinator expression BCWI.
Didn't verify. The combinator W is left contraction,
and since affine logic has no contraction, the

combinator W is not part of affine logic:

W: ((A -> (A ->B)) -> (A -> B))

Mild Shock schrieb:

Julio Di Egidio schrieb:

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Well it does. It is based on the combinators B and C.
You cannot translate a lambda expression where x occurs twice
with B and C. You would need S.

Rule 7 and 8
https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C

With B and C, you can only translate λx.(E1 E2) if x
occurs in E1 or E2 or none, but not in both E1 and E2.

Basically the implied requirement to have an equivalence
between the natural deduction and the hilbert style proofs,
that every lambda express can be translated to BCI.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Well you wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

It exactly means that. Contraction means occurs twice.
For example this combinator W does not exist in affine
logic. It has the below type, so it shows left Contraction,

the two A are contracted into a single A:

W: ((A -> (A ->B)) -> (A -> B))

As a lambda expression it has a variable that occurs twice:

W = λxλy.((x y) y)

"The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by
Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen
Logik, whose results are set out in Curry (1930)." https://en.wikipedia.org/wiki/B,_C,_K,_W_system

Affine logic has a calculus which is Currys calculus minus
the W combinator and the K combinator replaced by the I combinator.

Julio Di Egidio schrieb:

On 19/12/2024 02:37, Mild Shock wrote: <https://en.wikipedia.org/wiki/Affine_logic> <https://en.wikipedia.org/wiki/Substructural_type_system>

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Interestingly although this proof (Curry Howard
term) does not exist in Affine Logic:

λx:A->A.λy:A.(x (x y)) : ((A -> A) -> (A -> A))

There is an alternative proof (Curry Howard
term) which does exist:

λx:A->A.x : ((A -> A) -> (A -> A))

This is just the I combinator of Affine Logic.

Mild Shock schrieb:

This is also not in the scope of advent of logic:

From: Mild Shock <[email protected]>
Date: Mon, 18 Nov 2024 23:22:11 +0100
Subject: Re: How to prove this theorem with intuitionistic natural
deduction?

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

The advent of logic has only implication (->)/2
and no conjunction (/\)/2:

Advent of Logic 2024: Weekend 2
[...]
The propositional logic can do with
*implication only*, and it should be Linear Logic.
French logician Jean-Yves Girard is credited
[...]

It says implication only. Just like here, implication
only is sometimes called positive logic:

Meredith, D. (1978). Positive logic and λ-constants.
Studia Logica, 37(3), 269–285. doi:10.1007/bf02124728

I think the example I gave is on page 288. The
lambda expression would need an additional combinator
W, it cannot be modelled with BCI alone:

λx:A->A.λy:A.(x (x y))   :  ((A -> A) -> (A -> A))

Meredith, D. gives the combinator expression BCWI.
Didn't verify. The combinator W is left contraction,
and since affine logic has no contraction, the

combinator W is not part of affine logic:

W: ((A -> (A ->B)) -> (A -> B))

Mild Shock schrieb:

Julio Di Egidio schrieb:

On 19/12/2024 00:30, Mild Shock wrote:

It cannot be a proof term of Affine Logic, since x occurs twice.

That is not what affine logic means.

Well it does. It is based on the combinators B and C.
You cannot translate a lambda expression where x occurs twice
with B and C. You would need S.

Rule 7 and 8
https://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B,_C

With B and C, you can only translate λx.(E1 E2) if x
occurs in E1 or E2 or none, but not in both E1 and E2.

Basically the implied requirement to have an equivalence
between the natural deduction and the hilbert style proofs,
that every lambda express can be translated to BCI.

Bye

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 19/12/2024 02:55, Mild Shock wrote:

Advent of Logic 2024: Weekend 2
[...]
The propositional logic can do with
*implication only*, and it should be Linear Logic.
French logician Jean-Yves Girard is credited
[...]

It says implication only. Just like here, implication
only is sometimes called positive logic:

Yeah, I didn't think to read another million and one messages for pieces
of the problem statement.

I find it too particular: you should be giving a requirement/behaviour,
such as indeed an "affine intuitionistic propositional logic (that
compiles to some functional code)", not imposing details on the
implementation.

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)