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/CAFXXJSvt8SpjWuMpPCsEwZbFieEGHXTKnD9e3Ur7a%3DghDTBg6A%40mail.gmail.com.
