Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorJamesSmith
   • CommentTimeMay 10th 2017
   • PermaLink
   Author: JamesSmith
   Format: MarkdownItexHi, 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?](https://math.stackexchange.com/questions/2269948/is-it-possible-to-derive-the-axiom-of-induction-from-a-model-of-the-natural-numb) ...and came across this page on nLab: [natural numbers type](https://ncatlab.org/nlab/show/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(...)$ 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

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

2. • CommentRowNumber2.
   • CommentAuthorRichard Williamson
   • CommentTimeMay 10th 2017
   • (edited May 10th 2017)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexHi 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)$ bit means that we are assuming that we have a proof (denoted $p_{0}$) of some proposition, denoted $P(0)$. The $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 $x$ and a proof $p$ of a proposition $P(x)$ involving $x$, we can obtain a proof $p_{s}(x,p)$ of the same proposition but with $successor(x)$ instead of $x$. The bit under the line means that, given any natural number $n$ (assumed at the extreme right of the upper line), we can deduce a proof of the same proposition for $n$. 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.

   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)$ bit means that we are assuming that we have a proof (denoted $p_{0}$) of some proposition, denoted $P(0)$. The $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 $x$ and a proof $p$ of a proposition $P(x)$ involving $x$, we can obtain a proof $p_{s}(x,p)$ of the same proposition but with $successor(x)$ instead of $x$. The bit under the line means that, given any natural number $n$ (assumed at the extreme right of the upper line), we can deduce a proof of the same proposition for $n$. 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.

3. • CommentRowNumber3.
   • CommentAuthorJamesSmith
   • CommentTimeMay 11th 2017
   • (edited May 11th 2017)
   • PermaLink
   Author: JamesSmith
   Format: MarkdownItexRichard, hi, thanks for commenting. I get the bit about $p_0:P(0)$ being a proof $p_0$ of the proposition $P(0)$, and so on. And I get the bit about $rec_p^n(...)$ being the proof for arbitrary $n$ 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.

   Richard, hi,

   thanks for commenting.

   I get the bit about $p_0:P(0)$ being a proof $p_0$ of the proposition $P(0)$, and so on. And I get the bit about $rec_p^n(...)$ being the proof for arbitrary $n$ 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.

4. • CommentRowNumber4.
   • CommentAuthorRichard Williamson
   • CommentTimeMay 11th 2017
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexYou're welcome! Glad if it was useful.

   You’re welcome! Glad if it was useful.

5. • CommentRowNumber5.
   • CommentAuthorJamesSmith
   • CommentTimeMay 15th 2017
   • PermaLink
   Author: JamesSmith
   Format: MarkdownItexHi, 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?](https://math.stackexchange.com/questions/2269948/is-it-possible-to-derive-the-axiom-of-induction-from-a-model-of-the-natural-numb/2275223#2275223) Many thanks, James

   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