Path: ...!npeer.as286.net!npeer-ng0.as286.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: French Philosophy in 2024 (Was: Minimal Logics in the 2020's: A Meteoric Rise) Date: Fri, 12 Jul 2024 11:37:41 +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:37:39 -0000 (UTC) Injection-Info: solani.org; logging-data="582401"; 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:etKMfmgL6tIFZqKsHSROHLEzENU= X-User-ID: eJwFwQcBwEAIBDBL8HAMOYziX0ITiLGNq8EUh+tHQhTbJeDL0JRPqVrEpOmsqmM9YseJA/UcN3wTzzKB/QE/kxUD In-Reply-To: Bytes: 4698 Lines: 123 Hi, Actually thridness is not only the art of making three-fold divisions. Usually one aims a finding a 3 that is the relation between 1 and 2, so that we have this relation satisfied: 3(1, 2) Of course we can have the stance, and say that |- does that already. Only |- is highly ambigious, if you see Γ |- α you don't know what was the last inference rule applied. But for proof extraction you want exactly know that. Bye P.S.: And Peirce isn't wrong when he says thirdness is enough, just take set theory, which can do all of mathematics? Its based on this thirdness only: x ∈ y The set membership. But set membership is as ugly as |-, it also doesn't say why an element belongs to a set. LoL Mild Shock schrieb: > 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 >> >