Re: Still on negative translation for substructural logics

On 01/12/2024 16:17, Julio Di Egidio wrote:

Here is an interesting new case, which I had thought should be *unsolvable*:
 ```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !.  % DNE<->LEM
```

<snip>

Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get).  Indeed, I am rather worried that it just solves everything I throw at it, though not the falsities...

I am an idiot: that statement is not true intuitionistically, but it is true classically, so in fact nothing strange there.
-Julio