How to prove this theorem with intuitionistic natural deduction?

[Julio Di Egidio]

Dear logicians,

How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?

`(P -> Q -> R) |- (P /\ Q -> R)`

Thanks for any help.

-Julio

[Mild Shock]

0: P -> (Q -> R) (Premisse)
1: P /\ Q (Assumption)
2: P (/\E,1)
3: Q -> R (->E,0,2)
4: Q (/\E,1)
5: R (->E,3,4)
6: P /\ Q -> R (Discharge,1)

Post by Julio Di Egidio
Dear logicians,
How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?
  `(P -> Q -> R) |- (P /\ Q -> R)`
Thanks for any help.
-Julio

[Julio Di Egidio]

Post by Mild Shock

Post by Julio Di Egidio
`(P -> Q -> R) |- (P /\ Q -> R)`

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

Wonderful, thank you.

-Julio

[Mild Shock]

Hi,

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 (*). What would λ-prolog
give via curry howard? If we would use something
along these lines:

https://en.wikipedia.org/wiki/%CE%9BProlog#Programming_in_%CE%BBProlog

The proof search is loosely from the book
figure 9.6 Programming in Higher-Order Logic
from Miler and Nadathur.

Bye

(*) Displayed in Fitch Style.

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio
`(P -> Q -> R) |- (P /\ Q -> R)`

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

Wonderful, thank you.
-Julio

[Julio Di Egidio]

Post by Mild Shock
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

[Mild Shock]

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

Post by Julio Di Egidio

Post by Mild Shock
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
```plain
?- solve_test.
- 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.
- 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

[Julio Di Egidio]

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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

[Julio Di Egidio]

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
```
?- solve_t.
- 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!
- 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
```
?- 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

[Ross Finlayson]

Post by Julio Di Egidio

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
```
?- solve_t.
- 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!
- 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
```
?- 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

Good afternoon, what is this about briefly?

[Julio Di Egidio]

Post by Ross Finlayson

Post by Julio Di Egidio

Post by Julio Di Egidio
```
?- 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

[Ross Finlayson]

Post by Julio Di Egidio

Post by Ross Finlayson

Post by Julio Di Egidio

Post by Julio Di Egidio
```
?- 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...
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
Julio

Hallo Julio, well then warm regards.

The "intuitionistic", reflects mostly part of the dialectic,
thesis/antithesis/synthesis, the anti-thesis part, grounded
on its own ideals, then when later combined, what's new is
old again - intuitionism today is either theory tomorrow
or gathering dust in the basement of Hilbert's Infinite Living
Working Museum the speculative theories.

The, "axiomless", then, natural deduction, is what I think you mean
when you say "intuitionistic", natural deduction, then that deduction
is a very thorough sort of idea - with both "abstraction" and
generalization and "reduction" and simplification or mathematics
the theory the practice.

Here it's considered to demand a brief metaphysics and the
establishment of a putative true, complete, consistent theory,
a "mere metaphysics", that's though the theory, with nothing/everything
then universals and point/space and "axiomless natural geometry".

It seems definitely so that "material implication" of course is
excluded from a true monotone, modal theory with
free/unrestricted/many-ordered monotonicity and modality and entailment.
The "material
implication" or "quasi-modal" is furthermore considered "post-classical"
or "quasi-classical".


Then, for solvers like those of the day, or Mizar or Metamath or
Coq given types or Lean or what, then there's probably still one
thing about "infinite-union" versus "pair-wise union", the illative
or univalent, with regards to a theory being a sort of, "heno-theory",
that is one theory and one model, then variously in perspective,
for example a set theory and/or a part theory, each of those
set up in universals.

This of course involves quantifier disambiguation for universals
and predicativity for universals and these kinds of things,
and the "extra-ordinary" as natural, vis-a-vis super _natural_,
and _super_ natural, natural.

You can find my podcasts I've setup an approach to nouveau mechanics,
and been getting into "Foundations" rather usually.

https://www.youtube.com/@rossfinlayson

So, modal and "thorough", relevance logic, given a deductive goal
to attain to to arrive at, makes for a "fuller dialectic" then
why inductive inference has that its partial and can't fulfill
itself, or after for example Goodman's "A Riddle of Induction",
then why "axiomless natural deduction" sorts out for a strong
mathematical platonism and strong (not weak) logicist positivism,
together, and first for a sort of, "axiomless geometry", via,
"axiomless natural deduction", since stipulations are unfounded.

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

Warm regards, Ross

[Julio Di Egidio]

Post by Ross Finlayson

Post by Julio Di Egidio
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

[Mild Shock]

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

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
```
?- solve_t.
- 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!
- 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
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```
-Julio

[Mild Shock]

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

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
notation(gliv(X), (~(~X)))

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
```
?- solve_t.
- 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!
- 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
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```
-Julio

[Mild Shock]

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?

Post by Mild Shock
But you will not immediately see the
difference. Since for tautologies, by
(~(~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.
https://www.leancop.de/ileansep/index.html#Source

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
notation(gliv(X), (~(~X)))

Post by Julio Di Egidio

Post by Mild Shock

Post by Julio Di Egidio

Post by Mild Shock
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
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
```
?- solve_t.
- 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!
- 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
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```
-Julio

[Julio Di Egidio]

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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

[Julio Di Egidio]

Post by Julio Di Egidio

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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...

Post by Julio Di Egidio
Here are lecture notes that maybe have a complete answer/recipe, see
<https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>
<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

[Mild Shock]

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

Post by Julio Di Egidio

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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
<https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
-Julio

[Mild Shock]

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 .

Post by Mild Shock
But in a linear logic you can do
    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.
https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical/intuitionistic_logic_in_linear_logic

Post by Julio Di Egidio

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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
<https://www.cs.cmu.edu/%7Efp/courses/15816-f16/lectures/27-classical.pdf>
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
-Julio

[Julio Di Egidio]

Post by Mild Shock
In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.
A o- A o- .. A o- B
\-- n times --/
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

[Mild Shock]

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

Post by Julio Di Egidio

Post by Mild Shock
In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.
A o- A o- .. A o- B
\-- n times --/
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

[Mild Shock]

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.

Post by Mild Shock
A o- A o- .. A o- B
\-- n times --/
Well I don't know an online affine logic prover.
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

Post by Julio Di Egidio

Post by Mild Shock
In affine logic you can possibly do something like iterative
deepening, only its iterative contraction.
A o- A o- .. A o- B
\-- n times --/
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

[Julio Di Egidio]

Post by Mild Shock
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

[Mild Shock]

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.

Post by Julio Di Egidio

Post by Mild Shock
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.

<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

[Julio Di Egidio]

Post by Mild Shock
"Type system" can be another word for "logic with
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

[Julio Di Egidio]

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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

[Mild Shock]

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?

Post by Julio Di Egidio
((p->q)->p)->p
Peirce law is not provable in minimal logic.
notation(dnt(X), ~X->(~(~X)))
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic
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

[Mild Shock]

Hi,
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>

Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

You can try searching here:

https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20

Post by Julio Di Egidio
Dear logicians,
How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?
  `(P -> Q -> R) |- (P /\ Q -> R)`
Thanks for any help.
-Julio

[Mild Shock]

Now if you want to join cstheory.stackexchange.com it
says Anybody can ask a question Anybody can answer
The best answers are voted up and rise to the top
It allows only questions that "can be discussed between
two professors or between two graduate students working
on Ph.D.'s, but not usually between a professor and a
typical undergraduate student".
https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed
I am not lying when I say even Andrej Bauer did
that. But how do you want to launch a proof assistants
site, I assume for everybody? if you cannot divert
cs theory questions to another stackexchange?
proof assistants are full of cs theory stuff.

Very problematic behaviour!

Mostowski Collapse - 29.11.2021, 00:19:03
https://groups.google.com/g/sci.logic/c/12DNbf3QI5I/m/V_Yal3wBBgAJ

Hi,
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.
https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20

Post by Julio Di Egidio
Dear logicians,
How to prove the following theorem with natural deduction in
intuitionistic propositional logic (namely, no classical inference rules)?
   `(P -> Q -> R) |- (P /\ Q -> R)`
Thanks for any help.
-Julio

[Julio Di Egidio]

Post by Julio Di Egidio
Hi,
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

Don't make it personal, a third of the world population is nazi-retarded
by now: the incivilization and involution is just like the Huns, not
even grass grows anymore.

It's a fucking shame for humanity: but there just seems to be no bottom
to it, it's like those rats on the boat, killing and shitting on all
intelligence and decency to begin with.

"Progress" is watch these nazi-retards play WW3, get some popcorn...


-Julio

[Mild Shock]

Its extremly personal, because SO and other
systems establish para-governemental prisons,
and mostly the reason is a form

of agile processes, agil forms of website
development, including the many "business rules"
that are involved in SO,

thats a very dangerous form of creating such
things, since it might violate existing law
which also applies to the digital.

P.S.: In a normal IT setting you have
subject matter experts that define "business
rules", such mechanisms should be a playground

for infantile developers with a mindset of a 5 year old.

Post by Julio Di Egidio

Post by Julio Di Egidio
Hi,
 >
<https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.

Don't make it personal, a third of the world population is nazi-retarded
by now: the incivilization and involution is just  like the Huns, not
even grass grows anymore.
It's a fucking shame for humanity: but there just seems to be no bottom
to it, it's like those rats on the boat, killing and shitting on all
intelligence and decency to begin with.
"Progress" is watch these nazi-retards play WW3, get some popcorn...
-Julio

[Mild Shock]

Post by Mild Shock
such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

Corr.:

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.

[Mild Shock]

One problem I generally see is, that most people
are not aware, that an employee has no rights
on the stuff he writes for his employer.

Standard Rules:
- Work for Hire Doctrine: In most jurisdictions, code
written by an employee within the scope of their employment is
considered a "work for hire," meaning the employer owns
the intellectual property (IP) unless otherwise agreed in writing.
- Employment Contracts: Most employment agreements
explicitly state that any code, inventions, or intellectual
property created as part of your job belongs to the employer.
- Use of Employer Resources: If an employee uses the
employer’s time, tools, or resources to create code, the employer
generally owns the resulting work.

Exceptions:
- Independent Work: If an employee writes code outside
working hours, without using company resources, and it’s
unrelated to their job, they may retain rights. Some
jurisdictions, like California, have laws (e.g., California Labor Code
§2870) protecting employees in such cases.
- Negotiated Agreements: If the employee has a specific
agreement (e.g., consulting or freelance arrangements),
ownership terms might differ.

So like 90% of the stackoverflow users cannot
go into an agreement individually, since they are
employed, with stackoverflow in that they would be
able to give a license to what they write.

Post by Mild Shock

Post by Mild Shock
such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.

[Mild Shock]

It could be that among the exceptions is
also certain academic work. So maybe
there are different rules for CSTHEORY,

that for SO. Which has different audience.
But especially SO is problematic, since
it adresses "developers", they start their site with:

"Every developer has a
tab open to Stack Overflow."
For over 15 years we’ve been the Q&A platform
of choice that millions of people visit every
month to ask questions, learn, and
share technical knowledge.
https://stackoverflow.com/

So what is really "muddled" is thery IP
theft. Although they offer stack overflow
for teams. But maybe there is another solution

to the dilemma, something inbetween and more
fluid. Like GitHub, where you easily switch back
and forth a repository from private to non-private.

It is probably part and parcel of their marketing
stategiy that they make it most difficult to get
control over your own IP. So as to move you into

stackoverflow for teams. Which is of course a
moronic idea that this would work. There are
quite a couple of alternatives around,

Scryer Prolog uses GitHub discussions. But GitHub
can be also extremly Nazi.

Post by Mild Shock
One problem I generally see is, that most people
are not aware, that an employee has no rights
on the stuff he writes for his employer.
- Work for Hire Doctrine: In most jurisdictions, code
written by an employee within the scope of their employment is
considered a "work for hire," meaning the employer owns
the intellectual property (IP) unless otherwise agreed in writing.
- Employment Contracts: Most employment agreements
explicitly state that any code, inventions, or intellectual
property created as part of your job belongs to the employer.
- Use of Employer Resources: If an employee uses the
employer’s time, tools, or resources to create code, the employer
generally owns the resulting work.
- Independent Work: If an employee writes code outside
working hours, without using company resources, and it’s
unrelated to their job, they may retain rights. Some
jurisdictions, like California, have laws (e.g., California Labor Code
§2870) protecting employees in such cases.
- Negotiated Agreements: If the employee has a specific
agreement (e.g., consulting or freelance arrangements),
ownership terms might differ.
So like 90% of the stackoverflow users cannot
go into an agreement individually, since they are
employed, with stackoverflow in that they would be
able to give a license to what they write.

Post by Mild Shock

Post by Mild Shock
such mechanisms should be a playground
for infantile developers with a mindset of a 5 year old.

such mechanisms should not be a playground
for infantile developers with a mindset of a 5 year old.