Path: ...!3.eu.feeder.erje.net!feeder.erje.net!news2.arglkargh.de!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: sci.logic
Subject: Re: French Philosophy in 2024 (Was: Minimal Logics in the 2020's: A
 Meteoric Rise)
Date: Fri, 12 Jul 2024 11:37:14 +0200
Message-ID: <v6qtg8$hoo1$1@solani.org>
References: <v67685$6fr5$1@solani.org> <v6qsqm$hoan$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:37:12 -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:I6jKAC3v+emDp8B1QWBGkBYfyzA=
In-Reply-To: <v6qsqm$hoan$1@solani.org>
X-User-ID: eJwFwYEBwCAIA7CXpFBg54ja/09YQk/LU5HMoKgcGY6iWlixlnoHthofm+FXgFFTRcnREOx2kzXDN3g/Py8VDw==
Bytes: 4198
Lines: 109

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.
>