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.
