Path: ...!news.nobody.at!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Re: The error in Jan von Platos presentation (Re: Minimal Logics in
 the 2020's: A Meteoric Rise)
Date: Sat, 13 Jul 2024 10:58:44 +0200
Message-ID: <v6tfk3$j975$3@solani.org>
References: <b406aa35-c39b-46f3-862f-1cc4b75143ae@googlegroups.com>
 <1b7ce2bd-722b-4c2e-b853-12fc2232752bn@googlegroups.com>
 <v6731e$6eft$1@solani.org> <v6te42$j8a9$2@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 13 Jul 2024 08:58:43 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="632037"; 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.18.2
Cancel-Lock: sha1:O8F9NgJodM93GvRW0Y5LbRfnbBs=
X-User-ID: eJwNyrEBACEIBLCVwAP0xwHk9h/h7VLEERq9LTzM6VTsbsU3g5NLanqvWw75rsaLT03aWMIuVx9U81A8CynhP1k3FeA=
In-Reply-To: <v6te42$j8a9$2@solani.org>
Bytes: 3531
Lines: 72

The error is here, taken from his Table 4.1:

A => B, Γ |- A    B, Γ |- C
---------------------------- L=>
      A => B, Γ |- C

When he halucinates duplication also
known as contraction:

 > The premisses are simpler than the condusion
 > in all the rules except possibly in the left
 > premiss of rule L=>. That is the only source
 > of non-termination. Rules other than L=> can
 > produce duplication, if an active formula had
 > another occurrence in the antecedent. This
 > source of duplication comes to an end.

But in backward search the looping is not
caused because of A => B or some such would be
duplicated. None of the L=> rule branches shows
some formula twice. The calculi of Gentzen are

usually already known that propositional proof
search for them can be implement contraction free,
this is not what causes looping. What causes the
looping is simply that the same sequent might

again, other rules then L=> are also not to blame
at all. Just make an example with A atomic, and
you get an infinite decend:

P => B, Γ |- P         B, Γ |- P
--------------------------------- (L=>)
.....
P => B, Γ |- P         B, Γ |- P
--------------------------------- (L=>)
P => B, Γ |- P

Mild Shock schrieb:
> The sad news is, the book is only
> worth some fire wood.
> 
> Plato (p. 83 of Elements of Logical Reasoning
> 
> Interestingly the book uses non-classical
> logic, since it says:
> 
>  > Sequent calculus offers a good possibility for
>  > exhaustive proof search in propositional logic:
>  > We can check through all the possibilities for
>  > malking a derivation. If none of them worked,
>  > i.e., if each had at least one branch in which
>  > no rule applied and no initial sequent was reached,
>  > the given sequent is underivable. The
>  > symbol |/-, is used for underivability.
> 
> And then it has unprovable:
> 
> c. |/- A v ~A
> 
> d. |/- ~~A => A
> 
> But mostlikely the book has a blind spot, some
> serious errors, or totally unfounded claims, since
> for example with such a calculus, the unprovability
> of Peirce’s Law cannot be shown so easily.
> 
> Exhaustive proof search will usually not terminate.
> There are some terminating calculi, like Dyckhoffs
> LJT, but a naive calculus based on Gentzens take
> will not terminate.
>