Deutsch English Français Italiano |
<v67ta1$6pt0$1@solani.org> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!eternal-september.org!feeder3.eternal-september.org!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: Fri, 5 Jul 2024 06:37:22 +0200 Message-ID: <v67ta1$6pt0$1@solani.org> References: <v67685$6fr5$1@solani.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 5 Jul 2024 04:37:21 -0000 (UTC) Injection-Info: solani.org; logging-data="223136"; 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:WAhXvwzKDg4C7e5RPOl8zN84etk= In-Reply-To: <v67685$6fr5$1@solani.org> X-User-ID: eJwFwYEBwDAEBMCVgvdkHBX2H6F3bhR2gE74+vaMC5CWWzyiV1FXLbuORRKpD+/4bU3lfOLcMLZF5EBqfynZFFI= Bytes: 3123 Lines: 60 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.