Re: Counter Example by Troelstra & Schwichtenberg (Was: Still on negative translation for substructural logics)

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