Re: Minimal Logics in the 2020's: A Meteoric Rise

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.