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: Re: The error in Jan von Platos presentation (Was: Minimal Logics in
 the 2020's: A Meteoric Rise)
Date: Sun, 14 Jul 2024 00:13:50 +0200
Message-ID: <v6uu6t$id7a$1@solani.org>
References: <v67685$6fr5$1@solani.org> <v6te19$j8a9$1@solani.org>
 <v6tfgh$j975$2@solani.org> <v6utmn$icto$3@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:13:49 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="603370"; 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:zRZ6SfUeW2hBxSyxiMWSYi14llI=
In-Reply-To: <v6utmn$icto$3@solani.org>
X-User-ID: eJwFwQkBwDAIA0BLPE0YcmgB/xJ2B6fyxSF4sFhRytZVbKDt3oi2qfUvX9kIRsWyK3Kk5IsKCL39cQ6zyR9Y7BVe
Bytes: 3609
Lines: 63

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