> I could confirm that the current known proof is the shortest possible
Finding a shorter proof may still be possible if you're lucky, but proving it to be minimal is very unlikely, unless you have massive amounts of resources at your hands: Estimated from w5's data table <https://xamidi.github.io/pmGenerator/README.html#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info>, you would have to generate files with a combined size of around 404054704152 * 2.37^((63-55)/2) bytes, which are approx. 12.75 TB in order to cover all proofs up to lenght 63, which would ensure the 65-step proof is minimal. Moreover, the final step alone would require pmGenerator around 2173.65*(2173.65 / 759.14)^4 ≈ 146103.49 core-h (i.e. around 16.67 years CPU-time) and 759.14*(759.14/320.89)^4 ≈ 23778.51 GiB of RAM, assuming that the exponential growth factors do not increase (which they probably do, so it most likely is even worse). As you can see from w5's behavioral graph <https://xamidi.github.io/pmGenerator/svg/plot/w5-bgraph.svg>, most formulas quickly generated in w5 are insanely long, but this leads to making filtering really easy, which led to the short proofs of w5 at https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs without too much effort. This also means that w5's conclusions seem to be nicely distributed over the whole range of formulas. But since its known proofs are so small already, you have to be lucky to still find improvements, and minimal proofs might use very long formulas. So I'm not sure w5 is a good choice. Regardless of what you'll choose in the end, I wish you good luck and much success! [email protected] schrieb am Samstag, 8. Juni 2024 um 03:29:28 UTC+2: > > I am looking forward to your findings. Which system(s) are you looking > into? > > For now I'll keep doing something simple, just to get more confidence with > the tool. In the discussion > https://github.com/xamidi/pmGenerator/discussions/2 I read that it should > be easy to handle Walsh's fift axiom > https://xamidi.github.io/pmGenerator/svg/walsh5th.svg, so I think I'll > try to minimize the proof of "id" from it (since I also read that you > exhausted the search up to 55 steps, but the shortest proof that you know > of id is 65 steps, this means that even if I don't find anything, I could > confirm that the current known proof is the shortest possible, which is > interesting information). > > My computer is relatively mediocre, but it's not the first time I stress > it to do long running math related computations (like minimizing set.mm > proofs, reducing > axioms in set.mm or excluding a composite number in GIMPS > https://www.mersenne.org/). > > > Ok, I might now understand what Gino was about. This is a great > clarification! > > It was helpful for me as well to understand what Wolfram really meant. > > Il giorno sabato 8 giugno 2024 alle 00:21:46 UTC+2 > [email protected] ha scritto: > >> > but instead allowed resolution >> <https://en.wikipedia.org/wiki/Resolution_(logic)> to occur >> >> Oops, resolution and paramodulation, as noted on Otter's wiki article >> <https://en.wikipedia.org/wiki/Otter_(theorem_prover)>. >> >> >> > The axiomatization I provided, based on wolfram's axiom, is complete >> for Boolean algebra already. [...] To be clear, this axiom system will not >> be able to prove all theorems in propositional logic: it is quite obviously >> restricted to theorems of the form |- ( ph <-> ps ) [...] >> >> Ok, I might now understand what Gino was about. This is a great >> clarification! >> I'd like to add that as long as the operators of a system are >> functionally complete and it proves all theorems over those formulas, the >> system implicitly proves all theorems in propositional logic, which can be >> taken as aliases, just like pmproofs.txt >> <https://us.metamath.org/mmsolitaire/pmproofs.txt> does it — e.g. to >> prove *1.2:"((P v P) -> P)", one actually proves "((~ P -> P) -> P)". >> For Boolean algebra over {⊼}, this could be solved by using something >> like x⊼(x⊼x)=f(ψ) as an alias for each propositional formula ψ, where f >> converts any propositional formula over any desired operators into a >> corresponding formula in terms of ⊼, e.g. f(⊤)= x⊼(x⊼x), >> f(a∨b)=(a⊼a)⊼(b⊼b), etc. >> >> Metamath avoids implicit aliases by using "definitions" which are in fact >> axioms, since they introduce further symbols into the object language for >> convenience. Minimalistic deductive systems do not do this. >> >> >> > By the way, this is unrelated, but I know you are the person that >> created https://github.com/xamidi/pmGenerator/tree/1.2.0 [...] >> >> I should probably also note that version 1.2.0 was released 3 months ago, >> and https://github.com/xamidi/pmGenerator links to the current version >> (e.g. I recently added some nice graphical overviews to the readme file). >> >> >> [email protected] schrieb am Freitag, 7. Juni 2024 um 23:12:54 UTC+2: >> >>> On Fri, Jun 7, 2024 at 6:07 PM Discher, Samiro < >>> [email protected]> wrote: >>> >>>> 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. >>>> >>> >>> The axiomatization I provided, based on wolfram's axiom, is complete for >>> Boolean algebra already. That's exactly the point. I think you can be >>> slightly more minimalistic and use euc instead of trans, as follows: >>> >>> ${ euc.1 $e |- p = q $. euc.2 $e |- p = r $. >>> euc $a |- q = 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 euc ) AABABZAEBBAAAAACZFD $. >>> >>> ${ symm.1 $e |- p = q $. >>> symm $p |- q = p $= >>> ( refl euc ) ABACADE $. $} >>> >>> ${ trans.1 $e |- p = q $. trans.2 $e |- q = r $. >>> trans $p |- p = r $= >>> ( symm euc ) BACABDFEG $. $} >>> >>> What it means to be "complete for boolean algebra" here is that metamath >>> can prove |- ( ph <-> ps ) iff the above axiomatization can prove |- p = q, >>> where p and q are the encodings of ph and ps as NAND formulas respectively. >>> >>> > 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). >>>> >>> >>> The most natural way to do this in set.mm would be to simply take the >>> equivalents of the above axioms as pseudo-axioms in a section, namely >>> {bicomi,bitri} | bitr3i, nanbi12i, and wolfram (i.e. the axiom you get by >>> transcribing 'ax' above using wnan and wbi). >>> >>> To be clear, this axiom system will not be able to prove all theorems in >>> propositional logic: it is quite obviously restricted to theorems of the >>> form |- ( ph <-> ps ), and it is also language-restricted to only use >>> formulas in terms of NAND unless you add some definitions. But we would say >>> that propositional logic is a conservative extension of equational boolean >>> algebra, since all the theorems in the image of the translation are >>> provable iff they are provable in the equational logic. >>> >>> If you wanted to stick something minimal on top of this system to make >>> it complete for propositional logic, I would suggest adding some >>> definitions to the source language: >>> >>> * !p = p | p >>> * p /\ q = !(p | q) >>> * p -> q = p | !q >>> * p \/ q = !p -> q >>> * 1 = p \/ !p >>> >>> and then using the inference rule |- ( ph <-> T. ) ==> |- ph to allow >>> interpreting proofs of the form |- p = 1 as playing the role of |- p (which >>> is not otherwise well formed in equational logic). You can also add the >>> following definition: >>> >>> * (p <-> q) = (p -> q) /\ (q -> p) >>> >>> but then you will want to prove |- (p <-> q) = 1 <==> |- p = q to >>> ensure conservativity (since the translation makes <-> and = the same thing >>> and thus implicitly implies that these two are equivalent). >>> >>> >>>> >>>> ------------------------------ >>>> *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/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de >>>> >>>> <https://groups.google.com/d/msgid/metamath/e754e9f197134a08b7b74774cd8173f4%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/6e71cb40-84bb-4dd1-b17f-d523823bc20bn%40googlegroups.com.
