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 TODO, a technique also sometimes referred to as unary numbers.

Natural numbers in STELF

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

$$n ::= 0 \,|\, \texttt{s}(n)$$

This representation translates easily into STELF:

%sort nat %.
%term z nat %.
%term s %pi 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 STELF

The addition of these natural numbers is defined by the judgment $\texttt{plus}(N_1,N_2,N_3)$, where $N_1$, $N_2$, and $N_3$ are natural numbers. In the definition below, capital letters stand for metavariables that can range over all natural numbers.

$${ \over \texttt{plus}(0,N,N) }\mathit{p\textit{-}z}$$ $${ \texttt{plus}(N_1,N_2,N_3) \over \texttt{plus}(\texttt{s}(N_1),N_2,\texttt{s}(N_3)) }{\mathit{p\textit{-}s}}$$

These judgments also translate cleanly into STELF:

%sort plus {_ nat} {_ nat} {_ nat} %.
%term p-z plus z N N %.
%term p-s %pi (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 STELF, which you can see by looking at STELF’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 $\texttt{plus}(N_1,N_2,N_3)$ allows us to conclude $\texttt{plus}(\texttt{s}(N_1),N_2,\texttt{s}(N_3))$.

Consider this derivation which encodes the fact that $2 + 1 = 3$:

$${ { \over { \texttt{plus}(0,\;\;\texttt{s}(0),\;\;\texttt{s}(0)) } }{\mathit{p\textit{-}z}} \over { { \texttt{plus}(\texttt{s}(0),\;\;\texttt{s}(0),\;\;\texttt{s}(\texttt{s}(0))) } \over { \texttt{plus}(\texttt{s}(\texttt{s}(0)),\;\;\texttt{s}(0),\;\;\texttt{s}(\texttt{s}(\texttt{s}(0)))) } }{\mathit{p\textit{-}s}} }{\mathit{p\textit{-}s}}$$

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

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

See also

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

External link

• Natural numbers at Wikipedia