Path: ...!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: Minimal Logics in the 2020's: A Meteoric Rise
Date: Sun, 7 Jul 2024 23:16:29 +0200
Message-ID: <v6f0jc$b0bc$3@solani.org>
References: <v67685$6fr5$1@solani.org> <v67ta1$6pt0$1@solani.org>
 <v6evuk$b08o$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 7 Jul 2024 21:16:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="360812"; 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:mprOUt07JVCz8AyM5PIvgHgcgss=
X-User-ID: eJwFwQkBwDAIA0BLKRAeOYUV/xJ2R/XjE+Z043Ltyn5RuXOqY8TieaezulCQxua7z+YOlRiDsFEaVK8J4AdTNhTa
In-Reply-To: <v6evuk$b08o$1@solani.org>
Bytes: 4551
Lines: 109

Hi,

This has only become talk of the town recently
under the heading of Constructive S4 Modal Logic
or CS4. It somehow demonstrates that prejudice

against computer science, like lambda calculus is
too abstract, is possibly unfounded. The challenge
would be to draw connections and foster inter-

disciplinary dialog. The next challenge would
be to distill a simple didactical extract of it
and draw road maps!

Categorical and Kripke Semantics for Constructive S4 Modal Logic
Alechina et al. - 2003
https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf

What they call fallible worlds, does Segerberg
1968 call abnormal worlds.

Bye

Mild Shock schrieb:
> Hi,
> 
> There are possibly issues of interdisciplinary
> work. For example Sorensen & Urzyczyn in their
> Lectures on the Curry-Howard Isomorphism say that
> the logic LP has no name in literature.
> 
> On the other hand Segerbergs paper, shows that
> a logic LP, in his labeling JP, that stems from
> accepting Peice's Law is equivalent to a logic
> accepting Curry's Refutation rule,
> 
> i.e the logic JE with:
> 
>       Γ, A => B |- A
>      -----------------
>           Γ |- A
> 
> But the logic JE also implies that LEM was added!
> 
> Bye
> 
> Mild Shock schrieb:
>> The meteoric rise of Curry-Howard isomorphism
>> and minimal logic, possibly because proof assistants
>> such as Lean, Agda, etc… all use it, is quite ironic,
>> in the light of this statement:
>>
>>  > Because of the vagueness of the notions of “constructive
>>  > proof”, “constructive operation”, the BHK-interpretation
>>  > has never become a versatile technical tool in the way
>>  > classical semantics has. Perhaps it is correct to say
>>  > that by most people the BHK-interpretation has never been
>>  > seen as an intuitionistic counterpart to classical semantics.
>>  > https://festschriften.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf
>>
>> Mild Shock schrieb:
>>> Could be a wake-up call this many participants
>>> already in the commitee, that the whole logic
>>> world was asleep for many years:
>>>
>>> Non-Classical Logics. Theory and Applications XI,
>>> 5-8 September 2024, Lodz (Poland)
>>> https://easychair.org/cfp/NCL24
>>>
>>> Why is Minimal Logic at the core of many things?
>>> Because it is the logic of Curry-Howard isomoprhism
>>> for symple types:
>>>
>>> ----------------
>>> Γ ∪ { A } ⊢ A
>>>
>>> Γ ∪ { A } ⊢ B
>>> ----------------
>>> Γ ⊢ A → B
>>>
>>> Γ ⊢ A → B           Δ ⊢ A
>>> ----------------------------
>>> Γ ∪ Δ ⊢ B
>>>
>>> And funny things can happen, especially when people
>>> hallucinate duality or think symmetry is given, for
>>> example in newer inventions such as λμ-calculus,
>>>
>>> but then omg ~~p => p is nevertheless not provable,
>>> because they forgot an inference rule. LoL
>>>
>>> Recommended reading so far:
>>>
>>> Propositional Logics Related to Heyting’s and Johansson’s
>>> February 2008 - Krister Segerberg
>>> https://www.researchgate.net/publication/228036664
>>>
>>> The Logic of Church and Curry
>>> Jonathan P. Seldin - 2009
>>> https://www.sciencedirect.com/handbook/handbook-of-the-history-of-logic/vol/5/suppl/C 
>>>
>>>
>>> Meanwhile I am going back to my tinkering with my
>>> Prolog system, which even provides a more primitive
>>> logic than minimal logic, pure Prolog is minimal
>>>
>>> logic without embedded implication.
>>
>