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/6720db36-0a05-4cb9-99d2-2b4b88f7af9an%40googlegroups.com.
