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?"

Now, thanks also to your help, I have fixed my rule for `->E` and now my
little solver in plain Prolog does it:

```plain
?- solve_test.

solve_test::pos:
- absorp: [(p->q)]=>p->p/\q --> true
- andcom: [p/\q]=>q/\p --> true
- export: [(p/\q->r)]=>p->q->r --> true
- import: [(p->q->r)]=>p/\q->r --> true
- frege_: [(p->q->r)]=>(p->q)->p->r --> true
- hsyll_: [(p->q),(q->r)]=>p->r --> true
solve_test::pos: tot.=6, FAIL=0 --> true.

solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.

true.
```

```plain
?- solve(([]=>(p->q->r)->p/\q->r), Qs).
Qs = [
impi((p->q->r)),
impi(p/\q),
impe(1:(q->r)),
impe(1:p),
impe(2:r),
impe(2:q),
equi(2:r),
ande(1:(p,q)),
equi(2:q),
ande(1:(p,q)),
equi(1:p)
].
```

In fact, it's still in its infancy and the output is still a flat mess
with wrong hypothesis numbering, but I will keep working on it with the
idea of going well past just propositional: will start sharing as soon
as I manage to implement negation, and a proper proof tree...

-Julio

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

Well my question was not really an advertisement
of λ-prolog, more an attempt to get assesment
of λ-prolog as viability for proof search.

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

It seems to me λ-prolog has the following
pros and cons:

- Good: If the prover uses member/2 to access
assumptions, or the list constructor to
push assumptions, you can do this with
embedded implication.

- Bad: If the prover uses select/3 things
get nasty. Maybe a linar logic version of
λ-prolog would help?

Bye

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?"

Now, thanks also to your help, I have fixed my rule for `->E` and now my little solver in plain Prolog does it:

```plain
?- solve_test.

solve_test::pos:
- absorp: [(p->q)]=>p->p/\q --> true
- andcom: [p/\q]=>q/\p --> true
- export: [(p/\q->r)]=>p->q->r --> true
- import: [(p->q->r)]=>p/\q->r --> true
- frege_: [(p->q->r)]=>(p->q)->p->r --> true
- hsyll_: [(p->q),(q->r)]=>p->r --> true
solve_test::pos: tot.=6, FAIL=0 --> true.

solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.

true.
```

```plain
?- solve(([]=>(p->q->r)->p/\q->r), Qs).
Qs = [
    impi((p->q->r)),
    impi(p/\q),
    impe(1:(q->r)),
    impe(1:p),
    impe(2:r),
    impe(2:q),
    equi(2:r),
    ande(1:(p,q)),
    equi(2:q),
    ande(1:(p,q)),
    equi(1:p)
].
```

In fact, it's still in its infancy and the output is still a flat mess
with wrong hypothesis numbering, but I will keep working on it with the
idea of going well past just propositional: will start sharing as soon
as I manage to implement negation, and a proper proof tree...

-Julio

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

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

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

On 22/11/2024 18:23, Julio Di Egidio wrote:

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).
```

Never mind, I have fixed it: just needed to get rid of those `once`!
Will update the Gist shortly.

If you have any feedback already, it's very welcome: anyway, will keep
you guys posted.

-Julio

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

On 27/11/2024 04:02, Ross Finlayson wrote:

On 11/22/2024 09:30 AM, Julio Di Egidio wrote:

On 22/11/2024 18:23, Julio Di Egidio wrote:

On 19/11/2024 14:55, Mild Shock wrote:
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```

Never mind, I have fixed it: just needed to get rid of those `once`!
Will update the Gist shortly.

If you have any feedback already, it's very welcome: anyway, will keep
you guys posted.

Good afternoon, what is this about briefly?

Hi Ross, it's a little linear propositional solver at this stage, but
with ambitions...

See here: <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>

Julio

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

On 27/11/2024 18:58, Ross Finlayson wrote:

On 11/27/2024 04:06 AM, Julio Di Egidio wrote:

Hi Ross, it's a little linear propositional solver at this stage, but
with ambitions...

Of course a variety of what are "non-standard", results, according
to the standard, are standard again, establishing the very ideals
and "goals" of inference, intuitionistic in the sense of a
"fuller dialectic".

I think my system is actually affine, not linear.
Whichever, that up to computability logic is the key idea: <https://en.wikipedia.org/wiki/Substructural_type_system>

Anyway, experimenting while learning... Indeed,
"I just write code that works, theory comes later".

Thanks for the feedback.

-Julio

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

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

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

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))

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

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

Actually I don't know whether the reverse
direction really holds. This needs
probably more work. We would need to have

(~X -> (~(~X))) -> (~(~X))

provable in minimal logic?

Mild Shock schrieb:

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))

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

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

On 28/11/2024 00:55, Mild Shock wrote:

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)))

Indeed Glivenko's is to embed classical into intuitionistic, not into
linear (or affine).

OTOH, you can try the code yourself: with that 'dnt' the solver solves
all the classical theorems I have been able to think about, Pierce's law included, otherwise it fails: because of linearity essentially, i.e. not
enough hypotheses... <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>

That said, that 'dnt' is almost surely not really correct, indeed maybe
it only works for me because my reduction rules are linear (affine
actually), yet my operators for now are only the intuitionistic ones, I
do not have the whole set of linear operators.

Here are lecture notes that maybe have a complete answer/recipe, see
from page 5, but I still cannot fully parse what they write: <https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>

Meanwhile, you might have seen it, I have also asked on SE: <https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

-Julio

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

On 28/11/2024 01:52, Julio Di Egidio wrote:

On 28/11/2024 00:55, Mild Shock wrote:

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)))

Indeed Glivenko's is to embed classical into intuitionistic, not into
linear (or affine).

OTOH, you can try the code yourself: with that 'dnt' the solver solves
all the classical theorems I have been able to think about, Pierce's law included, otherwise it fails: because of linearity essentially, i.e. not enough hypotheses... <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>

That said, that 'dnt' is almost surely not really correct, indeed maybe
it only works for me because my reduction rules are linear (affine
actually), yet my operators for now are only the intuitionistic ones, I
do not have the whole set of linear operators.

Though that is itself most probably nonsense: there are no linear
operators in the classical theorems...

Here are lecture notes that maybe have a complete answer/recipe, see
from page 5, but I still cannot fully parse what they write: <https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>

Meanwhile, you might have seen it, I have also asked on SE: <https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

And I thought this was an easy one. Maybe that 'dnt' *is* correct: but
maybe not. I just thought the expert would know straight away: me, I'd
have to formalize the whole thing in Coq to prove meta-properties, but
then I don't know what I am paying taxes for...


-Julio

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

On 28/11/2024 02:38, Mild Shock wrote:

In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.

Define A^n o- B as:

A o- A o- .. A o- B
\-- n times --/

The running the prover with this notation:

A -> B  := A^n o- B

repeatedly with increasing n .

Yeah, something like that, but I am pretty sure we can do better than
just trial and error.

-Julio

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

But in a linear logic you can do
intuitionistic logic by using this notation:

A -> B := !A o- B

BTW: There are alternative approaches to
directly find a notation for classical implication
in linear logic, without the need for Glivenkos theorem.

Just put an eye here:

https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical/intuitionistic_logic_in_linear_logic

Julio Di Egidio schrieb:

On 28/11/2024 00:55, Mild Shock wrote:

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)))

Indeed Glivenko's is to embed classical into intuitionistic, not into
linear (or affine).

OTOH, you can try the code yourself: with that 'dnt' the solver solves
all the classical theorems I have been able to think about, Pierce's law included, otherwise it fails: because of linearity essentially, i.e. not enough hypotheses... <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>

That said, that 'dnt' is almost surely not really correct, indeed maybe
it only works for me because my reduction rules are linear (affine
actually), yet my operators for now are only the intuitionistic ones, I
do not have the whole set of linear operators.

Here are lecture notes that maybe have a complete answer/recipe, see
from page 5, but I still cannot fully parse what they write: <https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>

Meanwhile, you might have seen it, I have also asked on SE: <https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

-Julio

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

In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.

Define A^n o- B as:

A o- A o- .. A o- B
\-- n times --/

The running the prover with this notation:

A -> B := A^n o- B

repeatedly with increasing n .

Mild Shock schrieb:

But in a linear logic you can do
intuitionistic logic by using this notation:

    A -> B := !A o- B

BTW: There are alternative approaches to
directly find a notation for classical implication
in linear logic, without the need for Glivenkos theorem.

Just put an eye here:

https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical/intuitionistic_logic_in_linear_logic

Julio Di Egidio schrieb:

On 28/11/2024 00:55, Mild Shock wrote:

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)))

Indeed Glivenko's is to embed classical into intuitionistic, not into
linear (or affine).

OTOH, you can try the code yourself: with that 'dnt' the solver solves
all the classical theorems I have been able to think about, Pierce's
law included, otherwise it fails: because of linearity essentially,
i.e. not enough hypotheses...
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>

That said, that 'dnt' is almost surely not really correct, indeed
maybe it only works for me because my reduction rules are linear
(affine actually), yet my operators for now are only the
intuitionistic ones, I do not have the whole set of linear operators.

Here are lecture notes that maybe have a complete answer/recipe, see
from page 5, but I still cannot fully parse what they write:
<https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf> >>

Meanwhile, you might have seen it, I have also asked on SE:
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>


-Julio

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

Well I don't know an online affine logic prover.
But you can play with linear logic here:

P -o P * P is not provable https://click-and-collect.linear-logic.org/?s=P+-o+P+*+P

!P -o P * P is provable https://click-and-collect.linear-logic.org/?s=%21P+-o+P+*+P

Julio Di Egidio schrieb:

On 28/11/2024 02:38, Mild Shock wrote:

In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.

Define A^n o- B as:

A o- A o- .. A o- B
\-- n times --/

The running the prover with this notation:

A -> B  := A^n o- B

repeatedly with increasing n .

Yeah, something like that, but I am pretty sure we can do better than
just trial and error.

-Julio

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

Affin and linear logic share the use once of a
hypothesis for implication, the unprovability of
P -o P * P being an example of this similarity.

The difference between these logics is somewhere
else in structural rules, and therefore I guess
disjunction is different, but not implication.

But this translation would at least cover implication:

A o- A o- .. A o- B
\-- n times --/

Mild Shock schrieb:

Well I don't know an online affine logic prover.
But you can play with linear logic here:

P -o P * P is not provable https://click-and-collect.linear-logic.org/?s=P+-o+P+*+P

!P -o P * P is provable https://click-and-collect.linear-logic.org/?s=%21P+-o+P+*+P

Julio Di Egidio schrieb:

On 28/11/2024 02:38, Mild Shock wrote:

In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.

Define A^n o- B as:

A o- A o- .. A o- B
\-- n times --/

The running the prover with this notation:

A -> B  := A^n o- B

repeatedly with increasing n .

Yeah, something like that, but I am pretty sure we can do better than
just trial and error.

-Julio

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

On 28/11/2024 09:04, Mild Shock wrote:

Affin and linear logic share the use once of a
hypothesis for implication, the unprovability of
P -o P * P being an example of this similarity.

Should have been yesterday, but it's still the next frontier:

<https://girard.perso.math.cnrs.fr/0.pdf>

Of course more than half of it is under a pay wall, but we'll do what we
can...

-Julio

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

What would make me already happy , if we would be able
to make definitions of these terms, namely:
- Affine logic
- Linear logic

I found this helpful, which isn't behind a paywall:

https://en.wikipedia.org/wiki/Substructural_type_system

"Type system" can be another word for "logic with
proof terms", if you look at:

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

And substructural fits the idea to drop
some of the structural rules.

But to be precise one would need to distingish
left and right structural rules. For example
contraction can happen in at least these two forms:

A & A -> A

A -> A v A

If you have (A & B -> C) == (A -> (B -> C)) you most
lilely won't get rid of the first form.

Julio Di Egidio schrieb:

On 28/11/2024 09:04, Mild Shock wrote:

Affin and linear logic share the use once of a
hypothesis for implication, the unprovability of
P -o P * P being an example of this similarity.

Should have been yesterday, but it's still the next frontier:

<https://girard.perso.math.cnrs.fr/0.pdf>

Of course more than half of it is under a pay wall, but we'll do what we can...

-Julio

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

On 28/11/2024 00:55, Mild Shock wrote:

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)))

We have gone over that already. Either you have memory problems or you
are purposely flooding the channel at this point.

-Julio

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

On 01/12/2024 14:15, Mild Shock wrote:

"Type system" can be another word for "logic with
proof terms", if you look at: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

Indeed, a proof tree is a program and a solver is a compiler. But the
real point is about *pure* *formal* logic, how it works and is the only
thing that works, as long as it pure: i.e. Logic proper is exactly
outside and above it, before and after any mechanics.

The received meta-theories and "philosophies" are completely upside down
and yet another global fraud on top of the genocides. And the advent of
their "AI", sold as a solution to problems when it's really the lobotomy
on a side and the lying with numbers on the other: another nail in the
global coffin.

-Julio

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

I am busy with other stuff. I have
decided to postpone logic for a while.

So although it was very temping to download
you software, and then replace these line:

notation(dnt(X), ~X->(~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>dnt(X)).

https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11

By these line:

notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>gliv(X)).

I am afraid I have no time for that. You
could do it by yourself. Or what

until somebody else does it. What will be
the results?

Julio Di Egidio schrieb:

On 28/11/2024 00:55, Mild Shock wrote:

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)))

We have gone over that already.  Either you have memory problems or you
are purposely flooding the channel at this point.

-Julio

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