Namespaces
Variants
Actions

Difference between revisions of "Natural numbers object"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (link)
m (Automatically changed introduction)
 
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
An [[Object in a category|object in a category]] equipped with structure giving it properties similar to those of the set of natural numbers in the category of sets. Natural numbers objects have been most extensively studied in the context of a [[Topos|topos]], but the definition (due to F.W. Lawvere [[#References|[a6]]]) makes sense in any category with finite products. Lawvere's definition (like the [[Peano axioms|Peano axioms]] for the set of natural numbers) takes the basic structure of the natural numbers object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200301.png" /> in a category <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200302.png" /> to consist of the zero element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200303.png" /> (where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200304.png" /> denotes the terminal object of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200305.png" />) and the successor mapping <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200306.png" />; the condition they are required to satisfy is that, given any diagram of the form
+
<!--This article has been texified automatically. Since there was no Nroff source code for this article,
 +
the semi-automatic procedure described at https://encyclopediaofmath.org/wiki/User:Maximilian_Janisch/latexlist
 +
was used.
 +
If the TeX and formula formatting is correct and if all png images have been replaced by TeX code, please remove this message and the {{TEX|semi-auto}} category.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200307.png" /></td> </tr></table>
+
Out of 42 formulas, 34 were replaced by TEX code.-->
  
in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200308.png" />, there is a unique <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n1200309.png" /> such that
+
{{TEX|semi-auto}}{{TEX|part}}
 +
An [[Object in a category|object in a category]] equipped with structure giving it properties similar to those of the set of natural numbers in the category of sets. Natural numbers objects have been most extensively studied in the context of a [[Topos|topos]], but the definition (due to F.W. Lawvere [[#References|[a6]]]) makes sense in any category with finite products. Lawvere's definition (like the [[Peano axioms|Peano axioms]] for the set of natural numbers) takes the basic structure of the natural numbers object $N$ in a category $\mathcal{C}$ to consist of the zero element $o : 1 \rightarrow N$ (where $1$ denotes the [[terminal object]] of $\mathcal{C}$) and the successor mapping $s : N \rightarrow N$; the condition they are required to satisfy is that, given any diagram of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003010.png" /></td> </tr></table>
+
\begin{equation*} A \stackrel { x } { \rightarrow } B \stackrel { t } { \rightarrow } B \end{equation*}
  
commutes. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003011.png" /> is Cartesian closed (see [[Closed category|Closed category]]), it is sufficient to demand this condition in the case when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003012.png" /> is the terminal object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003013.png" />. It is clear from the form of the definition that a natural numbers object, if it exists, is unique up to canonical isomorphism.
+
in $\mathcal{C}$, there is a unique $f : N \times A \rightarrow B$ such that
  
The definition is a particular case of the scheme of primitive recursion, rephrased in categorical terms; it implies that every [[Primitive recursive function|primitive recursive function]] of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003014.png" /> variables is  "realized" as a morphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003015.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003016.png" />, and that two such morphisms are equal provided the equality of the corresponding functions is provable in primitive recursive arithmetic. (For more information on the representability of recursive functions in categories, see [[#References|[a5]]], Part III.)
+
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003010.png"/></td> </tr></table>
  
Any Grothendieck topos (see [[Site|Site]]) contains a natural numbers object; more generally, in any Cartesian closed category with countable coproducts, the countable copower of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003017.png" /> will serve as a natural numbers object. However, there are examples of toposes, such as the effective topos of M. Hyland, in which a natural numbers object exists but is not a countable copower of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003018.png" />. Natural numbers objects in toposes were studied by P. Freyd [[#References|[a2]]]: he showed that an object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003019.png" /> in a topos, equipped with morphisms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003020.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003021.png" /> as above, is a natural numbers object if and only if the diagram
+
commutes. If $\mathcal{C}$ is Cartesian closed (see [[Closed category|Closed category]]), it is sufficient to demand this condition in the case when $A$ is the terminal object $1$. It is clear from the form of the definition that a natural numbers object, if it exists, is unique up to canonical isomorphism.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003022.png" /></td> </tr></table>
+
The definition is a particular case of the scheme of primitive recursion, rephrased in categorical terms; it implies that every [[Primitive recursive function|primitive recursive function]] of $k$ variables is  "realized"  as a morphism $N ^ { k } \rightarrow N$ in $\mathcal{C}$, and that two such morphisms are equal provided the equality of the corresponding functions is provable in primitive recursive arithmetic. (For more information on the representability of recursive functions in categories, see [[#References|[a5]]], Part III.)
 +
 
 +
Any Grothendieck topos (see [[Site|Site]]) contains a natural numbers object; more generally, in any Cartesian closed category with countable coproducts, the countable copower of $1$ will serve as a natural numbers object. However, there are examples of toposes, such as the effective topos of M. Hyland, in which a natural numbers object exists but is not a countable copower of $1$. Natural numbers objects in toposes were studied by P. Freyd [[#References|[a2]]]: he showed that an object $N$ in a topos, equipped with morphisms $o$ and $s$ as above, is a natural numbers object if and only if the diagram
 +
 
 +
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003022.png"/></td> </tr></table>
  
 
is a coproduct and
 
is a coproduct and
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003023.png" /></td> </tr></table>
+
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003023.png"/></td> </tr></table>
  
is a [[co-equalizer]], and also that these conditions are equivalent to the validity of the Peano axioms expressed in the internal logic of the topos. Further, a topos contains a natural numbers object if and only if it contains an object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003024.png" /> which is  "Dedekind-infinite"  in the sense that there exists a monomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003025.png" /> whose image is disjoint from some well-supported subobject of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003026.png" />. From the first of Freyd's characterizations, it follows that a functor between countably-cocomplete toposes which preserves finite limits and finite coproducts will preserve countable coproducts if and only if it preserves co-equalizers.
+
is a [[co-equalizer]], and also that these conditions are equivalent to the validity of the Peano axioms expressed in the internal logic of the topos. Further, a topos contains a natural numbers object if and only if it contains an object $A$ which is  "Dedekind-infinite"  in the sense that there exists a monomorphism $A \rightarrow A$ whose image is disjoint from some well-supported subobject of $A$. From the first of Freyd's characterizations, it follows that a functor between countably-cocomplete toposes which preserves finite limits and finite coproducts will preserve countable coproducts if and only if it preserves co-equalizers.
  
Natural numbers objects suffice not only for the recursive definition of morphisms, but also (under suitable hypotheses) for the recursive construction of objects of a topos. In particular, G. Wraith showed that the existence of a natural numbers object in a topos implies the existence of list objects: a list object over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003027.png" /> is an object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003028.png" /> equipped with morphisms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003029.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003030.png" /> such that, given morphisms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003031.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003032.png" />, there is a unique <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003033.png" /> making
+
Natural numbers objects suffice not only for the recursive definition of morphisms, but also (under suitable hypotheses) for the recursive construction of objects of a topos. In particular, G. Wraith showed that the existence of a natural numbers object in a topos implies the existence of list objects: a list object over $A$ is an object $L A$ equipped with morphisms $o _ { A } : 1 \rightarrow L A$ and $s _ { A } : A \times L A \rightarrow L A$ such that, given morphisms $x : B \rightarrow C$ and $t : A \times C \rightarrow C$, there is a unique $f : L A \times B \rightarrow C$ making
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003034.png" /></td> </tr></table>
+
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003034.png"/></td> </tr></table>
  
commute. (Note that a natural numbers object is just a list object over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003035.png" />.) Given these, B. Lesaffre showed how to translate the usual recursive construction of free algebras (for any finitely-presented algebraic theory) into the internal logic of any topos with a natural numbers object, and P. Johnstone used the latter to construct  "classifying toposes"  containing generic models of such theories over any such topos. (For details of these developments, see [[#References|[a4]]].) Conversely, A. Blass [[#References|[a1]]] showed that the presence of a natural numbers object is necessary as well as sufficient for the construction of classifying toposes.
+
commute. (Note that a natural numbers object is just a list object over $1$.) Given these, B. Lesaffre showed how to translate the usual recursive construction of free algebras (for any finitely-presented algebraic theory) into the internal logic of any topos with a natural numbers object, and P. Johnstone used the latter to construct  "classifying toposes"  containing generic models of such theories over any such topos. (For details of these developments, see [[#References|[a4]]].) Conversely, A. Blass [[#References|[a1]]] showed that the presence of a natural numbers object is necessary as well as sufficient for the construction of classifying toposes.
  
The existence of a natural numbers object, as a postulate, plays much the same role in topos theory as the axiom of infinity (see [[Infinity, axiom of|Infinity, axiom of]]) does in [[Set theory|set theory]]. In classical set theory, this axiom is normally viewed as giving rise to the incompleteness phenomenon (see [[Gödel incompleteness theorem|Gödel incompleteness theorem]]), via Gödel numbering of formulas; however, in the constructive logic of toposes, the picture is rather different. P. Freyd [[#References|[a3]]] showed that (provided one assumes a meta-theory with the axiom of infinity, so that one can construct free algebras) the free topos <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003036.png" /> (without natural numbers object) contains a non-zero object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003037.png" /> such that the slice category <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/n/n120/n120030/n12003038.png" /> has a natural numbers object. Using this, he was able to demonstrate the existence of a  "rewrite rule"  which converts any sentence in higher-order intuitionistic type theory with the axiom of infinity into a sentence in the corresponding theory without the axiom of infinity, in such a way that provability is preserved and reflected.
+
The existence of a natural numbers object, as a postulate, plays much the same role in topos theory as the axiom of infinity (see [[Infinity, axiom of|Infinity, axiom of]]) does in [[Set theory|set theory]]. In classical set theory, this axiom is normally viewed as giving rise to the incompleteness phenomenon (see [[Gödel incompleteness theorem|Gödel incompleteness theorem]]), via Gödel numbering of formulas; however, in the constructive logic of toposes, the picture is rather different. P. Freyd [[#References|[a3]]] showed that (provided one assumes a meta-theory with the axiom of infinity, so that one can construct free algebras) the free topos $\mathcal{F}$ (without natural numbers object) contains a non-zero object $R$ such that the slice category $\mathcal{F} / R$ has a natural numbers object. Using this, he was able to demonstrate the existence of a  "rewrite rule"  which converts any sentence in higher-order intuitionistic type theory with the axiom of infinity into a sentence in the corresponding theory without the axiom of infinity, in such a way that provability is preserved and reflected.
  
 
====References====
 
====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A.R. Blass,  "Classifying topoi and the axiom of infinity"  ''Algebra Univ.'' , '''26'''  (1989)  pp. 341–345</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  P. Freyd,  "Aspects of topoi"  ''Bull. Austral. Math. Soc.'' , '''7'''  (1972)  pp. 1–76</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  P. Freyd,  "Numerals and ordinals" , unpublished manuscript  (1980)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  P.T. Johnstone,  G.C. Wraith,  "Algebraic theories in toposes"  P.T. Johnstone (ed.)  R. Paré (ed.) , ''Indexed Categories and their Applications'' , ''Lecture Notes Math.'' , '''661''' , Springer  (1978)  pp. 141–242</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  J. Lambek,  P.J. Scott,  "Introduction to higher order categorical logic" , Cambridge Univ. Press  (1986)</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  F.W. Lawvere,  "An elementary theory of the category of sets"  ''Proc. Nat. Acad. Sci.'' , '''52'''  (1964)  pp. 1506–1511</TD></TR></table>
+
<table><tr><td valign="top">[a1]</td> <td valign="top">  A.R. Blass,  "Classifying topoi and the axiom of infinity"  ''Algebra Univ.'' , '''26'''  (1989)  pp. 341–345</td></tr><tr><td valign="top">[a2]</td> <td valign="top">  P. Freyd,  "Aspects of topoi"  ''Bull. Austral. Math. Soc.'' , '''7'''  (1972)  pp. 1–76</td></tr><tr><td valign="top">[a3]</td> <td valign="top">  P. Freyd,  "Numerals and ordinals" , unpublished manuscript  (1980)</td></tr><tr><td valign="top">[a4]</td> <td valign="top">  P.T. Johnstone,  G.C. Wraith,  "Algebraic theories in toposes"  P.T. Johnstone (ed.)  R. Paré (ed.) , ''Indexed Categories and their Applications'' , ''Lecture Notes Math.'' , '''661''' , Springer  (1978)  pp. 141–242</td></tr><tr><td valign="top">[a5]</td> <td valign="top">  J. Lambek,  P.J. Scott,  "Introduction to higher order categorical logic" , Cambridge Univ. Press  (1986)</td></tr><tr><td valign="top">[a6]</td> <td valign="top">  F.W. Lawvere,  "An elementary theory of the category of sets"  ''Proc. Nat. Acad. Sci.'' , '''52'''  (1964)  pp. 1506–1511</td></tr></table>

Latest revision as of 17:43, 1 July 2020

An object in a category equipped with structure giving it properties similar to those of the set of natural numbers in the category of sets. Natural numbers objects have been most extensively studied in the context of a topos, but the definition (due to F.W. Lawvere [a6]) makes sense in any category with finite products. Lawvere's definition (like the Peano axioms for the set of natural numbers) takes the basic structure of the natural numbers object $N$ in a category $\mathcal{C}$ to consist of the zero element $o : 1 \rightarrow N$ (where $1$ denotes the terminal object of $\mathcal{C}$) and the successor mapping $s : N \rightarrow N$; the condition they are required to satisfy is that, given any diagram of the form

\begin{equation*} A \stackrel { x } { \rightarrow } B \stackrel { t } { \rightarrow } B \end{equation*}

in $\mathcal{C}$, there is a unique $f : N \times A \rightarrow B$ such that

commutes. If $\mathcal{C}$ is Cartesian closed (see Closed category), it is sufficient to demand this condition in the case when $A$ is the terminal object $1$. It is clear from the form of the definition that a natural numbers object, if it exists, is unique up to canonical isomorphism.

The definition is a particular case of the scheme of primitive recursion, rephrased in categorical terms; it implies that every primitive recursive function of $k$ variables is "realized" as a morphism $N ^ { k } \rightarrow N$ in $\mathcal{C}$, and that two such morphisms are equal provided the equality of the corresponding functions is provable in primitive recursive arithmetic. (For more information on the representability of recursive functions in categories, see [a5], Part III.)

Any Grothendieck topos (see Site) contains a natural numbers object; more generally, in any Cartesian closed category with countable coproducts, the countable copower of $1$ will serve as a natural numbers object. However, there are examples of toposes, such as the effective topos of M. Hyland, in which a natural numbers object exists but is not a countable copower of $1$. Natural numbers objects in toposes were studied by P. Freyd [a2]: he showed that an object $N$ in a topos, equipped with morphisms $o$ and $s$ as above, is a natural numbers object if and only if the diagram

is a coproduct and

is a co-equalizer, and also that these conditions are equivalent to the validity of the Peano axioms expressed in the internal logic of the topos. Further, a topos contains a natural numbers object if and only if it contains an object $A$ which is "Dedekind-infinite" in the sense that there exists a monomorphism $A \rightarrow A$ whose image is disjoint from some well-supported subobject of $A$. From the first of Freyd's characterizations, it follows that a functor between countably-cocomplete toposes which preserves finite limits and finite coproducts will preserve countable coproducts if and only if it preserves co-equalizers.

Natural numbers objects suffice not only for the recursive definition of morphisms, but also (under suitable hypotheses) for the recursive construction of objects of a topos. In particular, G. Wraith showed that the existence of a natural numbers object in a topos implies the existence of list objects: a list object over $A$ is an object $L A$ equipped with morphisms $o _ { A } : 1 \rightarrow L A$ and $s _ { A } : A \times L A \rightarrow L A$ such that, given morphisms $x : B \rightarrow C$ and $t : A \times C \rightarrow C$, there is a unique $f : L A \times B \rightarrow C$ making

commute. (Note that a natural numbers object is just a list object over $1$.) Given these, B. Lesaffre showed how to translate the usual recursive construction of free algebras (for any finitely-presented algebraic theory) into the internal logic of any topos with a natural numbers object, and P. Johnstone used the latter to construct "classifying toposes" containing generic models of such theories over any such topos. (For details of these developments, see [a4].) Conversely, A. Blass [a1] showed that the presence of a natural numbers object is necessary as well as sufficient for the construction of classifying toposes.

The existence of a natural numbers object, as a postulate, plays much the same role in topos theory as the axiom of infinity (see Infinity, axiom of) does in set theory. In classical set theory, this axiom is normally viewed as giving rise to the incompleteness phenomenon (see Gödel incompleteness theorem), via Gödel numbering of formulas; however, in the constructive logic of toposes, the picture is rather different. P. Freyd [a3] showed that (provided one assumes a meta-theory with the axiom of infinity, so that one can construct free algebras) the free topos $\mathcal{F}$ (without natural numbers object) contains a non-zero object $R$ such that the slice category $\mathcal{F} / R$ has a natural numbers object. Using this, he was able to demonstrate the existence of a "rewrite rule" which converts any sentence in higher-order intuitionistic type theory with the axiom of infinity into a sentence in the corresponding theory without the axiom of infinity, in such a way that provability is preserved and reflected.

References

[a1] A.R. Blass, "Classifying topoi and the axiom of infinity" Algebra Univ. , 26 (1989) pp. 341–345
[a2] P. Freyd, "Aspects of topoi" Bull. Austral. Math. Soc. , 7 (1972) pp. 1–76
[a3] P. Freyd, "Numerals and ordinals" , unpublished manuscript (1980)
[a4] P.T. Johnstone, G.C. Wraith, "Algebraic theories in toposes" P.T. Johnstone (ed.) R. Paré (ed.) , Indexed Categories and their Applications , Lecture Notes Math. , 661 , Springer (1978) pp. 141–242
[a5] J. Lambek, P.J. Scott, "Introduction to higher order categorical logic" , Cambridge Univ. Press (1986)
[a6] F.W. Lawvere, "An elementary theory of the category of sets" Proc. Nat. Acad. Sci. , 52 (1964) pp. 1506–1511
How to Cite This Entry:
Natural numbers object. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Natural_numbers_object&oldid=42157
This article was adapted from an original article by Peter Johnstone (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article