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

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.