Logic – Is Enderton Proving Second Order Induction in ‘Mathematical Introduction to Logic’?

Question

I am reading Enderton's "Mathematical Introduction to Logic" and I am puzzled by the following reasoning:

Enderton defines the symbols of propositional logic (sentence letters and connectives) and then defines some "formula-building operations". With these, he states:

Theorem: If $S$ is a set of wffs containing all the sentence symbols and closed under all five formula-building operations, then $S$ is the set of all wffs.

As far as I understand, this seems to me a second order statement of induction. Something which could be formalized as $(\forall S \subseteq \text{Form})(… \rightarrow S = \text{Form})$ where Form would be the set of all wffs. I now have two questions:

i) Is he actually stating and proving induction in second order form or is he doing something slightly different which I am missing?

ii) If he is stating and proving induction in second order form, why is he allowed to do that? Isn't it a problem to have induction in that form while trying to construct a simple propositional logic or, for that matter, a first order theory?

Answer 1

When teaching "Intro to Proofs" if we want to go over induction on $\mathbb N$, we'll almost certainly opt to phrase everything in terms of full second-order induction, even though it's doubtful that anything we will prove in class won't be formalizable in PA or much weaker. Why?

1. The second order phrasing is (superficially) simpler, more intuitive and has less formal baggage.
2. The second order induction principle is... true, right? Certainly most mathematicians see no problem with it.
3. There's no rule that says in an exposition that we have to formalize mathematics as parsimoniously as possible, or explicitly formalize it at all.

All three of these considerations apply straightforwardly to Enderton's exposition. The syntactical end of first-order logic can certainly be formalized in PRA or some very weak theory, and if we were explicitly doing it that way for some reason, this theorem would be some schema and there wouldn't be any second-order logic in sight.

But the point of Enderton's book is not to formalize the metatheory as parsimoniously as possible. It's just to teach some mathematical logic. So, like anyone else teaches any other subject of mathematics, Enderton is speaking 'ordinary mathematical English' and not getting bogged down in irrelevant issues of formalization.