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

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog
Subject	Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise)
Date	2024-07-14 00:14 +0200
Message-ID	<v6uu7j$id7a$2@solani.org> (permalink)
References	(1 earlier) <1b7ce2bd-722b-4c2e-b853-12fc2232752bn@googlegroups.com> <v6731e$6eft$1@solani.org> <v6te42$j8a9$2@solani.org> <v6tfk3$j975$3@solani.org> <v6utmf$icto$2@solani.org>

Show all headers | View raw

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

Thread

Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-06-04 07:49 -0700
  Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-06-20 08:20 -0700
    Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-06-21 03:24 -0700
    Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-06-23 02:14 -0700
      Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-06-24 15:25 -0700
        Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-07-29 17:58 -0700
          Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-01 06:48 -0700
            Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-01 06:54 -0700
              Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-01 07:31 -0700
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-02 02:02 -0700
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-02 02:14 -0700
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-02 02:20 -0700
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-08-15 07:34 -0700
      Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-20 05:23 -0800
        Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-20 09:01 -0800
          Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-25 07:23 -0800
            Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-25 13:10 -0800
              Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-27 09:31 -0800
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-28 21:47 -0800
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-28 21:58 -0800
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-28 23:33 -0800
                Re: The road to Artificial Intelligence Mild Shock <bursejan@gmail.com> - 2023-11-30 15:43 -0800
      Zero Tokens comming out of me (Re: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-10-30 16:47 +0100
    FYI: New Journal NAI (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-11-06 17:18 +0100
      The Bee Clock Model (Re: FYI: New Journal NAI) Mild Shock <janburse@fastmail.fm> - 2024-11-06 17:41 +0100
    ChatGPT for the Flintstones: Bloomberg (Re: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-11-11 22:34 +0100
      Silicon Valley is the new Detroit (Re: ChatGPT for the Flintstones: Bloomberg) Mild Shock <janburse@fastmail.fm> - 2025-02-18 18:13 +0100
        Re: Silicon Valley is the new Detroit (Re: ChatGPT for the Flintstones: Bloomberg) Mild Shock <janburse@fastmail.fm> - 2025-02-18 18:14 +0100
  Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-07-04 23:09 +0200
    The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-05 03:52 +0200
      Re: The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-05 03:54 +0200
        Euklid: Am I a joke to you? (Re: The curse of Negri & Plato) Mild Shock <janburse@fastmail.fm> - 2024-07-13 08:21 +0200
    Re: Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-07-05 06:38 +0200
      Re: Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-07-07 23:13 +0200
        Re: Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-07-07 23:17 +0200
    French Philosophy in 2024 (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-12 11:27 +0200
      Re: French Philosophy in 2024 (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-12 11:37 +0200
        Corona isn't over 2024 (Was: French Philosophy in 2024) Mild Shock <janburse@fastmail.fm> - 2024-07-12 12:20 +0200
        Re: Corona isn't over 2024 (Was: French Philosophy in 2024) Mild Shock <janburse@fastmail.fm> - 2024-07-12 12:36 +0200
    The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-13 10:33 +0200
      Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-13 10:58 +0200
        Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-14 00:05 +0200
          Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-14 00:14 +0200
    Distinction between Computation & Derivation (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-22 12:55 +0200
    Prolegomena by Rappaport (Re: Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence)) Mild Shock <janburse@fastmail.fm> - 2024-07-31 22:15 +0200
      2nd Cognitive Turn ~~> no Bayesian Brain (Re: Prolegomena by Rappaport) Mild Shock <janburse@fastmail.fm> - 2024-08-03 22:50 +0200
        Ok I made a joke, sorry (e: 2nd Cognitive Turn ~~> no Bayesian Brain) Mild Shock <janburse@fastmail.fm> - 2024-08-03 23:29 +0200
          Re: Ok I made a joke, sorry (e: 2nd Cognitive Turn ~~> no Bayesian Brain) Mild Shock <janburse@fastmail.fm> - 2024-08-03 23:55 +0200
            bullshit bullshit bullshit (Re: Ok I made a joke, sorry) Mild Shock <janburse@fastmail.fm> - 2024-08-04 00:14 +0200
    The two rules (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-08-04 00:57 +0200
    "Emotional AI" and "Spiritual AI" (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-10-03 12:28 +0200
      Oh shit, too late! (Re: "Emotional AI" and "Spiritual AI" (Re: Minimal Logics in the 2020's: A Meteoric Rise)) Mild Shock <janburse@fastmail.fm> - 2024-10-03 12:40 +0200
  LLM and Prolog, a Marriage in Heaven? (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-08-04 22:10 +0200
    The anchoring problem in a real world philosopher (Was: LLM and Prolog, a Marriage in Heaven?) Mild Shock <janburse@fastmail.fm> - 2024-08-08 16:56 +0200
      Long life learning also for real world philosophers? (Re: The anchoring problem in a real world philosopher) Mild Shock <janburse@fastmail.fm> - 2024-08-08 17:18 +0200
  Prolog for the pre frontal context (PFC) (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-08-28 17:28 +0200
  Re: Prolog for the pre frontal cortex (PFC) (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-08-28 17:31 +0200
  No time for the hairdresser betweeen 09.06.2023 and 11.07.2024 (Re: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-09-01 16:43 +0200
  Holy Shit: AI is cheaper than Humans (Was: The road to Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-09-01 22:38 +0200
    AI robots from Disney (Was: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-01 23:17 +0200
      I can't stand Mira Murati's Eyewash (Was: AI robots from Disney (Was: Holy Shit: AI is cheaper than Humans)) Mild Shock <janburse@fastmail.fm> - 2024-09-03 12:01 +0200
        After blue, green why not start yellow (Re: I can't stand Mira Murati's Eyewash) Mild Shock <janburse@fastmail.fm> - 2024-09-03 17:56 +0200
          miramurati bye bye (Re: After blue, green why not start yellow) Mild Shock <janburse@fastmail.fm> - 2024-09-25 22:09 +0200
            Im memoriam Doug Lenant (1950 - 2023) (Re: miramurati bye bye) Mild Shock <janburse@fastmail.fm> - 2024-12-01 00:56 +0100
              2026 the Year Prolog **plonked** Itself [Strawberry Prolog is back] (Was: Im memoriam Doug Lenant (1950 - 2023)) Mild Shock <janburse@fastmail.fm> - 2026-02-04 02:20 +0100
                Spies and Playboys: Don't use insecure E-mail [https://www.jmail.world/ Example] Mild Shock <janburse@fastmail.fm> - 2026-02-04 11:19 +0100
                Some ANTHEM Cringe Nonsense [More Dead Horses] (Was: 2026 the Year Prolog **plonked** Itself [Strawberry Prolog is back]) Mild Shock <janburse@fastmail.fm> - 2026-02-05 09:53 +0100
                Gecode: Guns N' Roses - Dead Horse (Was: Some ANTHEM Cringe Nonsense [More Dead Horses]) Mild Shock <janburse@fastmail.fm> - 2026-02-05 10:21 +0100
                2026 the Year golang lost its Marbles (Was: 2026 the Year Prolog **plonked** Itself [Strawberry Prolog is back]) Mild Shock <janburse@fastmail.fm> - 2026-02-14 09:53 +0100
                Mark V. Shaney caused Julio Di Egidio Suicide (Re: 2026 the Year golang lost its Marble) Mild Shock <janburse@fastmail.fm> - 2026-02-14 12:51 +0100
                Is Causal AI simply ReLU (Geoffrey E. Hinton 2010) (Re: Mark V. Shaney caused Julio Di Egidio Suicide) Mild Shock <janburse@fastmail.fm> - 2026-02-17 11:37 +0100
                Gen Alpha will grow up with Causal AI (Was: Is Causal AI simply ReLU (Geoffrey E. Hinton 2010)) Mild Shock <janburse@fastmail.fm> - 2026-02-19 20:00 +0100
                LRM moving from FOM to TCS [Lean Prover] (Was: Is Causal AI simply ReLU (Geoffrey E. Hinton 2010))) Mild Shock <janburse@fastmail.fm> - 2026-02-27 10:20 +0100
                Original Subject established by Chinese Scientists [Extenics] (Re: LRM moving from FOM to TCS [Lean Prover]) Mild Shock <janburse@fastmail.fm> - 2026-02-28 16:36 +0100
                DeepSeekMath: From psychophysischer Parallelismus to GPRO (Re: Odysseus PTSD: Does Function need Consistency?) Mild Shock <janburse@fastmail.fm> - 2026-03-06 02:29 +0100
            "superhumaness" excels "stackoverflow reputation" (Was: Im memoriam Doug Lenant (1950 - 2023) Mild Shock <janburse@fastmail.fm> - 2024-12-01 01:08 +0100
              para-governemental institution of violence (Re: "superhumaness" excels "stackoverflow reputation") Mild Shock <janburse@fastmail.fm> - 2024-12-01 11:42 +0100
              Not only $TSLA is on fire sale! [The Decline of Prolog] (Was: "superhumaness" excels "stackoverflow reputation") Mild Shock <janburse@fastmail.fm> - 2025-03-14 13:37 +0100
                Re: Not only $TSLA is on fire sale! [The Decline of Prolog] (Was: "superhumaness" excels "stackoverflow reputation") Mild Shock <janburse@fastmail.fm> - 2025-03-14 14:06 +0100
                Splitting up the Prologue to Prolog Mild Shock <janburse@fastmail.fm> - 2025-05-19 10:54 +0200
    Safe Superintelligence (SSI): Now they are dancing Mild Shock <janburse@fastmail.fm> - 2024-09-05 19:51 +0200
      Re: Safe Superintelligence (SSI): Now they are dancing Mild Shock <janburse@fastmail.fm> - 2024-09-05 23:51 +0200
        Salem Aleikum: Maxwella's Equations Mild Shock <janburse@fastmail.fm> - 2024-09-09 13:15 +0200
          non judicium, sed latrocinium (Re: Salem Aleikum: Maxwella's Equations) Mild Shock <janburse@fastmail.fm> - 2024-09-10 08:58 +0200
        Internet was made for cats (Re: Safe Superintelligence (SSI): Now they are dancing) Mild Shock <janburse@fastmail.fm> - 2024-09-13 12:58 +0200
          I was there, 3000 years ago (Re: Internet was made for cats) Mild Shock <janburse@fastmail.fm> - 2024-09-13 13:01 +0200
            Even Haitians are now voting for Trump (Re: I was there, 3000 years ago (Re: Internet was made for cats)) Mild Shock <janburse@fastmail.fm> - 2024-09-13 13:04 +0200
          supply chain attack (Was: Internet was made for cats( Mild Shock <janburse@fastmail.fm> - 2024-09-17 22:18 +0200
            Polyfill Supply Chain Attack (Was: supply chain attack) Mild Shock <janburse@fastmail.fm> - 2024-10-11 09:12 +0200
    USA is shitting its pants (Was: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-16 00:20 +0200
      scryer prolog is dead, BILAI instead? (Was: USA is shitting its pants) Mild Shock <janburse@fastmail.fm> - 2024-09-18 15:45 +0200
        Microsoft is plagiarizing my Invention [LLMs under the hood] Mild Shock <janburse@fastmail.fm> - 2024-10-08 16:00 +0200
          Geoffrey Hinton / Nobelpreis für Physik [Re: Microsoft is plagiarizing my Invention [LLMs under the hood]] Mild Shock <janburse@fastmail.fm> - 2024-10-08 16:03 +0200
        thank you for the FLOPs (Was: scryer prolog is dead, BILAI instead?) Mild Shock <janburse@fastmail.fm> - 2024-12-01 14:34 +0100
          Is old school mode directed compilation dead? (Was: thank you for the FLOPs) Mild Shock <janburse@fastmail.fm> - 2025-01-24 17:57 +0100
            Re: Is old school mode directed compilation dead? (Was: thank you for the FLOPs) Mild Shock <janburse@fastmail.fm> - 2025-01-24 17:58 +0100
              format/2 doesn't agree with Trealla or SWI (Was: Is old school mode directed compilation dead?) Mild Shock <janburse@fastmail.fm> - 2025-01-25 14:13 +0100
              DCG Translation with Unification Spillling (Was: Is old school mode directed compilation dead?) Mild Shock <janburse@fastmail.fm> - 2025-01-25 20:44 +0100
                Re: DCG Translation with Unification Spillling (Was: Is old school mode directed compilation dead?) Mild Shock <janburse@fastmail.fm> - 2025-01-25 20:44 +0100
          Will WASM be fast some time? (Was: thank you for the FLOPs) Mild Shock <janburse@fastmail.fm> - 2025-03-04 10:09 +0100
            Re: Will WASM be fast some time? (Was: thank you for the FLOPs) Mild Shock <janburse@fastmail.fm> - 2025-03-04 10:13 +0100
      Book Project: WomanLogic (Re: USA is shitting its pants) Mild Shock <janburse@fastmail.fm> - 2024-11-14 22:25 +0100
        Re: Book Project: WomanLogic (Re: USA is shitting its pants) Mild Shock <janburse@fastmail.fm> - 2024-11-14 22:26 +0100
  Happy Birthday 75 Years of Artificial Intelligence Mild Shock <janburse@fastmail.fm> - 2024-10-23 01:18 +0200
    Does ChatGPT know the difference between "k" and "kkkkkkkkkk"? Mild Shock <janburse@fastmail.fm> - 2024-10-23 01:18 +0200
    What is it like to be a Bat? Mild Shock <janburse@fastmail.fm> - 2024-10-23 22:35 +0200
      How Monkeys see the World (Re: What is it like to be a Bat?) Mild Shock <janburse@fastmail.fm> - 2024-10-23 22:45 +0200
    Low-Code Penetration Prediction (Re: Happy Birthday 75 Years of Artificial Intelligence) Mild Shock <janburse@fastmail.fm> - 2024-10-30 23:09 +0100

csiph-web