Deutsch English Français Italiano |
<v67k2b$6l2j$2@solani.org> View for Bookmarking (what is this?) Look up another Usenet article |
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: sci.logic Subject: The curse of Negri & Plato (Was: Minimal Logics in the 2020's: A Meteoric Rise) Date: Fri, 5 Jul 2024 03:59:39 +0200 Message-ID: <v67k2b$6l2j$2@solani.org> References: <v67685$6fr5$1@solani.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 5 Jul 2024 01:59:39 -0000 (UTC) Injection-Info: solani.org; logging-data="218195"; 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:w0ZuvTybA4IYJo3mPiCFXVs6zbg= In-Reply-To: <v67685$6fr5$1@solani.org> X-User-ID: eJwNykkBwDAIBEBLULIE5HD6l5DOeyDKWvco9GCxMibXBkXBniR+vqZkLybegY5s9387jMJUA4GczXKZaK4HS0MWFw== Bytes: 4090 Lines: 103 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.