search

bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

[3] ZFC and Peano introductions #3

Closed Chobbes closed 6 years ago

Chobbes commented 6 years ago

Hmmm, I'm not sure how I feel about introducing ZFC and Peano numbers, and then immediately switching to a different section, and introducing several other definitions... Maybe bring these up where they are actually used? Otherwise the reader will think these are irrelevant details at the time, and then will have forgotten them when they are actually needed.

I'm also not sure that the ZFC definition is all that useful. It doesn't really add much, and I also wonder if bringing up the axiom of choice is anything more than a distraction. I understand that you're delving into the ZFC name, but I don't even know if it's worth bringing up "ZFC" as opposed to just saying "set theory", especially since you probably aren't actually going to rigorously introduce ZFC?

bor0 commented 6 years ago

Good catch! I think it's great to just refer to set theory rather than ZFC throughout. I think it's also good to move Peano a bit below where it's actually used. Thank you!