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: comp.lang.prolog Subject: French Philosophy in 2024 (Was: Minimal Logics in the 2020's: A Meteoric Rise) Date: Fri, 12 Jul 2024 11:27:02 +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: Fri, 12 Jul 2024 09:27:00 -0000 (UTC) Injection-Info: solani.org; logging-data="581975"; 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:VtsA7Ypfy7r9WGdOQeCIQF3oSjw= In-Reply-To: X-User-ID: eJwFwQkRwEAIBDBLfAtFDuxw/iU0gacmKxIZeHiqoitboPWZMdjfAO3mwY1BSXuv++sruxGSNcw7yWK/HzVWFV0= Bytes: 3746 Lines: 91 Hi, Now I had an extremly resilient correspondent, who wants to do proof extraction, but at the same time refuses to learn the Curry-Howard isomorphism. But its so easy, was just watching: Hyperon Session with Dr. Ben Goertzel https://www.youtube.com/watch?v=5Uy3j4WCiXQ At t=1853 he mentions C. S. Peirce thirdness, which you can use to explain the Curry-Howard isomorphism: 1 *\ Γ = Context | \ | * 3 t = λ-Expression | / 2 */ α = Type The above is a trikonic visualization of the judgement Γ |- t : α, applying the art of making three-fold divisions. But I guess C. S. Peirce is not read in France, since it requires English. Or maybe there is a french translation? Bye 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 >