CINXE.COM
natural number in nLab
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> natural number in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><!--/*--><![CDATA[/*><!--*/ .toc ul {margin: 0; padding: 0;} .toc ul ul {margin: 0; padding: 0 0 0 10px;} .toc li > p {margin: 0} .toc ul li {list-style-type: none; position: relative;} .toc div {border-top:1px dotted #ccc;} .rightHandSide h2 {font-size: 1.5em;color:#008B26} table.plaintable { border-collapse:collapse; margin-left:30px; border:0; } .plaintable td {border:1px solid #000; padding: 3px;} .plaintable th {padding: 3px;} .plaintable caption { font-weight: bold; font-size:1.1em; text-align:center; margin-left:30px; } /* Query boxes for questioning and answering mechanism */ div.query{ background: #f6fff3; border: solid #ce9; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; max-height: 20em; overflow: auto; } /* Standout boxes for putting important text */ div.standout{ background: #fff1f1; border: solid black; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; overflow: auto; } /* Icon for links to n-category arXiv documents (commented out for now i.e. disabled) a[href*="http://arxiv.org/"] { background-image: url(../files/arXiv_icon.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 22px; } */ /* Icon for links to n-category cafe posts (disabled) a[href*="http://golem.ph.utexas.edu/category"] { background-image: url(../files/n-cafe_5.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pdf files (disabled) a[href$=".pdf"] { background-image: url(../files/pdficon_small.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pages, etc. -inside- pdf files (disabled) a[href*=".pdf#"] { background-image: url(../files/pdf_entry.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ a.existingWikiWord { color: #226622; } a.existingWikiWord:visited { color: #226622; } a.existingWikiWord[title] { border: 0px; color: #aa0505; text-decoration: none; } a.existingWikiWord[title]:visited { border: 0px; color: #551111; text-decoration: none; } a[href^="http://"] { border: 0px; color: #003399; } a[href^="http://"]:visited { border: 0px; color: #330066; } a[href^="https://"] { border: 0px; color: #003399; } a[href^="https://"]:visited { border: 0px; color: #330066; } div.dropDown .hide { display: none; } div.dropDown:hover .hide { display:block; } div.clickDown .hide { display: none; } div.clickDown:focus { outline:none; } div.clickDown:focus .hide, div.clickDown:hover .hide { display: block; } div.clickDown .clickToReveal, div.clickDown:focus .clickToHide { display:block; } div.clickDown:focus .clickToReveal, div.clickDown .clickToHide { display:none; } div.clickDown .clickToReveal:after { content: "A(Hover to reveal, click to "hold")"; font-size: 60%; } div.clickDown .clickToHide:after { content: "A(Click to hide)"; font-size: 60%; } div.clickDown .clickToHide, div.clickDown .clickToReveal { white-space: pre-wrap; } .un_theorem, .num_theorem, .un_lemma, .num_lemma, .un_prop, .num_prop, .un_cor, .num_cor, .un_defn, .num_defn, .un_example, .num_example, .un_note, .num_note, .un_remark, .num_remark { margin-left: 1em; } span.theorem_label { margin-left: -1em; } .proof span.theorem_label { margin-left: 0em; } :target { background-color: #BBBBBB; border-radius: 5pt; } /*]]>*/--></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <!--//--><![CDATA[//><!-- MathJax.Ajax.config.path["Contrib"] = "/MathJax"; MathJax.Hub.Config({ MathML: { useMathMLspacing: true }, "HTML-CSS": { scale: 90, extensions: ["handle-floats.js"] } }); MathJax.Hub.Queue( function () { var fos = document.getElementsByTagName('foreignObject'); for (var i = 0; i < fos.length; i++) { MathJax.Hub.Typeset(fos[i]); } }); //--><!]]> </script> <script type="text/javascript"> <!--//--><![CDATA[//><!-- window.addEventListener("DOMContentLoaded", function () { var div = document.createElement('div'); var math = document.createElementNS('http://www.w3.org/1998/Math/MathML', 'math'); document.body.appendChild(div); div.appendChild(math); // Test for MathML support comparable to WebKit version https://trac.webkit.org/changeset/203640 or higher. div.setAttribute('style', 'font-style: italic'); var mathml_unsupported = !(window.getComputedStyle(div.firstChild).getPropertyValue('font-style') === 'normal'); div.parentNode.removeChild(div); if (mathml_unsupported) { // MathML does not seem to be supported... var s = document.createElement('script'); s.src = "https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=MML_HTMLorMML-full"; document.querySelector('head').appendChild(s); } else { document.head.insertAdjacentHTML("beforeend", '<style>svg[viewBox] {max-width: 100%}</style>'); } }); //--><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> natural number </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/13006/#Item_8" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="arithmetic">Arithmetic</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/number+theory">number theory</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic">arithmetic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+geometry">arithmetic geometry</a>, <a class="existingWikiWord" href="/nlab/show/arithmetic+topology">arithmetic topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+arithmetic+geometry">higher arithmetic geometry</a>, <a class="existingWikiWord" href="/nlab/show/E-%E2%88%9E+arithmetic+geometry">E-∞ arithmetic geometry</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/number">number</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a>, <a class="existingWikiWord" href="/nlab/show/integer+number">integer number</a>, <a class="existingWikiWord" href="/nlab/show/rational+number">rational number</a>, <a class="existingWikiWord" href="/nlab/show/real+number">real number</a>, <a class="existingWikiWord" href="/nlab/show/irrational+number">irrational number</a>, <a class="existingWikiWord" href="/nlab/show/complex+number">complex number</a>, <a class="existingWikiWord" href="/nlab/show/quaternion">quaternion</a>, <a class="existingWikiWord" href="/nlab/show/octonion">octonion</a>, <a class="existingWikiWord" href="/nlab/show/adic+number">adic number</a>, <a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinal number</a>, <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</a>, <a class="existingWikiWord" href="/nlab/show/surreal+number">surreal number</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/arithmetic">arithmetic</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Peano+arithmetic">Peano arithmetic</a>, <a class="existingWikiWord" href="/nlab/show/second-order+arithmetic">second-order arithmetic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/transfinite+arithmetic">transfinite arithmetic</a>, <a class="existingWikiWord" href="/nlab/show/cardinal+arithmetic">cardinal arithmetic</a>, <a class="existingWikiWord" href="/nlab/show/ordinal+arithmetic">ordinal arithmetic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/prime+field">prime field</a>, <a class="existingWikiWord" href="/nlab/show/p-adic+integer">p-adic integer</a>, <a class="existingWikiWord" href="/nlab/show/p-adic+rational+number">p-adic rational number</a>, <a class="existingWikiWord" href="/nlab/show/p-adic+complex+number">p-adic complex number</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/arithmetic+geometry">arithmetic geometry</a></strong>, <a class="existingWikiWord" href="/nlab/show/function+field+analogy">function field analogy</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+scheme">arithmetic scheme</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+curve">arithmetic curve</a>, <a class="existingWikiWord" href="/nlab/show/elliptic+curve">elliptic curve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+genus">arithmetic genus</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+Chern-Simons+theory">arithmetic Chern-Simons theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+Chow+group">arithmetic Chow group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Weil-%C3%A9tale+topology+for+arithmetic+schemes">Weil-étale topology for arithmetic schemes</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/absolute+cohomology">absolute cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Weil+conjecture+on+Tamagawa+numbers">Weil conjecture on Tamagawa numbers</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Borger%27s+absolute+geometry">Borger's absolute geometry</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Iwasawa-Tate+theory">Iwasawa-Tate theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/arithmetic+jet+space">arithmetic jet space</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adelic+integration">adelic integration</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/shtuka">shtuka</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Frobenioid">Frobenioid</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/Arakelov+geometry">Arakelov geometry</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/arithmetic+Riemann-Roch+theorem">arithmetic Riemann-Roch theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/differential+algebraic+K-theory">differential algebraic K-theory</a></p> </li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#operations_and_relations'>Operations and relations</a></li> <ul> <li><a href='#addition'> Addition</a></li> <li><a href='#minimum_function'> Minimum function</a></li> <li><a href='#maximum_function'>Maximum function</a></li> <li><a href='#distance_function'> Distance function</a></li> <li><a href='#absolute_value'>Absolute value</a></li> <li><a href='#less_than_relation'>Less than relation</a></li> <li><a href='#less_than_or_equal_to_relation'>Less than or equal to relation</a></li> <li><a href='#apart_from_relation'>Apart from relation</a></li> <li><a href='#observational_equality_relation'>Observational equality relation</a></li> <li><a href='#greater_than_relation'>Greater than relation</a></li> <li><a href='#greater_than_or_equal_to_relation'>Greater than or equal to relation</a></li> <li><a href='#multiplication'>Multiplication</a></li> <li><a href='#exponentiation'>Exponentiation</a></li> <li><a href='#division_and_remainder'>Division and remainder</a></li> </ul> <li><a href='#natural_numbers_objects'>Natural numbers objects</a></li> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#minima_of_subsets_of_natural_numbers'>Minima of subsets of natural numbers</a></li> <li><a href='#decreasing_sequences_of_natural_numbers'>Decreasing sequences of natural numbers</a></li> </ul> <li><a href='#Examples'>Examples</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <strong>natural number</strong> is traditionally one of the <a class="existingWikiWord" href="/nlab/show/numbers">numbers</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>, and so on. It is now common in many fields of mathematics to include <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> as a natural number as well. One advantage of doing so is that a natural number can then be identified with the <a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinality</a> of a <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a>, as well as a finite <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</a>. One can distinguish these as the <strong>nonnegative integers</strong> (with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>) and the <strong>positive integers</strong> (without <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>), at least until somebody uses ‘positive’ in the semidefinite sense. To a <a class="existingWikiWord" href="/nlab/show/set+theory">set theorist</a>, a natural number is essentially the same as an <strong><a class="existingWikiWord" href="/nlab/show/integer">integer</a></strong>, so they often use the shorter word; one can also clarify with <strong>unsigned integer</strong> (but this doesn't help with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>). In school mathematics, natural numbers with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> are called <strong>whole numbers</strong>.</p> <p>The set of natural numbers is often written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ω</mi></mrow><annotation encoding="application/x-tex">\omega</annotation></semantics></math>, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>ℵ</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">\aleph_0</annotation></semantics></math>. The last two notations refer to this set's structure as an <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</a> or <a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinal number</a> respectively, and they often (usually for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℵ</mi></mrow><annotation encoding="application/x-tex">\aleph</annotation></semantics></math>) have a subscript <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> allowing them to be generalised. In the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of mathematics, the <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a> states that this actually forms a set (rather than a proper class). At a foundational level, it's completely irrelevant whether <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> counts as a natural number or not; as <a class="existingWikiWord" href="/nlab/show/sets">sets</a> (and even as <a class="existingWikiWord" href="/nlab/show/natural+numbers+objects">natural numbers objects</a>), the two options are equivalent, so we are really talking about the choice of additive <a class="existingWikiWord" href="/nlab/show/semigroup">semigroup</a> structure (or <a class="existingWikiWord" href="/nlab/show/inclusion+map">inclusion map</a> into the set of <a class="existingWikiWord" href="/nlab/show/integers">integers</a>, etc).</p> <p>By default, our natural numbers always include <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>.</p> <h2 id="operations_and_relations">Operations and relations</h2> <p>We define the standard <a class="existingWikiWord" href="/nlab/show/arithmetic">arithmetic</a> and <a class="existingWikiWord" href="/nlab/show/metric">metric</a> operations and <a class="existingWikiWord" href="/nlab/show/order">order</a> relations of the <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> in <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> using <a class="existingWikiWord" href="/nlab/show/induction">induction</a> on the natural numbers.</p> <h3 id="addition"> Addition</h3> <p>Addition is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>+</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m + n:\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>+</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>+</mo><mn>0</mn><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">\vdash \beta_+^{0, 0}:0 + 0 =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>+</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>+</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_+^{0, s}(n):0 + s(n) =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>+</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>+</mo><mn>0</mn><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_+^{s, 0}(n):s(n) + 0 =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>+</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>+</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo>+</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_+^{s, s}(m, n):s(m) + s(n) =_\mathbb{N} s(s(m + n))</annotation></semantics></math></div> <h3 id="minimum_function"> Minimum function</h3> <p>The minimum function is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>min</mi><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \min(m, n):\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mi>min</mi> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mi>min</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">\vdash \beta_\min^{0, 0}:\min(0, 0) =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>min</mi> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>min</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\min^{0, s}(n):\min(0, s(n)) =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>min</mi> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>min</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\min^{s, 0}(n):\min(s(n), 0) =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>min</mi> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>min</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>min</mi><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\min^{s, s}(m, n):\min(s(m), s(n)) =_\mathbb{N} s(\min(m, n))</annotation></semantics></math></div> <h3 id="maximum_function">Maximum function</h3> <p>The maximum function is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>max</mi><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \max(m, n):\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mi>max</mi> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mi>max</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">\vdash \beta_\max^{0, 0}:\max(0, 0) =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>max</mi> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>max</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\max^{0, s}(n):\max(0, s(n)) =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>max</mi> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>max</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\max^{s, 0}(n):\max(s(n), 0) =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>max</mi> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>max</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>max</mi><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\max^{s, s}(m, n):\max(s(m), s(n)) =_\mathbb{N} s(\max(m, n))</annotation></semantics></math></div> <h3 id="distance_function"> Distance function</h3> <p>The distance function is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \rho(m, n):\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mi>ρ</mi> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mi>ρ</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">\vdash \beta_\rho^{0, 0}:\rho(0, 0) =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>ρ</mi> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ρ</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\rho^{0, s}(n):\rho(0, s(n)) =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>ρ</mi> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\rho^{s, 0}(n):\rho(s(n), 0) =_\mathbb{N} s(n)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mi>ρ</mi> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>ρ</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\rho^{s, s}(m, n):\rho(s(n), s(n)) =_\mathbb{N} \rho(n, n)</annotation></semantics></math></div> <h3 id="absolute_value">Absolute value</h3> <p>The absolute value is defined as the distance of a natural number from zero.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mo stretchy="false">|</mo><mi>n</mi><mo stretchy="false">|</mo><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \vert n \vert:\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msub><mi>δ</mi> <mrow><mo stretchy="false">|</mo><mo>−</mo><mo stretchy="false">|</mo></mrow></msub><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">|</mo><mi>n</mi><mo stretchy="false">|</mo><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>ρ</mi><mo stretchy="false">(</mo><mi>n</mi><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \delta_{\vert-\vert}(n):\vert n \vert =_\mathbb{N} \rho(n, 0)</annotation></semantics></math></div> <h3 id="less_than_relation">Less than relation</h3> <p>The less than relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo><</mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \lt n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo><</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo><</mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\lt^{0, 0}:0 \lt 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo><</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo><</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\lt^{0, s}(n):0 \lt s(n) \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo><</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo><</mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\lt^{s, 0}(n):s(n) \lt 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo><</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo><</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo><</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\lt^{s, s}(n):s(m) \lt s(n) \simeq m \lt n</annotation></semantics></math></div> <h3 id="less_than_or_equal_to_relation">Less than or equal to relation</h3> <p>The less than or equal to relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>≤</mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \leq n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>≤</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>≤</mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\leq^{0, 0}:0 \leq 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≤</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>≤</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\leq^{0, s}(n):0 \leq s(n) \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≤</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≤</mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\leq^{s, 0}(n):s(n) \leq 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≤</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo>≤</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\leq^{s, s}(n):s(m) \leq s(n) \simeq m \leq n</annotation></semantics></math></div> <h3 id="apart_from_relation">Apart from relation</h3> <p>The apart from relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>#</mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \# n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>#</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>#</mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\#^{0, 0}:0 \# 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>#</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>#</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\#^{0, s}(n):0 \# s(n) \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>#</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>#</mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\#^{s, 0}(n):s(n) \# 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>#</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>#</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo>#</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\#^{s, s}(n):s(m) \# s(n) \simeq m \# n</annotation></semantics></math></div> <h3 id="observational_equality_relation">Observational equality relation</h3> <p>The observational equality relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>≐</mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \doteq n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>≐</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>≐</mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\doteq^{0, 0}:0 \doteq 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≐</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>≐</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\doteq^{0, s}(n):0 \doteq s(n) \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≐</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≐</mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\doteq^{s, 0}(n):s(n) \doteq 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≐</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>≐</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo>≐</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\doteq^{s, s}(n):s(m) \doteq s(n) \simeq m \doteq n</annotation></semantics></math></div> <h3 id="greater_than_relation">Greater than relation</h3> <p>The greater than relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>></mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \gt n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>></mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>></mo><mn>0</mn><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\gt^{0, 0}:0 \gt 0 \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>></mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>></mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\gt^{0, s}(n):0 \gt s(n) \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>></mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>></mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\gt^{s, 0}(n):s(n) \gt 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>></mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>></mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo>></mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\gt^{s, s}(n):s(m) \gt s(n) \simeq m \gt n</annotation></semantics></math></div> <h3 id="greater_than_or_equal_to_relation">Greater than or equal to relation</h3> <p>The greater than or equal to relation is inductively defined by double induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>≥</mo><mi>n</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m \geq n \; \mathrm{type}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msubsup><mi>β</mi> <mo>≥</mo> <mrow><mn>0</mn><mo>,</mo><mn>0</mn></mrow></msubsup><mo>:</mo><mn>0</mn><mo>≥</mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">\vdash \beta_\geq^{0, 0}:0 \geq 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≥</mo> <mrow><mn>0</mn><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>≥</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>𝟘</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\geq^{0, s}(n):0 \geq s(n) \simeq \mathbb{0}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≥</mo> <mrow><mi>s</mi><mo>,</mo><mn>0</mn></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≥</mo><mn>0</mn><mo>≃</mo><mi>𝟙</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\geq^{s, 0}(n):s(n) \geq 0 \simeq \mathbb{1}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>≥</mo> <mrow><mi>s</mi><mo>,</mo><mi>s</mi></mrow></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>≥</mo><mi>s</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>m</mi><mo>≥</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\geq^{s, s}(n):s(m) \geq s(n) \simeq m \geq n</annotation></semantics></math></div> <h3 id="multiplication">Multiplication</h3> <p>Multiplication is inductively defined by induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><mi>m</mi><mo>+</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash m + n:\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>⋅</mo> <mn>0</mn></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mn>0</mn><mo>⋅</mo><mi>n</mi><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>0</mn></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\cdot^{0}(n):0 \cdot n =_\mathbb{N} 0</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>⋅</mo> <mi>s</mi></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo><mo>⋅</mo><mi>n</mi><msub><mo>=</mo> <mi>ℕ</mi></msub><mi>m</mi><mo>⋅</mo><mi>n</mi><mo>+</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\cdot^{s}(m, n):s(m) \cdot n =_\mathbb{N} m \cdot n + n</annotation></semantics></math></div> <h3 id="exponentiation">Exponentiation</h3> <p>Exponentiation is inductively defined by induction on the natural numbers</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msup><mi>n</mi> <mi>m</mi></msup><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash n^m:\mathbb{N}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mo>⋅</mo> <mn>0</mn></msubsup><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><msup><mi>n</mi> <mn>0</mn></msup><msub><mo>=</mo> <mi>ℕ</mi></msub><mn>1</mn></mrow><annotation encoding="application/x-tex">n:\mathbb{N} \vdash \beta_\cdot^{0}(n):n^0 =_\mathbb{N} 1</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi><mo>,</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>⊢</mo><msubsup><mi>β</mi> <mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow></msup></mrow> <mi>s</mi></msubsup><mo stretchy="false">(</mo><mi>m</mi><mo>,</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><msup><mi>n</mi> <mrow><mi>s</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">)</mo></mrow></msup><msub><mo>=</mo> <mi>ℕ</mi></msub><msup><mi>n</mi> <mi>m</mi></msup><mo>⋅</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}, n:\mathbb{N} \vdash \beta_{(-)^{(-)}}^{s}(m, n):n^{s(m)} =_\mathbb{N} n^m \cdot n</annotation></semantics></math></div> <h3 id="division_and_remainder">Division and remainder</h3> <p>Given a natural number <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>, we define the division function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>÷</mo><mi>n</mi><mo>:</mo><mi>ℕ</mi><mo>×</mo><msub><mi>ℕ</mi> <mo lspace="verythinmathspace" rspace="0em">+</mo></msub><mo>→</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m \div n: \mathbb{N} \times \mathbb{N}_{+} \to \mathbb{N}</annotation></semantics></math> such that</p> <ul> <li>for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><msub><mi>ℕ</mi> <mo lspace="verythinmathspace" rspace="0em">+</mo></msub></mrow><annotation encoding="application/x-tex">n:\mathbb{N}_{+}</annotation></semantics></math>, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo><</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m \lt n</annotation></semantics></math> then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>÷</mo><mi>n</mi><mo>=</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">m \div n = 0</annotation></semantics></math></li> <li>for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">m:\mathbb{N}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><msub><mi>ℕ</mi> <mo lspace="verythinmathspace" rspace="0em">+</mo></msub></mrow><annotation encoding="application/x-tex">n:\mathbb{N}_{+}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>m</mi><mo>+</mo><mi>n</mi><mo stretchy="false">)</mo><mo>÷</mo><mi>n</mi><mo>=</mo><mn>1</mn><mo>+</mo><mi>m</mi><mo>÷</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(m + n) \div n = 1 + m \div n)</annotation></semantics></math></li> </ul> <p>and the remainder function</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>m</mi><mspace width="thickmathspace"></mspace><mi>%</mi><mspace width="thickmathspace"></mspace><mi>n</mi><mo>≔</mo><mi>m</mi><mo>−</mo><mo stretchy="false">(</mo><mi>m</mi><mo>÷</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⋅</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m\ \%\ n \coloneqq m - (m \div n) \cdot n</annotation></semantics></math></div> <h2 id="natural_numbers_objects">Natural numbers objects</h2> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>N</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{N}</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>; indeed, it is the original example. This consists of an initial element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> (or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> is not used) and a successor operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>↦</mo><mi>n</mi><mo>+</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">n \mapsto n + 1</annotation></semantics></math> (or simply <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>↦</mo><msup><mi>n</mi> <mo>+</mo></msup></mrow><annotation encoding="application/x-tex">n \mapsto n^+</annotation></semantics></math>; in <a class="existingWikiWord" href="/nlab/show/computer+science">computer science</a>, one often writes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>+</mo></mrow><annotation encoding="application/x-tex">n+</annotation></semantics></math>) such that, for a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">a: X</annotation></semantics></math>, and a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">s: X \to X</annotation></semantics></math>, there exists a unique function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mstyle mathvariant="bold"><mi>N</mi></mstyle><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">f: \mathbf{N} \to X</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mn>0</mn></msub><mo>=</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">f_0 = a</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mrow><mi>n</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>n</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_{n+1} = s(f_n)</annotation></semantics></math>. This function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> is said to be constructed by <strong>primitive recursion</strong>. (Fancier forms of <a class="existingWikiWord" href="/nlab/show/recursion">recursion</a> are also possible.)</p> <p>The basic idea is that we define the values of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> one by one, starting with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mn>0</mn></msub><mo>=</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">f_0 = a</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mn>1</mn></msub><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_1 = s(a)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mn>2</mn></msub><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_2 = s(s(a))</annotation></semantics></math>, and so on. These are all both possible and necessary individually, but something must be put in the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> to ensure that this can go on uniquely forever.</p> <h2 id="properties">Properties</h2> <h3 id="minima_of_subsets_of_natural_numbers">Minima of subsets of natural numbers</h3> <p>In <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, any <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited</a> subset of the natural numbers possesses a minimal element. In <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, one cannot show this:</p> <div class="num_prop" id="BrouwerianCounterexample"> <h6 id="proposition">Proposition</h6> <p><strong>(a <a class="existingWikiWord" href="/nlab/show/Brouwerian+counterexample">Brouwerian counterexample</a>)</strong></p> <p>If every inhabited subset of the natural numbers possesses a minimal element, then the <a class="existingWikiWord" href="/nlab/show/excluded+middle">law of excluded middle</a> holds.</p> </div> <div class="proof"> <h6 id="proof">Proof</h6> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> be an arbitrary arithmetical formula. Then the subset</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>:</mo><mo>=</mo><mo stretchy="false">{</mo><mi>n</mi><mo>∈</mo><mi>ℕ</mi><mspace width="thinmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thinmathspace"></mspace><mi>n</mi><mo>=</mo><mn>1</mn><mo>∨</mo><mi>φ</mi><mo stretchy="false">}</mo><mo>⊆</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex"> U := \{ n \in \mathbb{N} \,|\, n = 1 \vee \varphi \} \subseteq \mathbb{N} </annotation></semantics></math></div> <p>is inhabited. By assumption, it possesses a minimal element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>n</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">n_0</annotation></semantics></math>. By discreteness of the natural numbers, either <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>n</mi> <mn>0</mn></msub><mo>=</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n_0 = 0</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>n</mi> <mn>0</mn></msub><mo>></mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n_0 \gt 0</annotation></semantics></math>. In the first case, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> holds. In the second case, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>φ</mi></mrow><annotation encoding="application/x-tex">\neg\varphi</annotation></semantics></math> holds.</p> </div> <p>In this sense, the natural numbers are not complete, and it’s fruitful to study their completion: For instance, the global sections of the completed natural numbers object in the <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">sheaf topos</a> on a topological space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> are in one-to-one correspondence with upper semicontinuous functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>→</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">X \to \mathbb{N}</annotation></semantics></math> (details at <em><a class="existingWikiWord" href="/nlab/show/one-sided+real+number">one-sided real number</a></em>).</p> <p>We can salvage the minimum principle in two ways:</p> <div class="num_prop"> <h6 id="proposition_2">Proposition</h6> <p>Any <strong><a class="existingWikiWord" href="/nlab/show/decidable+subset">detachable</a></strong> inhabited subset of the natural numbers possesses a minimal element.</p> </div> <div class="num_prop"> <h6 id="proposition_3">Proposition</h6> <p>Any inhabited subset of the natural numbers does <strong>not not</strong> possess a minimal element.</p> </div> <p>For instance, any finitely generated vector space over a <a class="existingWikiWord" href="/nlab/show/field">residue field</a> does <em>not not</em> possess a finite basis (pick a minimal generating set, guaranteed to <em>not not</em> exist). Interpreting this in the <a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a> of the sheaf topos of a <a class="existingWikiWord" href="/nlab/show/reduced+scheme">reduced scheme</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, one obtains the well-known fact that any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒪</mi> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">\mathcal{O}_X</annotation></semantics></math>-module locally of finite type over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is locally free on a dense open subset.</p> <h3 id="decreasing_sequences_of_natural_numbers">Decreasing sequences of natural numbers</h3> <p>Classically, any <em>weakly</em> decreasing sequence of natural numbers <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>a</mi> <mi>n</mi></msub><msub><mo stretchy="false">)</mo> <mi>n</mi></msub></mrow><annotation encoding="application/x-tex">(a_n)_n</annotation></semantics></math> is eventually constant, i.e. admits an index <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>a</mi> <mi>N</mi></msub><mo>=</mo><msub><mi>a</mi> <mrow><mi>N</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>=</mo><msub><mi>a</mi> <mrow><mi>N</mi><mo>+</mo><mn>2</mn></mrow></msub><mo>=</mo><mi>⋯</mi></mrow><annotation encoding="application/x-tex">a_N = a_{N+1} = a_{N+2} = \cdots</annotation></semantics></math>. Constructively, one can only prove for each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> that there exists an index <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>a</mi> <mi>N</mi></msub><mo>=</mo><msub><mi>a</mi> <mrow><mi>N</mi><mo>+</mo><mn>1</mn></mrow></msub><mo>=</mo><mi>⋯</mi><mo>=</mo><msub><mi>a</mi> <mrow><mi>N</mi><mo>+</mo><mi>M</mi></mrow></msub></mrow><annotation encoding="application/x-tex">a_N = a_{N+1} = \cdots = a_{N+M}</annotation></semantics></math>. (One may prove this by induction on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>a</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">a_0</annotation></semantics></math>; indeed, you can always find <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi><mo>≤</mo><msub><mi>a</mi> <mn>0</mn></msub><mi>M</mi></mrow><annotation encoding="application/x-tex">N \leq a_0 M</annotation></semantics></math>.) The classical principle is equivalent to the <a class="existingWikiWord" href="/nlab/show/limited+principle+of+omniscience">limited principle of omniscience</a> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> (which follows already when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>a</mi> <mn>0</mn></msub><mo>=</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">a_0 = 1</annotation></semantics></math>).</p> <p>On the other hand, there can be no <em>strictly</em> decreasing sequence of natural numbers. This is constuctively valid (proved by contradiction and induction on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>a</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">a_0</annotation></semantics></math>).</p> <p>This is relevant to <span class="newWikiWord">constructive algebra<a href="/nlab/new/constructive+algebra">?</a></span>, as this shows that formulating chain conditions needs some care. (It is easier to say ‘weakly’ than ‘strictly’ in the hypothesis, but then it's unclear how to state the conclusion.)</p> <h2 id="Examples">Examples</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/0">0</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/1">1</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/24">24</a></p> </li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/number">number</a>, <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a>, <a class="existingWikiWord" href="/nlab/show/integer">integer</a>, <a class="existingWikiWord" href="/nlab/show/rational+number">rational number</a>, <a class="existingWikiWord" href="/nlab/show/algebraic+number">algebraic number</a>, <a class="existingWikiWord" href="/nlab/show/Gaussian+number">Gaussian number</a>, <a class="existingWikiWord" href="/nlab/show/irrational+number">irrational number</a>, <a class="existingWikiWord" href="/nlab/show/real+number">real number</a>, <a class="existingWikiWord" href="/nlab/show/p-adic+number">p-adic number</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+numbers+type">natural numbers type</a>, <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decimal+numeral+representation+of+the+natural+numbers">decimal numeral representation of the natural numbers</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/conatural+number">conatural number</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/carrying">carrying</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/currying">currying</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/numeral">numeral</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/countable+ordinal">countable ordinal</a></p> </li> </ul> <h2 id="references">References</h2> <p>Origin of the <a class="existingWikiWord" href="/nlab/show/Dedekind-Peano+axioms">Dedekind-Peano axioms</a> for the <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Richard+Dedekind">Richard Dedekind</a>, <em>Was sind und was sollen die Zahlen?</em> (1888) [scan: <a href="https://rcin.org.pl/Content/37485/WA35_52499_2264brosz_Was-sind.pdf">pdf</a>, <a href="https://doi.org/10.1007/978-3-663-02788-1">doi:10.1007/978-3-663-02788-1</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Richard+Dedekind">Richard Dedekind</a> (transl. by W. Beman), <em>The nature and meaning of numbers</em>, Chapter II in: <em>Essays on the Theory of Numbers</em>, Chicago (1901) [<a href="http://www.gutenberg.org/ebooks/21016">Project Gutenberg</a>, <a href="https://www.gutenberg.org/files/21016/21016-pdf.pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Giuseppe+Peano">Giuseppe Peano</a>, <em>Arithmetices principia, nova methodo exposita</em>, [<a href="https://en.wikipedia.org/wiki/Arithmetices_principia,_nova_methodo_exposita">Wikipedia</a>]</p> </li> </ul> <p>Review:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/David+E.+Joyce">David E. Joyce</a>, <em>The Dedekind/Peano Axioms</em> (2005) [<a href="http://aleph0.clarku.edu/~djoyce/numbers/peano.pdf">pdf</a>]</li> </ul> <p>Broader historical review:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Leo+Corry">Leo Corry</a>, <em>A Brief History of Numbers</em>, Oxford University Press (2015) [<a href="https://global.oup.com/academic/product/a-brief-history-of-numbers-9780198702597">ISBN:9780198702597</a>]</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 16, 2023 at 10:11:57. See the <a href="/nlab/history/natural+number" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/natural+number" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/13006/#Item_8">Discuss</a><span class="backintime"><a href="/nlab/revision/natural+number/37" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/natural+number" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/natural+number" accesskey="S" class="navlink" id="history" rel="nofollow">History (37 revisions)</a> <a href="/nlab/show/natural+number/cite" style="color: black">Cite</a> <a href="/nlab/print/natural+number" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/natural+number" id="view_source" rel="nofollow">Source</a> </div> </div> <!-- Content --> </div> <!-- Container --> </body> </html>