I think I found a shorter proof of Łukasiewicz's second axiom (L2) from Walsh's second axiom (w2):
Statement of L2: CCNppp My proof of L2: DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 I verified this finding with the command: pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 -b -n -o L2.txt Which generates a text file called "L2.txt" containing the output string: "1. CCNppp" If I understand correctly, the output string should be the statement generated by the provided proof, written in Polish notation. The table on https://github.com/xamidi/pmGenerator/discussions/2 reports that the shortest known proof of L2 from w2 is 781 steps long, while my proof is 535 steps long, so, if everything checks out, mine would be shorter. @xamidi Does this seem correct to you? The difficulty of Walsh's second axiom (w2) is rated as "horrible - 10/10" on pmGenerator Github page, so this would be a nice result :-) Il giorno sabato 8 giugno 2024 alle 12:17:41 UTC+2 Gino Giotto ha scritto: > > 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/b61d2655-3593-4c33-85a8-036d1239e3c1n%40googlegroups.com.
