Hey all,
As I'm looking into metamath there is something lingering that is making
me uncomfortable: definitions are axioms.
This is obviously intended and by design by the community (the book has
a whole chapter about it), but I'm still uncomfortable with the
justifications and consequences.
A few irrational feelings I think I'm having:
- I can't parse or understand df-bi trivially. What does it mean?
- How do I know that the axioms of the definitions aren't introducing
contradictions?
- It seems that definitions aren't supposed to "extend the language",
but I don't get that sentiment as I read them
- We say "all you need is propositional and first order logic and set
theory axioms" but then proceed to introduce a bunch by definitions
I'm sure this can't be a new sentiment, since an entire chapter in the
book was dedicated to it, but I was wondering if:
(a) Does anyone have some explanation posted online that I could read
to inform myself and perhaps settle my anxiety?
(b) Is there a version of metamath and/or set.mm that don't rely on
definitions as axioms?
Terribly sorry if this was discussed multiple times (it must have), but
a quick search in this mailing list didn't match any obvious prior
discussion, so apologies if I missed some.
Sam
--
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/24691da6-2b8e-4c93-b34d-d12f15d57f17n%40googlegroups.com.
