CINXE.COM

<!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 (changes) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <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[/*></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[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </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 (changes) </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/diff/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"> <p class="show_diff"> Showing changes from revision #37 to #38: <ins class="diffins">Added</ins> | <del class="diffdel">Removed</del> | <del class="diffmod">Chan</del><ins class="diffmod">ged</ins> </p> <div class='rightHandSide'> <div class='toc clickDown' tabindex='0'> <h3 id='context'>Context</h3> <h4 id='arithmetic'>Arithmetic</h4> <div class='hide'> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/number+theory'>number theory</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic'>arithmetic</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+geometry'>arithmetic geometry</a>, <a class='existingWikiWord' href='/nlab/show/diff/arithmetic+topology'>arithmetic topology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+dimensional+arithmetic+geometry'>higher arithmetic geometry</a>, <a class='existingWikiWord' href='/nlab/show/diff/E-%E2%88%9E+geometry'>E-∞ arithmetic geometry</a></p> </li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/number'>number</a></strong></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural number</a>, <a class='existingWikiWord' href='/nlab/show/diff/integer'>integer number</a>, <a class='existingWikiWord' href='/nlab/show/diff/rational+number'>rational number</a>, <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real number</a>, <a class='existingWikiWord' href='/nlab/show/diff/irrational+number'>irrational number</a>, <a class='existingWikiWord' href='/nlab/show/diff/complex+number'>complex number</a>, <a class='existingWikiWord' href='/nlab/show/diff/quaternion'>quaternion</a>, <a class='existingWikiWord' href='/nlab/show/diff/octonion'>octonion</a>, <a class='existingWikiWord' href='/nlab/show/diff/p-adic+number'>adic number</a>, <a class='existingWikiWord' href='/nlab/show/diff/cardinal+number'>cardinal number</a>, <a class='existingWikiWord' href='/nlab/show/diff/ordinal+number'>ordinal number</a>, <a class='existingWikiWord' href='/nlab/show/diff/surreal+number'>surreal number</a></li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/arithmetic'>arithmetic</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Peano+arithmetic'>Peano arithmetic</a>, <a class='existingWikiWord' href='/nlab/show/diff/second-order+arithmetic'>second-order arithmetic</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/transfinite+arithmetic'>transfinite arithmetic</a>, <a class='existingWikiWord' href='/nlab/show/diff/cardinal+arithmetic'>cardinal arithmetic</a>, <a class='existingWikiWord' href='/nlab/show/diff/ordinal+arithmetic'>ordinal arithmetic</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/prime+field'>prime field</a>, <a class='existingWikiWord' href='/nlab/show/diff/p-adic+integer'>p-adic integer</a>, <a class='existingWikiWord' href='/nlab/show/diff/p-adic+number'>p-adic rational number</a>, <a class='existingWikiWord' href='/nlab/show/diff/p-adic+complex+number'>p-adic complex number</a></p> </li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+geometry'>arithmetic geometry</a></strong>, <a class='existingWikiWord' href='/nlab/show/diff/function+field+analogy'>function field analogy</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+scheme'>arithmetic scheme</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+curve'>arithmetic curve</a>, <a class='existingWikiWord' href='/nlab/show/diff/elliptic+curve'>elliptic curve</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+genus'>arithmetic genus</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+Chern-Simons+theory'>arithmetic Chern-Simons theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+Chow+group'>arithmetic Chow group</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Weil-%C3%A9tale+topology+for+arithmetic+schemes'>Weil-étale topology for arithmetic schemes</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/absolute+cohomology'>absolute cohomology</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Weil+conjecture+on+Tamagawa+numbers'>Weil conjecture on Tamagawa numbers</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Borger%27s+absolute+geometry'>Borger's absolute geometry</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Iwasawa-Tate+theory'>Iwasawa-Tate theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+jet+space'>arithmetic jet space</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/adelic+integral'>adelic integration</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/shtuka'>shtuka</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Frobenioid'>Frobenioid</a></p> </li> </ul> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/Arakelov+geometry'>Arakelov geometry</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/arithmetic+Riemann-Roch+theorem'>arithmetic Riemann-Roch theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/differential+algebraic+K-theory'>differential algebraic K-theory</a></p> </li> </ul> </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><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><li><a href='#natural_numbers_objects'>Natural numbers objects</a></li><li><a href='#properties'>Properties</a><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><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/diff/number'>numbers</a> <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_1' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>1</mn></mrow><annotation encoding='application/x-tex'>1</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>2</mn></mrow><annotation encoding='application/x-tex'>2</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_3' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_4' xmlns='http://www.w3.org/1998/Math/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/diff/cardinal+number'>cardinality</a> of a <a class='existingWikiWord' href='/nlab/show/diff/finite+set'>finite set</a>, as well as a finite <a class='existingWikiWord' href='/nlab/show/diff/ordinal+number'>ordinal number</a>. One can distinguish these as the <strong>nonnegative integers</strong> (with <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_5' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math>) and the <strong>positive integers</strong> (without <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_6' xmlns='http://www.w3.org/1998/Math/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/diff/set+theory'>set theorist</a>, a natural number is essentially the same as an <strong><a class='existingWikiWord' href='/nlab/show/diff/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math>). In school mathematics, natural numbers with <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_8' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>N</mi></mrow><annotation encoding='application/x-tex'>N</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mstyle mathvariant='bold'><mi>N</mi></mstyle></mrow><annotation encoding='application/x-tex'>\mathbf{N}</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{N}</annotation></semantics></math>, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ω</mi></mrow><annotation encoding='application/x-tex'>\omega</annotation></semantics></math>, or <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_13' xmlns='http://www.w3.org/1998/Math/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/diff/ordinal+number'>ordinal number</a> or <a class='existingWikiWord' href='/nlab/show/diff/cardinal+number'>cardinal number</a> respectively, and they often (usually for <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℵ</mi></mrow><annotation encoding='application/x-tex'>\aleph</annotation></semantics></math>) have a subscript <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_15' xmlns='http://www.w3.org/1998/Math/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/diff/foundation+of+mathematics'>foundations</a> of mathematics, the <a class='existingWikiWord' href='/nlab/show/diff/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_16' xmlns='http://www.w3.org/1998/Math/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/diff/set'>sets</a> (and even as <a class='existingWikiWord' href='/nlab/show/diff/natural+numbers+object'>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/diff/semigroup'>semigroup</a> structure (or <a class='existingWikiWord' href='/nlab/show/diff/inclusion+function'>inclusion map</a> into the set of <a class='existingWikiWord' href='/nlab/show/diff/integer'>integers</a>, etc).</p> <p>By default, our natural numbers always include <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_17' xmlns='http://www.w3.org/1998/Math/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/diff/arithmetic'>arithmetic</a> and <a class='existingWikiWord' href='/nlab/show/diff/metric+space'>metric</a> operations and <a class='existingWikiWord' href='/nlab/show/diff/order'>order</a> relations of the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a> in <a class='existingWikiWord' href='/nlab/show/diff/dependent+type+theory'>dependent type theory</a> using <a class='existingWikiWord' href='/nlab/show/diff/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_18' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_19' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_20' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_21' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_22' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_23' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_24' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_25' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_26' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_27' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_28' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_29' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_30' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_31' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_32' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_33' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_34' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_35' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_36' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_37' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_38' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_39' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_40' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_41' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_42' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_43' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_44' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_45' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_46' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_47' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_48' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_49' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_50' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_51' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_52' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_53' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_54' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_55' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_56' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_57' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_58' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_59' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_60' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_61' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_62' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_63' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_64' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_65' xmlns='http://www.w3.org/1998/Math/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' /><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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_66' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_67' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_68' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_69' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_70' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_71' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_72' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_73' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_74' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_75' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_76' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi></mrow><annotation encoding='application/x-tex'>n</annotation></semantics></math>, we define the division function <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_77' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_78' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>m:\mathbb{N}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_79' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_80' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_81' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_82' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>m:\mathbb{N}</annotation></semantics></math> and <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_83' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_84' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_85' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>m</mi><mspace width='thickmathspace' /><mi>%</mi><mspace width='thickmathspace' /><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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_86' xmlns='http://www.w3.org/1998/Math/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/diff/natural+numbers+object'>natural numbers object</a> in <a class='existingWikiWord' href='/nlab/show/diff/Set'>Set</a>; indeed, it is the original example. This consists of an initial element <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_87' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math> (or <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_88' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>1</mn></mrow><annotation encoding='application/x-tex'>1</annotation></semantics></math> if <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_89' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math> is not used) and a successor operation <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_90' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_91' xmlns='http://www.w3.org/1998/Math/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/diff/computer+science'>computer science</a>, one often writes <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_92' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>n</mi><mo>+</mo></mrow><annotation encoding='application/x-tex'>n+</annotation></semantics></math>) such that, for a set <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_93' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>, an element <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_94' xmlns='http://www.w3.org/1998/Math/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/diff/function'>function</a> <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_95' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_96' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_97' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_98' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_99' xmlns='http://www.w3.org/1998/Math/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/diff/recursion'>recursion</a> are also possible.)</p> <p>The basic idea is that we define the values of <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_100' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>f</mi></mrow><annotation encoding='application/x-tex'>f</annotation></semantics></math> one by one, starting with <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_101' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_102' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_103' xmlns='http://www.w3.org/1998/Math/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/diff/foundation+of+mathematics'>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/diff/classical+mathematics'>classical mathematics</a>, any <a class='existingWikiWord' href='/nlab/show/diff/inhabited+set'>inhabited</a> subset of the natural numbers possesses a minimal element. In <a class='existingWikiWord' href='/nlab/show/diff/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/diff/taboo'>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/diff/excluded+middle'>law of excluded middle</a> holds.</p> </div> <div class='proof'> <h6 id='proof'>Proof</h6> <p>Let <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_104' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='block' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_105' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>U</mi><mo>:</mo><mo>=</mo><mo stretchy='false'>{</mo><mi>n</mi><mo>∈</mo><mi>ℕ</mi><mspace width='thinmathspace' /><mo stretchy='false'>|</mo><mspace width='thinmathspace' /><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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_106' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_107' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_108' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_109' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>φ</mi></mrow><annotation encoding='application/x-tex'>\varphi</annotation></semantics></math> holds. In the second case, <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_110' xmlns='http://www.w3.org/1998/Math/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/diff/category+of+sheaves'>sheaf topos</a> on a topological space <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_111' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_112' xmlns='http://www.w3.org/1998/Math/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/diff/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/diff/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/diff/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/diff/internal+logic'>internal language</a> of the sheaf topos of a <a class='existingWikiWord' href='/nlab/show/diff/reduced+scheme'>reduced scheme</a> <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_113' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_114' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_115' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_116' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_117' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>N</mi></mrow><annotation encoding='application/x-tex'>N</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_118' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_119' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>M</mi></mrow><annotation encoding='application/x-tex'>M</annotation></semantics></math> that there exists an index <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_120' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>N</mi></mrow><annotation encoding='application/x-tex'>N</annotation></semantics></math> such that <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_121' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_122' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_123' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>N</mi></mrow><annotation encoding='application/x-tex'>N</annotation></semantics></math> so that <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_124' xmlns='http://www.w3.org/1998/Math/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/diff/limited+principle+of+omniscience'>limited principle of omniscience</a> for <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_125' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{N}</annotation></semantics></math> (which follows already when <math class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_126' xmlns='http://www.w3.org/1998/Math/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 class='maruku-mathml' display='inline' id='mathml_085285a46699200616c7259775ec86a8a72b6ab7_127' xmlns='http://www.w3.org/1998/Math/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/diff/zero'>0</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/one'>1</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/24'>24</a></p> </li> </ul> <h2 id='related_concepts'>Related concepts</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/number'>number</a>, <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural number</a>, <a class='existingWikiWord' href='/nlab/show/diff/integer'>integer</a>, <a class='existingWikiWord' href='/nlab/show/diff/rational+number'>rational number</a>, <a class='existingWikiWord' href='/nlab/show/diff/algebraic+number'>algebraic number</a>, <a class='existingWikiWord' href='/nlab/show/diff/Gaussian+number'>Gaussian number</a>, <a class='existingWikiWord' href='/nlab/show/diff/irrational+number'>irrational number</a>, <a class='existingWikiWord' href='/nlab/show/diff/real+number'>real number</a>, <a class='existingWikiWord' href='/nlab/show/diff/p-adic+number'>p-adic number</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/natural+numbers+type'>natural numbers type</a>, <a class='existingWikiWord' href='/nlab/show/diff/natural+numbers+object'>natural numbers object</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/decimal+numeral+representation+of+the+natural+numbers'>decimal numeral representation of the natural numbers</a></p> </li> <ins class='diffins'><li> <p><a class='existingWikiWord' href='/nlab/show/diff/extended+natural+number'>conatural number</a></p> </li></ins><ins class='diffins'> </ins><li> <p><a class='existingWikiWord' href='/nlab/show/diff/carrying'>carrying</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/currying'>currying</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/numeral'>numeral</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/countable+ordinal'>countable ordinal</a></p> </li> </ul> <h2 id='references'>References</h2> <p>Origin of the <a class='existingWikiWord' href='/nlab/show/diff/Peano+arithmetic'>Dedekind-Peano axioms</a> for the <a class='existingWikiWord' href='/nlab/show/diff/natural+number'>natural numbers</a>:</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Richard+Dedekind'>Richard Dedekind</a>, <em>Was sind und was sollen die Zahlen?</em> (1888) [scan: pdf, doi:10.1007/978-3-663-02788-1]</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/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) [[Project Gutenberg](http://www.gutenberg.org/ebooks/21016), <a href='https://www.gutenberg.org/files/21016/21016-pdf.pdf'>pdf</a>]</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Giuseppe+Peano'>Giuseppe Peano</a>, <em>Arithmetices principia, nova methodo exposita</em>, [[Wikipedia](https://en.wikipedia.org/wiki/Arithmetices_principia,_nova_methodo_exposita)]</p> </li> </ul> <p>Review:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/David+Joyce'>David E. Joyce</a>, <em>The Dedekind/Peano Axioms</em> (2005) [[pdf](http://aleph0.clarku.edu/~djoyce/numbers/peano.pdf)]</li> </ul> <p>Broader historical review:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Leo+Corry'>Leo Corry</a>, <em>A Brief History of Numbers</em>, Oxford University Press (2015) [[ISBN:9780198702597](https://global.oup.com/academic/product/a-brief-history-of-numbers-9780198702597)]</li> </ul> <p> </p> <p> </p> <p> </p> </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/diff/natural+number/37" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/natural+number" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</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>  </div>  </body> </html>