On 20/12/2024 18:46, Mild Shock wrote:

Julio Di Egidio schrieb:

On 20/12/2024 02:48, Mild Shock wrote:

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

That is simply wrong, affine logic can of course prove a statement
where, after the intros, hypothesis 1 is used once and hypothesis 2 is
not used at all. That wouldn't be valid for linear logic (in the
sense still of a substructural logic), as we are not using all
hypothesis.

If it were a tautology of Affine Logic,
it would have a BCI combinator expression.

Indeed, BCI gives linear logic (in the substructural sense), not affine...

<https://ncatlab.org/nlab/show/combinatory+logic>

-Julio

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

To the best of my knowledge (A -> (B -> A)) is
not a tautology of Affine Logic.

If it were a tautology of Affine Logic,
it would have a BCI combinator expression.

What should be the BCI combinator expression
that fills in the blank ?? here:

?? : (A -> (B -> A))

Can you demonstrate a BCI combinator expression
that has the type (A -> (B -> A)).


Julio Di Egidio schrieb:

On 20/12/2024 02:48, Mild Shock wrote:

Its quite intersting that Affine Logic can
be measured by the realization of this output:

- Output = Variable         % Repetition

Though, can it?  (More below.)

λx:A.λy:B.x : (A -> (B -> A))
I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

That is simply wrong, affine logic can of course prove a statement
where, after the intros, hypothesis 1 is used once and hypothesis 2 is
not used at all.  That wouldn't be valid for linear logic (in the sense still of a substructural logic), as we are not using all hypothesis.

As to how that relates to the lambda calculus side I still don't know,
but I find significant that you says Repetition while I (substructural
logic) says Use...

-Julio

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

Hi,

Ok, Ok, nobody cares. I will put different
labels on the bottles. And use this naming:

BCI: Linear Logic
BCK: Affine Logic
SK: Minimal Logic

You will see a further file linear.p in this
gist in a blink. Please be patient.

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72


Bye

P.S.: The logics concerning derivable
sentences show this inclusion:

Linear ⊂ Affine ⊂ Minimal


Julio Di Egidio schrieb:

On 20/12/2024 18:46, Mild Shock wrote:

Julio Di Egidio schrieb:

On 20/12/2024 02:48, Mild Shock wrote:

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

That is simply wrong, affine logic can of course prove a statement
where, after the intros, hypothesis 1 is used once and hypothesis 2
is not used at all.  That wouldn't be valid for linear logic (in the
sense still of a substructural logic), as we are not using all
hypothesis.

If it were a tautology of Affine Logic,
it would have a BCI combinator expression.

Indeed, BCI gives linear logic (in the substructural sense), not affine...

<https://ncatlab.org/nlab/show/combinatory+logic>

-Julio

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

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p

/* 3 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .

/* 2 negative test case */

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Mild Shock schrieb:

Hi,

Ok, Ok, nobody cares. I will put different
labels on the bottles. And use this naming:

BCI: Linear Logic
BCK: Affine Logic
SK: Minimal Logic

You will see a further file linear.p in this
gist in a blink. Please be patient.

https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72

Bye

P.S.: The logics concerning derivable
sentences show this inclusion:

Linear ⊂ Affine ⊂ Minimal

Julio Di Egidio schrieb:

On 20/12/2024 18:46, Mild Shock wrote:

Julio Di Egidio schrieb:

On 20/12/2024 02:48, Mild Shock wrote:

I tried it heuristically, Affine Logic can indeed not
prove (A -> (B -> A)). Don't know yet how to show it
rigorously, this would need some model theory.

That is simply wrong, affine logic can of course prove a statement
where, after the intros, hypothesis 1 is used once and hypothesis 2
is not used at all.  That wouldn't be valid for linear logic (in the
sense still of a substructural logic), as we are not using all
hypothesis.

If it were a tautology of Affine Logic,
it would have a BCI combinator expression.

Indeed, BCI gives linear logic (in the substructural sense), not
affine...

<https://ncatlab.org/nlab/show/combinatory+logic>

-Julio

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

On 20/12/2024 19:31, Mild Shock wrote:

<https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p>

/* 3 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .

/* 2 negative test case */

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Hmm, gentzen proves them all:

```
?- prove(pos, []=>(a->a)->(a->a), Ps).
Ps = [impI,init(0)] ;
Ps = [impI,impI,init(0)] ;
Ps = [impI,impI,impE(1),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->((a->b)->b), Ps).
Ps = [impI,impI,impE(0),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->(b->a), Ps).
Ps = [impI,impI,init(1)] ;
false.

?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false.
```

-Julio

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

Hi,

Could you define what you mean by "gentzen"?
The problem is Gentzen paper contains two calculi:

- NK/NJ: Classical and Intuitionistic Natural Deduction
The rules are called elimination/introduction rules https://en.wikipedia.org/wiki/Natural_deduction

- LK/LJ: Classical and Intuitionistic Sequent Calculus
The rules are called left/right rules https://en.wikipedia.org/wiki/Sequent_calculus

Can you convert this proof:

?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false

Into a BCK expression?

Bye

Julio Di Egidio schrieb:

On 20/12/2024 19:31, Mild Shock wrote:

<https://gist.github.com/Jean-Luc-Picard-2021/bc829e6c002b955a51a49ae3bf384c72#file-affine-p>


/* 3 positive test cases */

% ?- between(1,13,N), search(typeof(X, ((a->a)->(a->a))), N, 0).
% N = 3,
% X = c*k .

% ?- between(1,13,N), search(typeof(X, (a->((a->b)->b))), N, 0).
% N = 7,
% X = c*(c*k*k) .

% ?- between(1,13,N), search(typeof(X, (a->(b->a))), N, 0).
% N = 1,
% X = k .

/* 2 negative test case */

% ?- between(1,13,N), search(typeof(X, ((a->(a->b))->(a->b))), N, 0).
% false.

Hmm, gentzen proves them all:

```
?- prove(pos, []=>(a->a)->(a->a), Ps).
Ps = [impI,init(0)] ;
Ps = [impI,impI,init(0)] ;
Ps = [impI,impI,impE(1),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->((a->b)->b), Ps).
Ps = [impI,impI,impE(0),[init(0)],[init(0)]] ;
false.

?- prove(pos, []=>a->(b->a), Ps).
Ps = [impI,impI,init(1)] ;
false.

?- prove(pos, []=>(a->(a->b))->(a->b), Ps).
Ps = [impI,impI,impE(1),[init(0)],[impE(0),[init(0)],[init(0)]]] ;
false.
```

-Julio

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