Re: Affine Logic, what Properties does it have? (Was: Counter Example by Troelstra & Schwichtenberg)

But proving structural rules is a little
bit unorthodox. In the realm of rewrite rules,
one would for example prove a CR property:
https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem
And then conclude some normalization properties.
Justifying reference to "the normal form" of a
given normalizable term.
But if we do the CR orthodoxy we still have not
yet closed the abys between specification
and execution.
Mild Shock schrieb:

Ok, this here is classical logic,
deterministically expressed:
 prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
 It can readily prove Peirce Law:
 ?- prove([(((p->q)->p)->p)]).
true.
 With Coq or Isabelle/HOL you should be
also able to prove these meta theorems about
the Prolog predicate prove/1:
      prove([...,X,Y,...])
    ----------------------- (Exchange)
     prove([...,Y,X,...])
      prove([...,X,X,...])
    ----------------------- (Contraction)
      prove([...,X,...])
       prove([...,X,...])
    ----------------------- (Weakening)
     prove([...,Y,X,...])
 https://en.wikipedia.org/wiki/Structural_rule
 If you replace prove/1 with a deterministic prover
for affine logic, I guess you will still be
able to verify (Exchange) and (Weakening) for
 an arbitary input. But not anymore (Contraction)
in general. What is the deterministic prover for
affine logic?
 Julio Di Egidio schrieb:

On 04/12/2024 08:47, Mild Shock wrote:
>

Now I tried an example by Troelstra & Schwichtenberg:
>
solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
>
At least the second case shouldn't give false, as is seen here:

>
It fails if you do (the equivalent of) the intros before the TNT: I had a doubt about that, thanks for the test case.  This works as expected:
>
?- solve([]=>tnt((((((p->q)->q)->p)->q)/\(q->p))->q)).
>
-Julio
>