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

Even Dyckhoffs calculus LJT has (L=>=>) not
invertible and is still bugged by a selection
function dependency. Because of this complication
minimal logic calculi have traditionally been shown
decidable not by means of proof theory but
rather by means of model theory. You can look up
modal companions and then draw upon some finite
model upper bound. The seminal paper is:
 > Propositional Dynamic Logic of Regular Programs
 > Fischer & Ladner - 1979
 > https://www.sciencedirect.com/science/article/pii/0022000079900461
It contains the modal logic S4 as a special case:
 > The modal systems K, T, S4, S5 (cf. Ladner [16]) are
 > recognizable subsystems of propositional dynamic logic.
 >
 > K allows only the modality A,
 > T allows only the modality A u λ,
 > S4 allows ordy the modality A*,
 > S5 allows only the modality (A u A-)*.
Mild Shock schrieb:

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