> There are propositional systems with even smaller axioms, but those systems are not even based on modus ponens, e.g.: https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ .
So this is the linked single NAND axiom for propositional calculus by Stephen Wolfram: ((p·q)·r)·(p·((p·r)·p))=r My question is: how would this translate into Metamath? The set.mm database does not introduce the primitive "=" symbol until ax-6, so we are not allowed to use its properties at that stage. Given how Metamath works, my guess is that you'll need more than one "$a |-" statement anyway. Il Gio 6 Giu 2024, 03:32 [email protected] < [email protected]> ha scritto: > Meredith's axiom under https://us.metamath.org/mpeuni/meredith.html is a > minimal axiom (one out of seven) in the Hilbert system with operators {→,¬} > and modus ponens. > > Since 2021, assuming general correctness of Walsh's and Fitelson's paper > <http://fitelson.org/walsh.pdf> (which is still declared as under > review), it has been proven by exhaustive search that it is indeed not only > smallest-known, but minimal. > > In contrast, https://us.metamath.org/mpeuni/merco1.html is a minimal > axiom in the Hilbert system with operators { →, ⊥} and modus ponens. > > > Such things always depend on which operators and rule(s) of inference are > allowed. There are propositional systems with even smaller axioms, but > those systems are not even based on modus ponens, e.g.: > https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/. > (Note that all systems based on modus ponens must have formulas written in > terms of →.) > > I am researching systems of minimal axioms in terms of {→,¬} with open > access at https://github.com/xamidi/pmGenerator/discussions/2 in case you > are interested — you could even contribute to the project. On the project's > main page <https://github.com/xamidi/pmGenerator> I also wrote a few > things about Metamath's propositional system of set.mm, which I called > "Frege's calculus simplified by Łukasiewicz" due to its origin, and I used > it as a default system for my tool. > > > [email protected] schrieb am Donnerstag, 6. Juni 2024 um 02:37:03 > UTC+2: > >> In the discussion below, Samiro mentioned ~ retbwax1, which got me >> looking at >> ~ meredith and friends: >> >> https://groups.google.com/d/msgid/metamath/bc1cdba2626540ad8582917ddcec4d74%40rwth-aachen.de >> >> The comment in ~ meredith mentions that it's "thought to be the shortest >> possible axiom for propositional calculus", but then ~ merco1 and ~ >> merco2 go >> on to show ones that appear shorter. Does the ~ meredith comment still >> apply, >> and if so how is length of an axiom defined in this game? >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/90b6ca2b-f4d5-442e-890d-ae85bcea56e1n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/90b6ca2b-f4d5-442e-890d-ae85bcea56e1n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAPKSAW5oD62rvGSbcsL4eJHbdxiOh4GaSdf7Cqq8B8s7DFz4Vw%40mail.gmail.com.
