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

Discussion Tag Cloud

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.
    • CommentAuthorJamesSmith
    • CommentTimeMay 10th 2017

    Hi,

    I am trying to answer my own question here…

    Is it possible to derive the axiom of induction from a model of the natural numbers?

    …and came across this page on nLab:

    natural numbers type

    This seems to have what I need, but the going is hard. I wonder if anyone can help.

    I am stuck, for example, on what exactly rec p n(...)rec_p^n(...) is, and what a fibration is. The text says ’the above fibration’ but there is no fibration above so far as I can see, only what I’m guessing is a related display map. The page on fibrations is duanting and didn’t, at a quick glance, seem to give me the necessary relevant information.

    All help appreciated!

    Kind regards,

    James

    • CommentRowNumber2.
    • CommentAuthorRichard Williamson
    • CommentTimeMay 10th 2017
    • (edited May 10th 2017)

    Hi James,

    One cannot derive induction purely from the construction you have given. What you have given are basically the first two steps in Definition 2.1 at the nLab page. Induction corresponds to the third rule, the ’elimination rule’.

    I would not bother with Example 3.1 if you wish to understand this rule, just try to understand it itself. The things above the line are assumptions, the thing below the line is what the rule allows one to conclude. The p 0:P(0)p_{0} : P(0) bit means that we are assuming that we have a proof (denoted p 0p_{0}) of some proposition, denoted P(0)P(0). The x:,p:P(x)p s(x,p):P(successor(x))x:\mathbb{N}, p : P(x) \vdash p_{s}(x,p) : P(successor(x)) bit means that we are assuming that, given a natural number xx and a proof pp of a proposition P(x)P(x) involving xx, we can obtain a proof p s(x,p)p_{s}(x,p) of the same proposition but with successor(x)successor(x) instead of xx. The bit under the line means that, given any natural number nn (assumed at the extreme right of the upper line), we can deduce a proof of the same proposition for nn. As you will see, this is pretty much exactly induction as you are probably thinking of it.

    The computation rules are more technical, I would just ignore them for now.

    The reason that the Coq syntax does not include the elimination rule explicitly is that it comes for free from the ’Inductive’ keyword.

    • CommentRowNumber3.
    • CommentAuthorJamesSmith
    • CommentTimeMay 11th 2017
    • (edited May 11th 2017)

    Richard, hi,

    thanks for commenting.

    I get the bit about p 0:P(0)p_0:P(0) being a proof p 0p_0 of the proposition P(0)P(0), and so on. And I get the bit about rec p n(...)rec_p^n(...) being the proof for arbitrary nn now. So yes, I can see that the term elimination rule is in some very close sense analogous to the axiom of induction.

    This is the first time incidentally that I have understood the propositions as types paradigm. I now like the idea of theory based on dependent types, where propositions are types, because I’ve finally grasped its utility.

    Thanks again and regards.

  1. You’re welcome! Glad if it was useful.

    • CommentRowNumber5.
    • CommentAuthorJamesSmith
    • CommentTimeMay 15th 2017

    Hi,

    I added an answer to my own question. Here is the link again:

    Is it possible to derive the axiom of induction from a model of the natural numbers?

    Many thanks,

    James