> 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/c8b6550a-6dc1-4005-b5b6-9d03cf55af3bn%40googlegroups.com.
