# Natural numbers

The **natural numbers** are the numbers 0, 1, 2, etc. The term is generally used to indicate a specific technique of representing natural numbers as either zero or the successor of some other natural number - 0, s(0), s(s(0)), etc - as in Peano arithmetic, a technique also sometimes referred to as **unary numbers.**

## Contents

## Natural numbers in Twelf

Natural numbers in Twelf are usually defined in a similar way. Mathematically, natural numbers can be defined as zero or the successor of some other natural number:

This representation translates easily into Twelf:

nat: type. z: nat. s: nat -> nat.

The first line declares that `nat` is a type. The second line declares `z` (zero) to be an object of type `nat`, and the third line declars `s` (successor) to be a type constructor that takes an object `N` of type `nat` and produces another object `(s N)` of type `nat`.

## Addition of natural numbers in Twelf

The addition of these natural numbers is defined by the judgment , where , , and are natural numbers. In the definition below, capital letters stand for metavariables that can range over all natural numbers.

These judgments also translate cleanly into Twelf:

plus: nat -> nat -> nat -> type. p-z: plus z N N. p-s: plus (s N1) N2 (s N3) <- plus N1 N2 N3.

The first line defines the judgment, declaring `plus` to be a type family indexed by three terms of type `nat`.

The second line declares that for any natural number `N`, `p-z` is an object of type `plus z N N`, which corresponds to the axiom p-z above. The `N` is an implicit parameter - it is treated as a bound variable by Twelf, which you can see by looking at Twelf's output after checking the above code.

The third line says that `p-s` is a type constructor that, given an object `D` of type `plus N1 N2 N3` (where `N1`, `N2`, and `N3` are all implicit parameters that can
be treated as metavariables), produces an object, `p-s D`, with type `plus (s N1) N2 (s N3)`. This corresponds to the rule p-s, which given a derivation of allows us to conclude .

Consider this derivation which encodes the fact that :

This can be represented in Twelf by applying the type constructor `p-s` to the object `p-z` twice:

2+1=3 : plus (s (s z)) (s z) (s (s (s z))) = p-s (p-s p-z).

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)2+1=3 : plus (s (s z)) (s z) (s (s (s z))) = p-s (p-s p-z).

%% OK %%

## See also

- Natural numbers with inequality
- Division over the natural numbers
- Proving metatheorems with Twelf, which uses natural numbers as an example, and also discusses the adequacy of the encoding.