Path: ...!feeds.phibee-telecom.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: The error in Jan von Platos presentation (Was: Minimal Logics in the
 2020's: A Meteoric Rise)
Date: Sat, 13 Jul 2024 10:31:38 +0200
Message-ID: <v6te19$j8a9$1@solani.org>
References: <v67685$6fr5$1@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:31:37 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="631113"; 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:rlTfRpknrQsMdB1LDl0K6R3Jpus=
X-User-ID: eJwVx8EVwCAIBNGWWGEXLUcS7L+EmDeXP3RBT4ao4Llpjl7HdsXG3VXquQiWG3Oo9oP0Hgbgd5jJKEz3bMT7ATV7FCc=
In-Reply-To: <v67685$6fr5$1@solani.org>
Bytes: 2059
Lines: 32

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.