Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock Newsgroups: sci.logic Subject: Minimal Logics in the 2020's: A Meteoric Rise Date: Fri, 5 Jul 2024 03:31:46 +0200 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 5 Jul 2024 01:31:47 -0000 (UTC) Injection-Info: solani.org; logging-data="217612"; 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:9OLZ6TufEJyg8l0nwSEuDgP1j9Y= X-User-ID: eJwNxskBwDAIA7CVEmOOjgMU9h+h1Usqdq2dpkZdXRLY6gdy/FggJ9Ph5N59J/4NM5dCjaq5LlUHHT0MfdEfRXQVhg== In-Reply-To: Bytes: 4279 Lines: 107 But minimal logic rejects Ex Falso Quodlibet. So you cannot prove in general: /* not provable in minimal logic */ A, ~A |- B % EFQ minimal logic is a paraconsistent and btw also a paracomplete logic. It also rejects: /* not provable in minimal logic */ |- ~A v A % LEM It has indeed a Meteoric Rise, you can check the growth of this Wikipedia page, 5 years or so ago, minial logic had only 1 page, https://en.wikipedia.org/wiki/Minimal_logic now its a dozen pages? Why is this so? Because Coq, Lean, Agda, etc.. are built on top of minimal logic? Mild Shock schrieb: > I minimal logic, if you define: > >    ~A := A => f > > You can already prove, thats just modus ponens: > >    A, ~A |- f > > Or if you want you can also prove, i.e. rephrase > it, with approproate introducton of a conjunction & > by Curry Howard inference rules for "products": > >    |- ~(A & ~A) > > Thats the law of non-contradiction: > > https://en.wikipedia.org/wiki/Law_of_noncontradiction > > Its hard wired into minimal logic. > > olcott schrieb: >> On 7/4/2024 5:03 PM, Mild Shock wrote: >>> 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. >> >> Prolog logic such that provable means true and false >> means unprovable is the key foundation of correct reasoning. >> >> It simply implicitly rejects expressions that would otherwise >> result in mathematical incompleteness as not truth bearers >> within its system. This is the way that correct reasoning >> actually works. >> >> When expressions of language are self-contradictory such >> that X and ~X cannot be proven within the system Prolog >> rejects X. Mathematical logic would conclude that the >> system is incomplete. >> >> >