Re: The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise)

Hi,
I am not halucinating that Negri is nonsense:
This calculus does not terminate (e.g. on Peirce’s
formula). Negri [42] shows how to add a loop-checking
mechanism to ensure termination. The effect on complexity
isn’t yet clear; but the loop-checking is expensive.
Intuitionistic Decision Procedures since Gentzen
The Jägerfest - 2013
https://apt13.unibe.ch/slides/Dyckhoff.pdf
Bye
Mild Shock schrieb:

Hi,
 A few years ago I was impressed by
the output of either Negri or Plato,
or the two together.
 Now they are just an annoyance, all
they show is that they are neither talented
nor have sufficient training.
 Just have a look at:
  > Terminating intuitionistic calculus
 > Giulio Fellin and Sara Negri
 > https://philpapers.org/rec/FELATI
 Beside the too obvious creative idea and motive
behind it, it is most likely complete useless
nonsense. Already this presentation in the
 paper shows utter incompetence:
 Γ, A → B ⊢ A           Γ, A → B, B ⊢ Δ
----------------------------------------
            Γ, A → B  ⊢ Δ
 Everybody in the business knows that the
looping, resulting from the A → B copying,
is a fact. But can be reduced since the
 copying on the right hand side is not needed.
 Γ, A → B ⊢ A           Γ, B ⊢ Δ
--------------------------------
         Γ, A → B  ⊢ Δ
 The above variant is enough. Just like Dragalin
presented the calculus. I really wish people
would completely understand these master pieces,
 before they even touch multi consequent calculi:
 Mathematical Intuitionism: Introduction to Proof Theory
Albert Grigorevich Dragalin - 1988
https://www.amazon.com/dp/0821845209
 Contraction-Free Sequent Calculi for Intuitionistic Logic
Roy Dyckhoff - 1992
http://www.cs.cmu.edu/~fp//courses/atp/cmuonly/D92.pdf
 Whats the deeper semantic (sic!) explanation of the
two calculi GHPC and GCPC? I have a Kripke semantics
explanation in my notes, didn't release it yet.
 Have Fun!
 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.