Wolfram's axiom is in "equational logic". That means that all theorems are of the form |- A = B, and the rules of inference are more or less:
* symmetry: If |- A = B then |- B = A * instantiation: If |- A = B then |- A[sigma] = B[sigma] for any substitution sigma to the variables in A and B * substitution: If |- A = B and |- C[A] = D[A] then |- C[B] = D[B] where C[_] and D[_] are contexts, i.e. terms with a hole in them which are filled by A and B respectively For example, I asked FindEquationalProof to prove |- (a|a)|(a|a) = a from wolfram's axiom |- ((a|b)|c)|(a|((a|c)|a)) = c, and the first step was: |- a|((a|b)|a) = b|((a|c)|(((a|c)|(a|((a|b)|a)))|(a|c))) which is obtained from the rules above as: 1. |- ((a|b)|c)|(a|((a|c)|a)) = c (axiom) 2. |- (((a|b)|c)|(a|((a|c)|a)))|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a) (instantiate a -> a|b, b -> c, c -> a|((a|c)|a) in 1) 3. |- c|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a) (substitute 1 in 2, with pattern _|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a)) 4. |- a|((a|c)|a) = c|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) (symmetry 3) 5. |- a|((a|b)|a) = b|((a|c)|(((a|c)|(a|((a|b)|a)))|(a|c))) (instantiate a -> a, b -> c, c -> b) (this is actually one step in wolfram's logic, which does certain operations like symmetry and bound variable renaming in zero steps). This is a fundamentally different kind of logic from metamath's usual FOL style inferential system, where the proof goals are of the form |- phi and modus ponens is traditionally the main inference rule. See ql.mm ( https://us.metamath.org/qleuni/mmtheorems1.html#ax-a1) for an example of an equational logic implemented in metamath. On Thu, Jun 6, 2024 at 6:34 PM [email protected] < [email protected]> wrote: > > 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 > <https://groups.google.com/d/msgid/metamath/0d6f9a46-fb9c-4ff8-916a-1f60b80eb5b1n%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/CAFXXJSsnSV6T%2BwkiXYr4rC%2BOFDCbxoKGUo3_PF1x5kH1WVh4KA%40mail.gmail.com.
