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: Minimal Logics in the 2020's: A Meteoric Rise
Date: Fri, 5 Jul 2024 00:03:51 +0200
Message-ID: <v67685$6fr5$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 4 Jul 2024 22:03:49 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="212837"; 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:oWzTJRmF4qSYyTdOuOUK/tfsH4c=
X-User-ID: eJwNycEBwCAIA8CVQJIA42gt+4/Q3vcYcj0JUeBwcN7qHKtu2jT/1SrsHbhDT1jwlZfPMkuprU90FqCKmvsBGSsTgg==
X-Mozilla-News-Host: news://news.solani.org:119
Bytes: 2266
Lines: 44

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.