> 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.
