Path: ...!2.eu.feeder.erje.net!feeder.erje.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock Newsgroups: comp.lang.prolog Subject: Re: Minimal Logics in the 2020's: A Meteoric Rise (Was: The road to Artificial Intelligence) Date: Sun, 7 Jul 2024 23:13:18 +0200 Message-ID: References: <1b7ce2bd-722b-4c2e-b853-12fc2232752bn@googlegroups.com> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Sun, 7 Jul 2024 21:13:16 -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:m3+5mhIABQlKOqcAtS2kTjimuYs= X-User-ID: eJwNyckBACAIA7CVQGnVceTafwT9JphUxjKChkYfXKSHiTl0/BuyD3x5kNxTJDmqZ6aEVt1PW6vFjxe6Mx48ShW+ In-Reply-To: Bytes: 4336 Lines: 98 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. >> >> Mild Shock schrieb: >>> >>> Your new Scrum Master is here! - ChatGPT, 2023 >>> https://www.bbntimes.com/companies/ai-will-make-agile-coaches-and-scrum-masters-redundant-in-less-than-2-years >>> >>> >>> LoL >>> >>> Thomas Alva Edison schrieb am Dienstag, 10. Juli 2018 um 15:28:05 UTC+2: >>>> Prolog Class Signpost - American Style 2018 >>>> https://www.youtube.com/watch?v=CxQKltWI0NA >> >