Path: ...!3.eu.feeder.erje.net!feeder.erje.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Does Jens Ottens Int-Prover also do the Repeat? (Was: Girards
 Exponentiation after Dragalins Implication)
Date: Sun, 1 Dec 2024 17:17:29 +0100
Message-ID: <vii26o$m0sn$1@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vihvl9$9568$1@solani.org>
 <vii0l0$m02t$1@solani.org> <vii13u$m07d$1@solani.org>
 <vii1hm$m0g5$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 Dec 2024 16:17:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="721815"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:ZycmudpupugrQq8vA8lpXZxwpbs=
X-User-ID: eJwFwQEBwCAMAzBLsLIW5Jxu+JfwJMFJazG58uULGxidhEu6Zndfxy51ee5T/hQxgFleDT7hbp1itNJn/HKbFf0=
In-Reply-To: <vii1hm$m0g5$1@solani.org>
Bytes: 6880
Lines: 180

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
========== REMAINDER OF ARTICLE TRUNCATED ==========