Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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)

    nnLan 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 SS\subseteq\mathbb{N}, 1S1\in S and n\forall n\in\mathbb{N} nSn+1Sn\in S \implies n+1\in S then S=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 02^{\aleph_0} subsets of \mathbb{N} but only 0\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 SS\subset \mathbb{N} is a subset, then P(n)(nS)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 SS 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 SS 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 SS 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 nn\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.