> Well, that's the point. Didn't Mario do the same in his example <https://groups.google.com/g/metamath/c/NgtZH75z-xA/m/R7laijLGAAAJ>? I might've just misunderstood this due to my lack in understanding of Metamath syntax, but his statement "this is actually one step in wolfram's logic, which does certain operations like symmetry and bound variable renaming in zero steps" seems to confirm that he used multiple steps in Metamath for a single step in Wolfram's system.
> If you allow yourself to add as many rules as you want then you are formalizing something different than what the OTTER theorem prover was doing on page 7 and 8 of https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf and the what Wolfram showed about in the middle of the writing of https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ to prove the first Sheffer axiom. Only as many as required, but now you actually motivated me to look into some details in order to confirm my guesses. Their OTTER proofs(in https://www.cs.unm.edu/~mccune/papers/basax/DN-1.in) only used: list(usable). x = x. % Denial of the Robbins basis. B + A != A + B | (A + B) + C != A + (B + C) | ((A + B) @ + (A @ + B) @) @ != B | $Ans(Robbins_basis). end_of_list. The latter seems like an encoding of symmetry/commutativity, associativity and "Robbins". Note that due to it being a clause set, all but the last clauses are negated premises of a rule, but the conclusion is empty, so each of the premises is actually an axiom. So it makes sense that they have previously called this "3-basis {(Commutativity+),(Associativity+),(Robbins)}". They did not specify any actual rules, but instead allowed resolution <https://en.wikipedia.org/wiki/Resolution_(logic)> to occur. So their "proofs" are actually metaproofs to any imaginary Hilbert system (the kind of proof systems which Metamath can implement) of which they omitted details, which you have to define as you see fit when you are building one. This confirms my previous guesses. I don't know if there is any well-definedness in what they measure as a "single proof step", but translated in a Hilbert system, my guess is still that you need to combine multiple steps into one in order to count proof lengths like they do. Of course, a correct definition must entail that syntactical consequences (which are independent of proof length) do not differ. I might have totally missed your point here. I am really confused on where you take issue and why only now and not about Mario's solution, and after I already criticized what I'd consider the same issue. > By the way, this is unrelated, but I know you are the person that created https://github.com/xamidi/pmGenerator/tree/1.2.0, and I wanted you to know that I tried your program a few weeks ago and I like it a lot. [...] You might see me contributing some time in the future (particularly regarding the challenges of https://github.com/xamidi/pmGenerator/discussions/2). Nice, thanks for the feedback! I currently have quite a contribution for w3 of the challenge in the making and I am still terribly failing with w2. (Though, I have an idea how to tackle it, but this is an implementation effort for which I need to make time). I am looking forward to your findings. Which system(s) are you looking into? > The metamath set.mm database does not really care about minimal proofs all the way back to the axioms, but I do. But while .mm databases may not care about fundamental proof lengths (since they care about compressed proof size instead), it was the Metamath project that inspired all of my work on condensed detachment. In an email correspondence with Norman Megill in 2020 I asked him about minimal proofs regarding set.mm, and he led me to Metamath's mmsolitaire project and inspired me to create pmGenerator with the following words: "There is a separate project to find the "shortest after unfolding" proofs, i.e. shortest proofs directly from axioms, for the propositional calculus theorems in Principia Mathematica. The page is here: http://us.metamath.org/mmsolitaire/pmproofs.txt These proofs are shown in "condensed detachment" notation. [...] For pmproofs.txt, the basic unification algorithm for proofs in D-notation is given as "Rule D" in the "A finitely axiomatized..." paper on the Metamath Home Page. The program drule.c implements this in the function dAlgorithm(), which might provide hints if you want to write your own. (The drule.c internals are a little rough and ad-hoc, originally intended for my personal experiments and not for public release. It may be easier to write your own program rather than modify it.)" When I figured out there wasn't even a single tool to fully parse condensed detachment proofs (but only Norman's version to compute final conclusions over proofs, and only supporting propositional axioms of set.mm), I felt there was a strong need for such a tool. I find the elegance and simplicity of condensed detachment very appealing, but apparently I mostly fail to inspire others. [email protected] schrieb am Freitag, 7. Juni 2024 um 20:23:55 UTC+2: > > Essentially, I would look at what Wolfram's system is able to do and > introduce rules until they (in combination) can do everything that is > required. Then also provide the axiom, and you're done. > > Well, that's the point. If you allow yourself to add as many rules as you > want then you are formalizing something different than what the OTTER > theorem prover was doing on page 7 and 8 of > https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf and the what Wolfram > showed about in the middle of the writing of > https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ > > to prove the first Sheffer axiom. > > > If you are asking for technical details, sorry but I do not care > enough about "Boolean algebra" to work these out. I think it is a > complicated mess that has no pure logical character whatsoever > > By the way, this is unrelated, but I know you are the person that created > https://github.com/xamidi/pmGenerator/tree/1.2.0, and I wanted you to > know that I tried your program a few weeks ago and I like it a lot. The > metamath set.mm database does not really care about minimal proofs all > the way back to the axioms, but I do. You might see me contributing some > time in the future (particularly regarding the challenges of > https://github.com/xamidi/pmGenerator/discussions/2). > > Il giorno venerdì 7 giugno 2024 alle 18:07:41 UTC+2 > [email protected] ha scritto: > >> > Can you tell me how would you formalize Wolfram's axiom in Metamath >> without equality? (So that I can be sure we are on the same page). >> >> "<->" / "=" is an equivalence relation, so reflexivity, transitivity and >> symmetry of it must be covered by rules. ( >> https://en.wikipedia.org/wiki/Equivalence_relation#Definition) >> >> Essentially, I would look at what Wolfram's system is able to do and >> introduce rules until they (in combination) can do everything that is >> required. Then also provide the axiom, and you're done. >> I understood Mario's approach as doing just that, except that he provided >> a fundamental axiomatization, not one merely proven on top of another >> system (like set.mm). >> >> If you are asking for technical details, sorry but I do not care enough >> about "Boolean algebra" to work these out. I think it is a complicated mess >> that has no pure logical character whatsoever (which is also why I think we >> would need several rules only to encode what "=" does). In particular, I >> think it is very hard and may even be impossible to provide an "elegant" >> axiomatization that doesn't need to combine a bunch of rules for what in >> Boolean algebra is considered a single step. >> >> ------------------------------ >> *Von:* [email protected] <[email protected]> im Auftrag >> von Gino Giotto <[email protected]> >> *Gesendet:* Freitag, 7. Juni 2024 17:51:14 >> >> *An:* Metamath >> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional >> calculus >> Can you tell me how would you formalize Wolfram's axiom in Metamath >> without equality? (So that I can be sure we are on the same page). >> Il giorno venerdì 7 giugno 2024 alle 17:15:25 UTC+2 >> [email protected] ha scritto: >> >>> > Note that simply replacing the "=" with "<->" will lead you to an >>> incomplete system, because you have no way to derive a propositional >>> statement where the "<->" is not present. >>> >>> >>> Using "<->" was what I proposed. I cannot follow your statement. When >>> you have multiple rules that can do everything that is semantically defined >>> by Boolean algebra, you sure can derive everything that semantically >>> follows. The question is, why you wouldn't be able to define the required >>> rules in Metamath (and prove them in set.mm based on only propositional >>> primitives). >>> >>> >>> > the axioms in Mario's formalization would not provide all properties >>> that you need to know the full behaviour of the classical biconditional >>> operator >>> >>> >>> Which in set.mm is meaningless. All you need is to derive whichever >>> rules are required (in Metamath such is called "Theorem" with an >>> "Hypothesis"), but based on ax-1, ax-2, ax-3, ax-mp, df-bi, and df-nan >>> (which includes df-an). How can this not be possible? If it is not, there >>> must be a lack of expressiveness in the Metamath language, or Wolfram's "=" >>> must do something that is not true for "<->". Since the propositional >>> calculus is complete. >>> ------------------------------ >>> *Von:* [email protected] <[email protected]> im Auftrag >>> von Gino Giotto <[email protected]> >>> *Gesendet:* Freitag, 7. Juni 2024 16:53:19 >>> *An:* Metamath >>> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional >>> calculus >>> >>> > Why not? What features are used by Wolfram's rules that cannot be >>> described in Metamath language? Shouldn't propositional logic alone suffice >>> (as I mentioned earlier), let alone ZFC? >>> >>> I am referring to the chapter called "Other axiomatizations related to >>> classical propositional calculus", which appears before the properties >>> about equality (and set theory) are introduced. To formalize Wolfram's >>> system into that chapter, you have to find a way to eliminate/translate the >>> equality inference rules (which I don't think it's possible). >>> >>> Note that simply replacing the "=" with "<->" will lead you to an >>> incomplete system, because you have no way to derive a propositional >>> statement where the "<->" is not present. The tautology "|- ( ph -/\ >>> ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) )" is not derivable for example. >>> However, if you keep the "=" as a foreign symbol from classical >>> propositional calculus then you can derive an equivalent formulation as >>> "|- ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) ) = T." ("true" can >>> be defined in terms of NAND). >>> >>> you might say that replacing "=" with "<->" would allow to derive "|- ( >>> ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) ) <-> T." anyway, but the >>> axioms in Mario's formalization would not provide all properties that you >>> need to know the full behaviour of the classical biconditional operator. >>> >>> In Wolfram's system the biconditional can be added with a conservative >>> definition "|- ( ph <-> ps ) = ( ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) >>> -/\ ( ph -/\ ps ) )" and statements like "|- ( ps <-> ph ) = ( ph <-> >>> ps )" are derivable without issues. But what happens if I add a >>> definition of biconditional when the symbol "<->" was already used in >>> the system? Then I can now rewrite any biconditional into NAND operations, >>> and eventually derive expressions that do not contain any biconditional. >>> This was impossible before, therefore I didn't add a definition, I added an >>> axiom, so my original axiomatic system was not sufficient to properly >>> describe classical propositional calculus. >>> >>> Il giorno venerdì 7 giugno 2024 alle 10:21:14 UTC+2 >>> [email protected] ha scritto: >>> >>>> >>>> > So, we can't even formalize it in set.mm chapter about alternative >>>> axiom systems for propositional calculus at all. >>>> >>>> Why not? What features are used by Wolfram's rules that cannot be >>>> described in Metamath language? Shouldn't propositional logic alone >>>> suffice >>>> (as I mentioned earlier), let alone ZFC? >>>> >>>> >>>> [email protected] schrieb am Freitag, 7. Juni 2024 um 02:19:20 >>>> UTC+2: >>>> >>>>> I could not have wished for a better answer. He does actually assume >>>>> inferences about equality. So, we can't even formalize it in set.mm >>>>> chapter about alternative axiom systems for propositional calculus at >>>>> all. >>>>> Il giorno venerdì 7 giugno 2024 alle 00:54:27 UTC+2 [email protected] >>>>> ha scritto: >>>>> >>>>>> On Thu, Jun 6, 2024 at 11:07 AM Gino Giotto <[email protected]> >>>>>> wrote: >>>>>> >>>>>>> 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? >>>>>>> >>>>>> >>>>>> To answer this question directly, here's a metamath axiomatization of >>>>>> wolfram's axiom system and a proof of step 1: >>>>>> >>>>>> $c term wff |- = ( ) $. >>>>>> $v p q r s ph $. >>>>>> tp $f term p $. >>>>>> tq $f term q $. >>>>>> tr $f term r $. >>>>>> ts $f term s $. >>>>>> wph $f wff ph $. >>>>>> weq $a wff p = q $. $( equality $) >>>>>> tna $a term ( p q ) $. $( nand $) >>>>>> >>>>>> ${ symm.1 $e |- p = q $. >>>>>> symm $a |- q = p $. $} >>>>>> ${ trans.1 $e |- p = q $. trans.2 $e |- q = r $. >>>>>> trans $a |- p = r $. $} >>>>>> ${ naeq.1 $e |- p = q $. naeq.2 $e |- r = s $. >>>>>> naeq $a |- ( p r ) = ( q s ) $. $} >>>>>> >>>>>> ax $a |- ( ( ( p q ) r ) ( p ( ( p r ) p ) ) ) = r $. >>>>>> >>>>>> refl $p |- p = p $= >>>>>> ( tna ax symm trans ) AAABABZAFBBZAGAAAACZDHE $. >>>>>> >>>>>> step1 $p |- ( p ( ( p q ) p ) ) = ( q ( ( p r ) ( ( ( p r ) ( p ( ( p >>>>>> q ) p ) ) ) ( p r ) ) ) ) $= >>>>>> ( tna ax symm refl naeq trans ) >>>>>> AABDADDZACDZBDJDZKKJDKDDZDZBMDNJKBJEFLBMMACBE >>>>>> MGHI $. >>>>>> >>>>> -- >>> 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/fdfa1b17-a73c-41e7-b857-9af877a638c9n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/fdfa1b17-a73c-41e7-b857-9af877a638c9n%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/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%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/10ba674d-9698-43fd-ab33-3044f43e1cc1n%40googlegroups.com.
