Deutsch English Français Italiano |
<v67j9a$2vtu0$2@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: olcott <polcott333@gmail.com> Newsgroups: sci.logic Subject: Re: Minimal Logics in the 2020's: A Meteoric Rise Date: Thu, 4 Jul 2024 20:46:17 -0500 Organization: A noiseless patient Spider Lines: 95 Message-ID: <v67j9a$2vtu0$2@dont-email.me> References: <v67685$6fr5$1@solani.org> <v676rf$2u7lu$1@dont-email.me> <v67i45$6keq$1@solani.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 05 Jul 2024 03:46:18 +0200 (CEST) Injection-Info: dont-email.me; posting-host="f325a973008a37eaa6ec545239278e3d"; logging-data="3143616"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX187s/lJC1aAmbBoAvS2ALFf" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:4U9RdUHoLRI6bYx81bxksWSWBEo= Content-Language: en-US In-Reply-To: <v67i45$6keq$1@solani.org> Bytes: 4043 On 7/4/2024 8:26 PM, Mild Shock wrote: > 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. > When provable means true and false means unprovable then (Γ ⊢ X) means X is true in Γ. then (Γ ⊢ ~X) means X is conventional false in Γ. the (Γ ⊬ X) ∧ (Γ ⊬ ~X) X is not a truth bearer in Γ. > 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. >> >> > -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer