> he stated that his axiom has 15 symbols Upon rereading Wolfram's articles (including https://www.wolfram.com/language/12/algebraic-computation/the-shortest-possible-axiom-for-boolean-logic.html), I couldn't even confirm this (I read them several years ago). Claiming that one found "The Shortest Possible Axiom for Boolean Logic" without even stating for which rules of inference and how long the axiom is and by which metric seems rather chaotic and bold..
But the metric I assumed is used here: https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf On page 3, Wolfram's single axiom is denoted as (Sh₁), and they write: > Equation (Sh₁) is a member of a list of 25 candidates sent to us by Stephen Wolfram [17], who asked whether Otter could prove any of the candidates to be single axioms. [...] > In Section 4 we show that (Sh₁), *which has length 15*, is a shortest single axiom in terms of the Sheffer stroke, and in Section 5 we narrow the list of possible length-15 Sheffer axioms to 16 candidates." You could read that paper and references in order to understand what these systems really are. [email protected] schrieb am Donnerstag, 6. Juni 2024 um 17:32:12 UTC+2: > > This is what makes me skeptical. > > > And rightfully so. These kind of systems with weird rules are a thing, as > you can see for example at > https://web.ics.purdue.edu/~dulrich/Twenty-six-open-questions-page.htm > (where NAND is calleld "Sheffer's joint-denial operator") or > https://en.wikipedia.org/wiki/Nicod%27s_axiom (which mentions a rule "Nicod's > modus ponens"), but rules should indeed always be stated explicitly. > Wolfram's article wouldn't pass peer review without modifications. > > > > Thierry second interpretation makes more sense to me. > > > But that one is definitely false since a rule with more than 0 premises is > not an axiom, and furthermore he stated that his axiom has 15 symbols, i.e. > "=" is a single operator. > > Moreover, the point was to state a single-axiom system. But given that for > handing both '<->' and '-/\' you most likely need multiple rules, the > whole approach is moot. Since when using multiple rules you do not need > *any* axioms for propositional logic (as we know, for example, from natural > deduction systems). > > > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag von > Gino Giotto <[email protected]> > *Gesendet:* Donnerstag, 6. Juni 2024 17:16:50 > *An:* Metamath > > *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional > calculus > > Whichever rule(s) Stephen Wolfram's system implicitly use(s), he > didn't even write them down explicitly — apparently not aware that this is > important, but possibly hiding the actual complex definition of the system. > > This is what makes me skeptical. By reading his post, he claims that his > axiom is all you need, but this doesn't look right to me. Let's assume that > his "=" is really the same thing as the metamath "<-> " and go forward > to prove all true propositional statements. Now let's say I want to prove > the simple tautology "|- ( ph -/\ ( ph -/\ ph ) )", to me it's > immediately noticeable that this is impossible (in metamath), unless you > add a rule of inference or other shorter axioms (in metamath there is no > way to unify a goal with a statement that has more symbols than it). > > Thierry second interpretation makes more sense to me. His "=" is not > really the set.mm "<-> ", but rather a bidirectional version of our "⇒", > which is the symbol the website uses to express the relashionship between > hypothesis and conclusion (e.g. ax-mp: ⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓). In > this interpretation his system would be composed of two rules of inferences > and no axioms. > Il giorno giovedì 6 giugno 2024 alle 16:27:28 UTC+2 > [email protected] ha scritto: > >> Corrections: >> >> >> "Whichever rule(s) Stephen Wolfram's systems implicitly use [...] His >> minimal axiom written", >> "|- ( ( ( ( ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph ) ) ) <-> >> ch )", >> >> "⊢(((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ)" >> ------------------------------ >> *Von:* [email protected] <[email protected]> im Auftrag >> von Discher, Samiro <[email protected]> >> *Gesendet:* Donnerstag, 6. Juni 2024 16:18:52 >> *An:* Gino Giotto; [email protected] >> *Betreff:* AW: [Metamath] Re: Shortest possible axiom for propositional >> calculus >> >> I don't like NAND-based systems because they tend to have rather >> complicated rules of inference (which doesn't make them look fundamental, >> which is the whole point of single-axiom systems). >> Whichever rule(s) Stephen Wolfram's system implicitly use(s), he didn't >> even write them down explicitly — apparently not aware that this is >> important, but possibly hiding the actual complex definition of the system. >> >> His axiom written in Metamath's language is simply >> >> |- (((ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph))) <-> ch >> >> in ASCII tokens (https://us.metamath.org/mpeuni/mmascii.html), or >> >> ⊢((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ >> >> in Unicode symbols. >> >> ------------------------------ >> *Von:* 'Thierry Arnoux' via Metamath <[email protected]> >> *Gesendet:* Donnerstag, 6. Juni 2024 11:42:40 >> *An:* [email protected]; Gino Giotto >> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional >> calculus >> >> >> The `=` sign here is set.mm's biconditional `<->`and we would probably >> count it as a second operation, which needs to be defined, etc. >> >> But maybe could encode it into two Metamath axioms: >> >> ${ >> ax-1.1 $e |- ((p·q)·r)·(p·((p·r)·p)) >> ax-1 $a |- r >> $} >> and >> >> ${ >> ax-2.1 $e |- r >> ax-2 $a |- ((p·q)·r)·(p·((p·r)·p)) >> $} >> _ >> Thierry >> >> >> On 06/06/2024 11:06, Gino Giotto wrote: >> >> > 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 >> >> <https://groups.google.com/d/msgid/metamath/CAPKSAW5oD62rvGSbcsL4eJHbdxiOh4GaSdf7Cqq8B8s7DFz4Vw%40mail.gmail.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/4f007556-4d80-4b8c-934e-01c52e43ce26%40gmx.net >> >> <https://groups.google.com/d/msgid/metamath/4f007556-4d80-4b8c-934e-01c52e43ce26%40gmx.net?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/b32870b9c8b64b5cb90ee1b3fac08a24%40rwth-aachen.de >> >> <https://groups.google.com/d/msgid/metamath/b32870b9c8b64b5cb90ee1b3fac08a24%40rwth-aachen.de?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/caf85902-88ae-4633-bad7-56ccbcaaa8a1n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/caf85902-88ae-4633-bad7-56ccbcaaa8a1n%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/0d6f9a46-fb9c-4ff8-916a-1f60b80eb5b1n%40googlegroups.com.
