Sujet : Re: Minimal Logics in the 2020's: A Meteoric Rise
De : polcott333 (at) *nospam* gmail.com (olcott)
Groupes : sci.logicDate : 05. Jul 2024, 02:46:17
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <v67j9a$2vtu0$2@dont-email.me>
References : 1 2 3
User-Agent : Mozilla Thunderbird
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; Geniushits a target no one else can see." Arthur Schopenhauer