> 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<http://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<http://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<http://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<http://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]<mailto:[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.
