> 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.
Well, that's the point. If you allow yourself to add as many rules as you want then you are formalizing something different than what the OTTER theorem prover was doing on page 7 and 8 of https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf and the what Wolfram showed about in the middle of the writing of https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ to prove the first Sheffer axiom. > 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 By the way, this is unrelated, but I know you are the person that created https://github.com/xamidi/pmGenerator/tree/1.2.0, and I wanted you to know that I tried your program a few weeks ago and I like it a lot. The metamath set.mm database does not really care about minimal proofs all the way back to the axioms, but I do. You might see me contributing some time in the future (particularly regarding the challenges of https://github.com/xamidi/pmGenerator/discussions/2). Il giorno venerdì 7 giugno 2024 alle 18:07:41 UTC+2 [email protected] ha scritto: > > 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). > > 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. > > ------------------------------ > *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/71e8f958-2f54-459d-9c0d-4c09af894140n%40googlegroups.com.
