> 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.
Nope, ok, definitely I should have looked at those data in the first place (you have a nice detailed documentation btw). I'll took some care to look at what seems promising. At the moment, this is really just an excuse to get a better hand at pmGenerator options and functionalities (basically the same thing I did for metamath). Il giorno sabato 8 giugno 2024 alle 08:43:08 UTC+2 [email protected] ha scritto: > > 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/1021973a-6d84-4596-91b1-9a2fa1b28741n%40googlegroups.com.
