> I'll took some care *I'll take*
Il giorno sabato 8 giugno 2024 alle 11:43:16 UTC+2 Gino Giotto ha scritto: > > 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/0106b895-8cb6-4cbf-91ef-1d3c99083a29n%40googlegroups.com.
