On Fri, Jun 7, 2024 at 6:07 PM Discher, Samiro <
[email protected]> wrote:
> If you are asking for technical details, sorry but I do not care enough
> about "Boolean algebra" to work these out. I think it is a complicated mess
> that has no pure logical character whatsoever (which is also why I think we
> would need several rules only to encode what "=" does). In particular, I
> think it is very hard and may even be impossible to provide an "elegant"
> axiomatization that doesn't need to combine a bunch of rules for what in
> Boolean algebra is considered a single step.
>
The axiomatization I provided, based on wolfram's axiom, is complete for
Boolean algebra already. That's exactly the point. I think you can be
slightly more minimalistic and use euc instead of trans, as follows:
${ euc.1 $e |- p = q $. euc.2 $e |- p = r $.
euc $a |- q = 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 euc ) AABABZAEBBAAAAACZFD $.
${ symm.1 $e |- p = q $.
symm $p |- q = p $=
( refl euc ) ABACADE $. $}
${ trans.1 $e |- p = q $. trans.2 $e |- q = r $.
trans $p |- p = r $=
( symm euc ) BACABDFEG $. $}
What it means to be "complete for boolean algebra" here is that metamath
can prove |- ( ph <-> ps ) iff the above axiomatization can prove |- p = q,
where p and q are the encodings of ph and ps as NAND formulas respectively.
> 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).
>
> "<->" / "=" is an equivalence relation, so reflexivity, transitivity and
> symmetry of it must be covered by rules. (
> https://en.wikipedia.org/wiki/Equivalence_relation#Definition)
>
> Essentially, I would look at what Wolfram's system is able to do and
> introduce rules until they (in combination) can do everything that is
> required.
>
> Then also provide the axiom, and you're done.
> I understood Mario's approach as doing just that, except that he provided
> a fundamental axiomatization, not one merely proven on top of another
> system (like set.mm).
>
The most natural way to do this in set.mm would be to simply take the
equivalents of the above axioms as pseudo-axioms in a section, namely
{bicomi,bitri} | bitr3i, nanbi12i, and wolfram (i.e. the axiom you get by
transcribing 'ax' above using wnan and wbi).
To be clear, this axiom system will not be able to prove all theorems in
propositional logic: it is quite obviously restricted to theorems of the
form |- ( ph <-> ps ), and it is also language-restricted to only use
formulas in terms of NAND unless you add some definitions. But we would say
that propositional logic is a conservative extension of equational boolean
algebra, since all the theorems in the image of the translation are
provable iff they are provable in the equational logic.
If you wanted to stick something minimal on top of this system to make it
complete for propositional logic, I would suggest adding some definitions
to the source language:
* !p = p | p
* p /\ q = !(p | q)
* p -> q = p | !q
* p \/ q = !p -> q
* 1 = p \/ !p
and then using the inference rule |- ( ph <-> T. ) ==> |- ph to allow
interpreting proofs of the form |- p = 1 as playing the role of |- p (which
is not otherwise well formed in equational logic). You can also add the
following definition:
* (p <-> q) = (p -> q) /\ (q -> p)
but then you will want to prove |- (p <-> q) = 1 <==> |- p = q to ensure
conservativity (since the translation makes <-> and = the same thing and
thus implicitly implies that these two are equivalent).
>
> ------------------------------
> *Von:* [email protected] <[email protected]> im Auftrag
> von Gino Giotto <[email protected]>
> *Gesendet:* Freitag, 7. Juni 2024 17:51:14
> *An:* Metamath
> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional
> calculus
>
> 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
> <https://groups.google.com/d/msgid/metamath/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%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/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de
> <https://groups.google.com/d/msgid/metamath/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de?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/CAFXXJSuUgPLEa4s2iwpUbPYdwRKb8MbrbjAmSUqYyRxboamX_g%40mail.gmail.com.
