Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.math |
| Subject | Re: Minimal Logics in the 2020's: A Meteoric Rise |
| Date | 2024-07-07 23:18 +0200 |
| Message-ID | <v6f0nb$b0bc$5@solani.org> (permalink) |
| References | <v676ba$6fr5$2@solani.org> <v67u1d$6q8s$3@solani.org> <v6f08h$b0bc$1@solani.org> |
Hi,
This has only become talk of the town recently
under the heading of Constructive S4 Modal Logic
or CS4. It somehow demonstrates that prejudice
against computer science, like lambda calculus is
too abstract, is possibly unfounded. The challenge
would be to draw connections and foster inter-
disciplinary dialog. The next challenge would
be to distill a simple didactical extract of it
and draw road maps!
Categorical and Kripke Semantics for Constructive S4 Modal Logic
Alechina et al. - 2003
https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf
What they call fallible worlds, does Segerberg
1968 call abnormal worlds.
Bye
Mild Shock schrieb:
> 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 isomorphism
>>> for simple 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.
>>
>
Back to sci.math | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-05 00:05 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise sobriquet <dohduhdah@yahoo.com> - 2024-07-05 03:50 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-05 04:06 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise sobriquet <dohduhdah@yahoo.com> - 2024-07-05 05:24 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-05 06:47 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-05 06:48 +0200
The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-05 04:07 +0200
Re: The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-05 04:08 +0200
Euklid: Am I a joke to you? (Re: The curse of Negri & Plato) Mild Shock <janburse@fastmail.fm> - 2024-07-13 08:18 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-05 06:49 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-07 23:10 +0200
Re: Minimal Logics in the 2020's: A Meteoric Rise Mild Shock <janburse@fastmail.fm> - 2024-07-07 23:18 +0200
French Philosophy in 2024 (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-12 11:30 +0200
Re: French Philosophy in 2024 (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-12 11:38 +0200
Corona isn't over 2024 (Was: French Philosophy in 2024) Mild Shock <janburse@fastmail.fm> - 2024-07-12 12:23 +0200
Re: Corona isn't over 2024 (Was: French Philosophy in 2024) Mild Shock <janburse@fastmail.fm> - 2024-07-12 12:36 +0200
The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-13 10:33 +0200
Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-13 10:56 +0200
Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-14 00:04 +0200
Re: The error in Jan von Platos presentation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-14 00:14 +0200
Distinction between Computation & Derivation (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-22 12:58 +0200
Prolegomena by Rappaport (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-07-31 22:16 +0200
2nd Cognitive Turn ~~> no Bayesian Brain (Re: Prolegomena by Rappaport) Mild Shock <janburse@fastmail.fm> - 2024-08-03 22:51 +0200
Ok I made a joke, sorry (Re: 2nd Cognitive Turn ~~> no Bayesian Brain) Mild Shock <janburse@fastmail.fm> - 2024-08-03 23:48 +0200
Re: Ok I made a joke, sorry (Re: 2nd Cognitive Turn ~~> no Bayesian Brain) Mild Shock <janburse@fastmail.fm> - 2024-08-04 00:00 +0200
bullshit bullshit bullshit (Was: Ok I made a joke, sorry) Mild Shock <janburse@fastmail.fm> - 2024-08-04 00:13 +0200
The two rules (Was: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-08-04 00:58 +0200
Re: The two rules (Was: Minimal Logics in the 2020's: A Meteoric Rise) Moebius <invalid@example.invalid> - 2024-08-04 01:45 +0200
The anchoring problem in a real world philosopher (Re: LLM and Prolog, a Marriage in Heaven?) Mild Shock <janburse@fastmail.fm> - 2024-08-08 17:11 +0200
Long life learning also for real world philosophers? (Re: The anchoring problem in a real world philosopher) Mild Shock <janburse@fastmail.fm> - 2024-08-08 17:19 +0200
Prolog for the pre frontal cortex (PFC) (Was: LLM and Prolog, a Marriage in Heaven?) Mild Shock <janburse@fastmail.fm> - 2024-08-28 20:46 +0200
Holy Shit: AI is cheaper than Humans (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-09-01 22:38 +0200
AI robots from Disney (Re: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-01 23:20 +0200
Re: Holy Shit: AI is cheaper than Humans (Re: Minimal Logics in the 2020's: A Meteoric Rise) Jim Burns <james.g.burns@att.net> - 2024-09-02 09:32 -0400
Re: Holy Shit: AI is cheaper than Humans (Re: Minimal Logics in the 2020's: A Meteoric Rise) Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-09-02 09:30 -0700
There is only a nature article about "low carbon emission" (Was: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-02 19:02 +0200
I can't stand Mira Murati's Eyewash (Re: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-03 12:03 +0200
After blue, green why not start yellow (Re: I can't stand Mira Murati's Eyewash) Mild Shock <janburse@fastmail.fm> - 2024-09-03 17:58 +0200
miramurati bye bye (Re: After blue, green why not start yellow) Mild Shock <janburse@fastmail.fm> - 2024-09-25 22:10 +0200
Safe Superintelligence (SSI): Now they are dancing Mild Shock <janburse@fastmail.fm> - 2024-09-05 19:52 +0200
Re: Safe Superintelligence (SSI): Now they are dancing Mild Shock <janburse@fastmail.fm> - 2024-09-05 23:52 +0200
Salem Aleikum: Maxwella's Equations (Re: Safe Superintelligence (SSI): Now they are dancing) Mild Shock <janburse@fastmail.fm> - 2024-09-09 13:20 +0200
non judicium, sed latrocinium (Re: Salem Aleikum: Maxwella's Equations) Mild Shock <janburse@fastmail.fm> - 2024-09-10 08:57 +0200
Internet was made for cats (Was: Safe Superintelligence (SSI): Now they are dancing) Mild Shock <janburse@fastmail.fm> - 2024-09-11 20:11 +0200
I was there, 3000 years ago (Re: Internet was made for cats) Mild Shock <janburse@fastmail.fm> - 2024-09-13 13:00 +0200
Even Haitians are now voting for Trump (Re: I was there, 3000 years ago (Re: Internet was made for cats)) Mild Shock <janburse@fastmail.fm> - 2024-09-13 13:03 +0200
supply chain attack (Re: Internet was made for cats) Mild Shock <janburse@fastmail.fm> - 2024-09-17 22:19 +0200
Polyfill Supply Chain Attack (Re: supply chain attack) Mild Shock <janburse@fastmail.fm> - 2024-10-11 09:13 +0200
USA is shitting its pants (Re: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-16 00:23 +0200
scryer prolog is dead, BILAI instead? Re: USA is shitting its pants (Re: Holy Shit: AI is cheaper than Humans) Mild Shock <janburse@fastmail.fm> - 2024-09-18 15:44 +0200
Microsoft is plagiarizing my Invention [LLMs under the hood] Mild Shock <janburse@fastmail.fm> - 2024-10-08 16:06 +0200
Geoffrey Hinton / Nobelpreis für Physik [Re: Microsoft is plagiarizing my Invention [LLMs under the hood]] Mild Shock <janburse@fastmail.fm> - 2024-10-08 16:06 +0200
"Emotional AI" and "Spiritual AI" (Re: Minimal Logics in the 2020's: A Meteoric Rise) Mild Shock <janburse@fastmail.fm> - 2024-10-03 12:29 +0200
Oh shit, too late! (Re: "Emotional AI" and "Spiritual AI" (Re: Minimal Logics in the 2020's: A Meteoric Rise)) Mild Shock <janburse@fastmail.fm> - 2024-10-03 12:41 +0200
csiph-web