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 <janburse@fastmail.fm>
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: <v6f0dc$b0bc$2@solani.org>
References: <b406aa35-c39b-46f3-862f-1cc4b75143ae@googlegroups.com>
 <1b7ce2bd-722b-4c2e-b853-12fc2232752bn@googlegroups.com>
 <v6731e$6eft$1@solani.org> <v67tb8$6pt0$2@solani.org>
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: <v67tb8$6pt0$2@solani.org>
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
>>
>