Re: The error in Jan von Platos presentation (Was: Minimal Logics in the 2020's: A Meteoric Rise)

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”.