Path: ...!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: Minimal Logics in the 2020's: A Meteoric Rise
Date: Fri, 5 Jul 2024 03:31:46 +0200
Message-ID: <v67ie3$6kgc$1@solani.org>
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, 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: <v67i45$6keq$1@solani.org>
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.
>>
>>
>