Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock Newsgroups: sci.logic Subject: Re: Minimal Logics in the 2020's: A Meteoric Rise Date: Sun, 7 Jul 2024 23:05:25 +0200 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Sun, 7 Jul 2024 21:05:24 -0000 (UTC) Injection-Info: solani.org; logging-data="360728"; 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:eRkyWHzmtf3azli6bItQcyYePkM= In-Reply-To: X-User-ID: eJwNx0kBwDAIBEBLnAvIgST4l9DOb1zBOGFwmK9vXUq1WcFtO64vCuNMWViZCBmKk9y5C+0UVWJ5BaL/kPcBPJMUeg== Bytes: 3738 Lines: 84 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. >