@Mike - ok, I understand your point now.

]]>I’ll try to optimize the wording (not now).

]]>As I said, I see the distinction. I was just saying that I think the description should emphasize first- versus second-order rather than “predicate” versus “subset”, since that’s where the distinction really lies.

]]>Right, David, thanks. I meant that if one is careful in specification which variables are bound in the predicate then the every notion of the class of allowed predicates effectively has the limit over quantification accounted for. The predicate here is assumed to have no free parameters other than $n\in\mathbb{N}$.

The collection of all subsets is

internallyuncountable - cf Skolem’s ’paradox’

Right. Though (correct me if I am wrong) if we have the axiom schema (parametrized by predicates), we can internally use one axiom from the schema at the time. Only metatheorems see the statements about the axiom schema. Besides, for the first order arithmetic alike the one in Mendelson, we do not use that serious fragment of set theory.

]]>Of course, the difference in first-/second-order is what one can quantify over. The collection of all subsets is *internally* uncountable - cf Skolem’s ’paradox’

Mike, by predicate I meant here a predicate which can be expressed as a sentence in the language of the first order theory, hence they come from definable subsets. Arbitrary subset $S$ is not expressible so (there are more subsets than formal sentences). The first order theory of course does not see the difference internally, if it can define a subset $S$ in such a theory then it can define the corresponding predicate, of course. But the full induction the usual sense can be used even for subsets which are not defined in the theory (for example we can do reasoning for some families of such subsets where we can not pick up indvidual members). We can talk about subsets which we can not concretize in that manner so that $S$ in your predicate becomes determined.

]]>I see the distinction, but I wouldn’t express it as a distinction between predicates and subsets. After all, if $S\subset \mathbb{N}$ is a subset, then $P(n) \coloneqq (n\in S)$ is a predicate.

]]>Yes, the second-order notion was first, before the first-order logical calculus had been completely codified if my history is right.

]]>But the second-order reasoning is very standard in practical mathematics and not something odd.

True, and of course an NNO captures how people use natural numbers, rather than models of first-order PA.

P.S. Peano’s axioms are originally due Dedekind, as you know.

I’d forgotten, so thanks! (Noether was apparently fond of saying “It’s already in Dedekind” :-)

]]>I tried to include both version in the idea section of induction; experts should correct me.

]]>Thank you David, indeed. The first order theories are the way to limit mathematics practice and thinking in the usual practice radically. E.g. talking about varying bases of a topology on a given set leads to the quantification over sets, now if we vary the topologies or underlying sets we are alread beyond and so on. This gives some strength to model theory as one can prove some things about rigid contexts. But the second-order reasoning is very standard in practical mathematics and not something odd. P.S. Peano’s axioms are originally due Dedekind, as you know.

]]>@Zoran

that looks to me like the second-order version of induction (which is what Peano originally wrote, and which is equivalent to what you get from an NNO in a topos), whereas logicians like the first-order one. The second-order induction schema axiomatises $\mathbb{N}$ up to isomorphism, rather than allowing non-standard models.

]]>$n$Lan entry induction states the weaker form of induction with respect to the usual mathematical practice; of course, this weaker form is the most usual in the logicians’ treatments. The practical mathematician’s form (and in usual university textbooks) is the following: if $S\subseteq\mathbb{N}$, $1\in S$ and $\forall n\in\mathbb{N}$ $n\in S \implies n+1\in S$ then $S = \mathbb{N}$. According to the Elliott Mendelson, *Introduction to mathematical logic*, D. Van Nostrad 1964 this is a weaker form of induction because there are $2^{\aleph_0}$ subsets of $\mathbb{N}$ but only $\aleph_0$ predicates. As long as one talks only about a single definable property it is the same thing, but if we talk about arbitrary (sets of) properties then we can get genuinely stronger statements.

The reference which you put (B. Jacobs) is a scan of an old version from 1997. I added the link to a newer extended 62 p. version (with more readable pdf link) published in 2011.

]]>I have added two references to *induction*.

Also, I added the missing (!) pointer to *coinduction* .