Does Jens Ottens Int-Prover also do the Repeat? (Was: Girards Exponentiation after Dragalins Implication)

Hi
Interesting question whether Jens Ottens Int-Prover
does also the repeat. I find in Jens Ottens Int-Prover
that he does indeed also do the repeat for
intuitionistic implication:

What is ileanSeP?
ileanSeP is a Prolog program that implements a very
compact theorem prover for first-order intuitionistic
logic. It is based on a single-succedent intuitionistic
sequent calculus very similar to Gentzen's LJ.
https://www.leancop.de/ileansep/
 From his source code ileansep_swi.pl (SWI-Prolog, 3 kbytes).
His tabular prover definition defines copying in the
last two columns. Copying is more critical when you
do first order logic the way Jens Otten usually does it:
fml((A=>B), 1,nin,[(A=>B)],         [C],[D],[], _, _,[!],A:B,C:D).
In propositional logic you don't need copying only
repeating, so if we would strip down Jens Ottens prover
to propositional logic, we could go with:
fml((A=>B), 1,nin,[(A=>B)],         [A],[B],[], _, _,[!],[],[]).
The result will then be the same repeat as in Dragalins
implication. What I am not aware whether Jens Otten published
some prover for Linear Logic. Who knows, maybe?
Bye
Mild Shock schrieb:

Hi,
 Linear logic you can of course do the following,
and define intuitionistic implication as follows:
 A -> B := ! A -o B
 Girards Exponention will do the repeating for you,
that is found in Dragalins Implication.
 I don't know how to incorporate the same into your Prolog code.
 Bye
 Mild Shock schrieb:

You see this behaviour here in the graphic
I posted with the answer on proofassistants.stackexchange.com:
>
Something tells me Glivenko theorem would need at least
intuitionistic logic, to prove for example Peirce law (*):
https://i.sstatic.net/lGQ8Iur9.png
>
The (L->) rule is applied twice, to prove
Pierce Law via Glivenko. You can only apply (L->)
twice if you implement Dragalins variant that
>
keeps X->Y in the right branch of then (L->) rule.
If you don't implement Dragalins implication, i.e.
if you don't implement intuitistic implication in
>
your Prolog code, I guess there is no chance for
Glivenkos theorem. You will be pretty much on your
own in a totally different terrain.
>
Mild Shock schrieb:

Hi,
>
This inference rule is incorrect:
>
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
     nth1(H, C0, (X->Y), C1),
     append(C1, [Y], C2),
     Gs = [C1=>X,C2=>Z],
     Ps = [H:X,H:Y].
>
The correct one would be, X->Y has to
be repeated in the left proof branch:
>
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
... put your prolog code here ...
>
Then you can only possibly prove Pierce Law
with Glivenko. Otherwise there is no chance.
>
See also here:
>
Mathematical Intuitionism: Introduction to Proof Theory
A. G. Dragalin
§3 THE SEQUENT CALCULUS - Page 11
The calculus GHPC
https://bookstore.ams.org/MMONO/67
>
Good Luck!
>
Bye
>
Mild Shock schrieb:

And what are the results? Your gist shows
this one here:
>
% Peirce's law:
solve_case(neg, pierce, [(p->q)->p]=>p).
>
And you reported:
>
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
>
What do you get with gliv/1?
>
Julio Di Egidio schrieb:

On 01/12/2024 15:32, Mild Shock wrote:
>
 > So although it was very temping to download
 > you software, and then replace these line:
 > <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
 > By these line:
 > notation(gliv(X), (~(~X)))
 > solve_t__sel(neg, C=>X) :-
 >     solve(C=>gliv(X)).
>
Or just change the definition of `dnt`, or create another one.  The code is functional and pretty flexible actually, `notation/5` is `multifile`.
>
 > I am afraid I have no time for that. You
 > could do it by yourself. Or what
>
I have already done it, and I have already told you the results! You have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's just me, you, and Ross once a month...
>
---
>
Here is an interesting new case, which I had thought should be *unsolvable*:
>
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !.  % DNE<->LEM
```
>
Unsolvable not just because my logic is *affine*, but because the actual statement, provable intuitionistically, is intrinsically higher-order:
>
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
>
while the statement I am proving above is this one, and it is not intuitionistically provable (AFAICT):
>
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
>
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... which is why I am also developing a meta-theory for it, in Coq:
>
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v> >
>
-Julio

>

>

>