Path: ...!2.eu.feeder.erje.net!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: Re: The error in Jan von Platos presentation (Was: Minimal Logics in
 the 2020's: A Meteoric Rise)
Date: Sun, 14 Jul 2024 00:05:13 +0200
Message-ID: <v6utmn$icto$3@solani.org>
References: <v67685$6fr5$1@solani.org> <v6te19$j8a9$1@solani.org>
 <v6tfgh$j975$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 22:05:11 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="603064"; 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:bKLJFot3fMYrGRA1nFOKDGukPu4=
In-Reply-To: <v6tfgh$j975$2@solani.org>
X-User-ID: eJwNyMkRACEIBMCUVByOcBYG8g9hfXVVQ3Rr2VXoxWA01z2QT/R9R0yfjNx0KdBX2ONzWEdOJZnmp7zCqE2u+gFOLxZA
Bytes: 2628
Lines: 37

Rather read the original, von Plato
takes his wisdom from:

 > The single-succedent sequent calculus of proof
 > search of Table 4.1 is a relatively recent invention:
 > Building on the work of Albert Dragalin (1978) on the
 > invertibility of logical rules in sequent calculi,
 > Anne Troelstra worked out the details of the proof
 > theory of this `contraction-free' calculus in the
 > book Basic Proof Theorv (2000).

But the book by Troelstra (1939-2019) and
Schwichtenberg (1949 -), doesn’t contain a minimal
logic is decidable theorem, based on some “loop
checking”, as indicated by von Plato on page 78.

The problem situation is similar as in Prolog SLD
resolution, where S stands for selection function.
Since the (L=>) inference rule is not invertible, it
involves a selection function σ,

that picks the active formula:

Γ, A => B |- A      Γ, B |- C          A selection function σ did pick
------------------------------- (L=>)  A => B from the left hand side
             Γ, A => B |- C

One selection function might loop, another
selection function might not loop. In Jens Otten
ileansep.p through backtracking over the predicate
select/3 and iterative deepening all selections

are tried. To show unprovability you have to show
looping for all possible selection functions, which
is obviously less trivial than the “root-first proof
search” humbug from von Platos vegan products

store that offers “naturally growing trees”.