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.
