How are the naturals numbers defined in Dependent type theor

Stream: new members

[Kent Van Vels]

I have basically two weeks of exposure to Dependent Type Theory, and I think of the mathematical world in terms of sets. I feel like I am east of Eden. So, to build my intuition, I would like to understand how the natural numbers are defined/constructed at level appropriate for an honors undergraduate student. Something like how Tao constructs the natural numbers using the Peano axioms in his undergraduate analysis book. Are there any resources any where I can read such a treatment? Is there a different structure, perhaps a group. that would be appropriate to understand first?

I appreciate any ideas. Thanks.

[Adam Topaz]

Lean's definition is here src#nat

[Adam Topaz]

it's an inductive type with two constructors: zero : nat and succ : nat -> nat.

[Adam Topaz]

the book #tpil has a section on inductive types that might be helpful as well.

[Kent Van Vels]

Yeah I was looking at that. It mentions a paper "Peter Dybjer. Inductive families. Formal Asp. Comput., 6(4):440–465, 1994". I will try to read that. #tpil also mentions that

It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, Pi types, and inductive types; everything else follows from those.

I would be very much interested to read an accounting of that.

Thank you.

[Patrick Massot]

#nng is the standard answer to this question.

[Kent Van Vels]

Thank you both, I got a copy of the Peter Dybjer paper from a list of links. I think I have very much enough to go on.

[Kent Van Vels]

The natural number game is what started me down this rabbit hole. Ha.

[Julian Berman]

There's also some talks Kevin's given which you may find interesting. E.g. https://www.youtube.com/watch?v=aIObfpWdDbo (don't worry it's not actually 4 hours)

[Jason Rute]

You might also find my answer to this stack exchange question useful. The main point is that when Lean processes inductive types like thenat it adds a new theorem (axiom?) to the global context called rec which is a super powered version of induction and recursion. It does all the work. Lean also automatically derives a bunch of theorems from rec. And even some of the built in syntax in Lean for working with inductive structures (like match blocks) is just syntactic sugar for rec-derived functions.

[Jason Rute]

This is explained in #tpil, but if you want a deeper dive into DTT, I recommend the first chapter of the HoTT book (https://homotopytypetheory.org/book/). They have a whole section on the natural numbers and how to derive it’s properties from rec.

[Kevin Buzzard]

@Kent Van Vels when you type

inductive nat : Type
| zero : nat
| succ : nat -> nat

into Lean, under the hood four new objects are created in the system. The first object is a new type called nat, which is introduced as an undefined constant. In other words, we can now talk about a new type called nat. The second and third objects are two new constructors for nat called nat.zero and nat.succ. This means that Lean now knows there's a term nat.zero : nat and a function nat.succ : nat -> nat. The fourth thing is a function which can be interpreted as both the principle of mathematical induction and the principle of mathematical recursion. The reason you can do both things with one function is that the Type universe and the Prop universe are both universes and so you can talk about functions taking values in a random universe and this covers both cases. Once you have recursion and induction you can prove all the other obvious things like zero isn't succ of anything, that succ is injective and so on. I wrote something about induction and inductive types here, which might help (I also came to this as a mathematician with some understanding of set theory but 0 knowledge of type theory).

[Kent Van Vels]

Thank you for the links. I appreciate it.

[Kent Van Vels]

Thank you, I think the post you linked to is very helpful.

[Arthur Paulino]

@Jason Rute in Lean 4 recursors (rec) are primitive declarations on their own, among with definitions, axioms, theorems etc

[Jason Rute]

Arthur Paulino said:

Jason Rute in Lean 4 recursors (rec) are primitive declarations on their own, among with definitions, axioms, theorems etc

I'm a bit confused. Are you saying some declaration keyword (like rec or recursor) is used to make declarations in Lean by users? If so, I have no idea what the syntax is or why a user would want to use this. Do you have documentation on this feature? (And I assume we are talking about something separate from local recursive declarations, right?)

[Jason Rute]

@Arthur Paulino, or are you just talking about an internal recursor designation for such declarations, for example:

-- Lean 4:
#print Nat.rec
recursor Nat.rec.{u} : {motive : Nat → Sort u} → motive Nat.zero → ((n : Nat) → motive n → motive (Nat.succ n)) → (t : Nat) → motive t

In that case is it just a rename of the Lean 3 eliminator designation?

-- Lean 3:
#print nat.rec
protected eliminator nat.rec : Π {motive : ℕ → Sort l}, motive 0 → (Π (n : ℕ), motive n → motive n.succ) → Π (n : ℕ), motive n

(Not that I understand completely what the eliminator designation provides in Lean 3. I guessnat.rec can't be a definition/theorem since there is no body/proof, and it shouldn't be an axiom as it shouldn't show up in the list of axioms. So that necessitates some other designation. Maybe eliminator also provides special judgmental equalities, or triggers the automatic creation of auxiliary theorems like nat.rec_on. It also likely makes the bookkeeping easier, especially when checking proofs in the kernel.)

[Arthur Paulino]

I was talking about the later, as you wrote the Nat.rec example