Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
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: <v6qst4$hoan$2@solani.org>
References: <b406aa35-c39b-46f3-862f-1cc4b75143ae@googlegroups.com>
 <1b7ce2bd-722b-4c2e-b853-12fc2232752bn@googlegroups.com>
 <v6731e$6eft$1@solani.org>
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: <v6731e$6eft$1@solani.org>
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
>