I'm currently taking a course of Logic and Computability. We've seen that given an inductively defined language, if we can prove that a property holds for the 'base case' (such as propositions) and it's maintained through the rules of the language, then it holds for all expressions of the language (the set of the words that have the property is closed under the rules of the language).
Even though it's intuitive and we've proven it by induction over the length of the construction sequences, that got me wanting to formalize what an inductive set actually is, why induction works and is valid (not the intuitive idea, but the formal bases including set theory), and how precisely is it that we can apply induction over inductive sets (again, that sounds obvious, but I want the formality).
I've been reading through a lot of books, but they either: talk about sets, assuming the formality of induction; talk about induction, assuming the formality of the definitions of sets and inductive sets; or they talk about languages assuming both. So is there some book or course notes that goes in depth with all these concepts, integrating them?
I've read (of course not in depth) the followings:
- A Mathematical Introduction to Logic - Enderton
- Logic, Computation and Set Theory - Forster
- Handbook of Mathematical Induction - Gunderson
- Classic Set Theory - Goldrei
And a few more pointing in the same direction
There is a chapter by Peter Aczel in the Handbook of Mathematical Logic: https://doi.org/10.1016/S0049-237X(08)71120-0 "An Introduction to Inductive Definitions" But the full text does not seem to be online.