> 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/40b4d3b7-9373-42cb-a719-c522fc9bafc1n%40googlegroups.com.
