Re: can λ-prolog do it? (Was: How to prove this theorem with intuitionistic natural deduction?)

But you will not immediately see the
difference. Since for tautologies, by
weakening if this here is provable:
(~(~X))
Then this here is also provbale.
~X->(~(~X))
And also vice versa, which a simple
classical transformation shows. So you
might only notice a speed difference,
speed in finding a proof.
P.S.: To get even more speed you
might apply some cuts here and then,
based on Gentzens inversion lemmas.
You see which cuts are allowed in Jens Ottens prover:
https://www.leancop.de/ileansep/index.html#Source
Mild Shock schrieb:

This is Peirce law:
 ((p->q)->p)->p
Peirce law is not provable in minimal logic.
 But I guess this is not Glivenko:
notation(dnt(X), ~X->(~(~X)))
 https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic   Glivenko would be simply:
notation(gliv(X), (~(~X)))
  Julio Di Egidio schrieb:

On 19/11/2024 14:55, Mild Shock wrote:

Julio Di Egidio schrieb:

On 19/11/2024 12:25, Mild Shock wrote:

Can λ-prolog do it? The proof is a little bit
tricky, since line 1 is used twice in
line 2 and in line 4. So its not a proof
tree, rather a proof mesh (*).

>
My reduction rules actually take a goal and, if it can be reduced, return proof steps and residual goals.  But indeed, my experiment has started with "how far can I get without lambda Prolog", aka "why lambda Prolog?"

>
I don't know exactly what your full source
code in plain Prolog is.

>
It's here for your preview, up to disjunction and with a beginning of a proof tree (still with the messed up numbering):
>
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
>
And it fails one test:
>
```
?- solve_t.
pos:begin:
- absorpt   : [(p->q)]=>p->p/\q             : ok
- andcomm   : [p/\q]=>q/\p                  : ok
- codilem   : [(p->q),(r->s),p\/r]=>q\/s    : FAIL!
- distand   : []=>p/\(q\/r)<->p/\q\/p/\r    : ok
- distor    : []=>p\/q/\r<->(p\/q)/\(p\/r)  : ok
- export    : [(p/\q->r)]=>p->q->r          : ok
- import    : [(p->q->r)]=>p/\q->r          : ok
- frege     : [(p->q->r)]=>(p->q)->p->r     : ok
- hsyllo    : [(p->q),(q->r)]=>p->r         : ok
- idempand  : []=>p/\p<->p                  : ok
- idempor   : []=>p\/p<->p                  : ok
pos:end: tot.=11, failed=1 : FAIL!
neg:begin:
- pierce    : []=>((p->q)->p)->p            : ok
neg:end: tot.=1, failed=0 : ok
false.
```
>
And I have already spent a day trying to find the bug, the trace is a little bit overwhelming:
>
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```
>
-Julio
>