# Formal proof of properties over inductive sets

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

• You may find my blog posting on this topic useful: dcproof.wordpress.com/2013/02/19/… See especially the follow-up at the end. – Dan Christensen Apr 1 at 13:43
• @Alexander: Dan's linked article is bogus. The answer to your question is that you need a meta-system MS to study FOL as a mathematical object. In modern logic, MS can be ZFC, but for core facts about FOL you only need a very weak MS such as ACA (look up "reverse mathematics" to learn more about it). And since you have basic competency in logic (which Dan does not), you can ask me more in the logic chat-room. – user21820 Jun 27 at 12:16