Does doing recursive definitions add new axioms?

Stream: general

[Thomas Scholz]

How does the process of inductively defining a new data type or doing recursive definitions function in the formal foundation underlying Lean? In first-order logic, the recursive definition of addition in Peano arithmetic corresponds to the addition of two axioms
- $\forall n.\, n + 0 = n$
- $\forall m, n.\, n + s(m) = s(n+m)$
But in type theory and Lean, the use of recursive definitions does not yield to expanding the formal system by new axioms, isn't it? I suppose that the possibility of recursive definitions, rather, is like a built-in feature of the formal system.
But how does this function if not adding new axioms for each definition? What are the inference rules of the formal system that allow to use recursive definitions without adding new axioms each time?

[Simon Hudon]

Lean's dependent type theory formalizes inductive types using recursors. If we take the example of nat, the declaration:

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

adds the following axioms / constants:

constant nat : Type
constant nat.zero : nat
constant nat.succ : nat -> nat
constant nat.rec : Π {C : nat -> Sort u}, C zero -> (Π n : nat, C n -> C (nat.succ n)) -> Π n : nat, C n

[Simon Hudon]

Once you have those, every recursive definition about nat can be expressed using nat.rec

[Thomas Scholz]

Ok, thanks very much!
And what are the inference rules of the formal system underlying Lean that create these axioms / constants from inductive definitions?

[Simon Hudon]

You may find that answer is @Mario Carneiro's master thesis: https://github.com/digama0/lean-type-theory/releases