## Not signed in

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

## Discussion Tag Cloud

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

• 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?

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

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

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

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.

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

• CommentRowNumber5.
• CommentAuthorJamesSmith
• CommentTimeMay 15th 2017

Hi,