It's not a conservative extension, as the intuitionistic logic development makes clear. Peirce's law ((p -> q) -> p) -> p is not provable from ax-1,2,mp but it is provable from ax-1,2,3,mp, even though there are no negations involved in the statement. By contrast, df-bi is a conservative extension even though it has a peculiar form. This is easy to prove because you can replace (p <-> q) with -. ((p -> q) -> -. (q -> p)) everywhere in a proof using biconditionals to reduce it to a proof which refers to the theorem bijust instead of df-bi, in the original axiom system.
On Sun, Mar 8, 2020 at 4:44 AM 'ookami' via Metamath < [email protected]> wrote: > Hello, > > After all the years I now improve && extend in particular the > propositional logic section, I am still stuck with a fundamental question. > > Is there a good reason why negation is handled differently from the > bi-conditional? The definition of <-> is implicit. We learn that it must > obey a particular expression, that enables us to retrieve the > characteristics of this operator later. > > Why on earth is tjhe same not done with negation? One can easily > reinterpret axiom ax-3 as an implicit *definition* of negation, thus > mandating a renaming to df-neg. The characteristics of negation are then > determined likewise. > > Looking forward to answers. > > Wolf Lammen > > -- > 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/42f13847-f827-4ce2-b39c-1528e5d76f40%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/42f13847-f827-4ce2-b39c-1528e5d76f40%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/CAFXXJSuirpAsJFAbbvnMT1dNand%2BqoBGrfJysKWHJNyyFDWh8A%40mail.gmail.com.
