## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJan 19th 2012
• (edited Jan 19th 2012)

I have added two references to induction.

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

• CommentRowNumber2.
• CommentAuthorzskoda
• CommentTimeNov 21st 2013

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.

• CommentRowNumber3.
• CommentAuthorzskoda
• CommentTimeNov 6th 2016
• (edited Nov 6th 2016)

$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.

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeNov 6th 2016

@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.

• CommentRowNumber5.
• CommentAuthorzskoda
• CommentTimeNov 6th 2016
• (edited Nov 6th 2016)

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.

• CommentRowNumber6.
• CommentAuthorzskoda
• CommentTimeNov 6th 2016

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

• CommentRowNumber7.
• CommentAuthorDavidRoberts
• CommentTimeNov 6th 2016
• (edited Nov 6th 2016)

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” :-)

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeNov 6th 2016

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

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeNov 7th 2016

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.

• CommentRowNumber10.
• CommentAuthorzskoda
• CommentTimeNov 7th 2016
• (edited Nov 7th 2016)

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.

• CommentRowNumber11.
• CommentAuthorDavidRoberts
• CommentTimeNov 7th 2016

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’

• CommentRowNumber12.
• CommentAuthorzskoda
• CommentTimeNov 7th 2016
• (edited Nov 7th 2016)

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 internally uncountable - 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.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeNov 7th 2016

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.

• CommentRowNumber14.
• CommentAuthorzskoda
• CommentTimeNov 7th 2016

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

• CommentRowNumber15.
• CommentAuthorDavidRoberts
• CommentTimeNov 7th 2016

@Mike - ok, I understand your point now.