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> internal logic 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[/*></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> internal logic </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/500/#Item_30" 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="categorical_algebra">Categorical algebra</h4> <div class="hide"><div> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>+<a class="existingWikiWord" href="/nlab/show/algebra">algebra</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/internalization">internalization</a> and <a class="existingWikiWord" href="/nlab/show/categorical+algebra">categorical algebra</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoid+object">monoid object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/group+object">group object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ring+object">ring object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+object">algebra object</a> (associative, <a class="existingWikiWord" href="/nlab/show/Lie+algebra+object">Lie</a>, …)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/module+object">module object</a>/<a class="existingWikiWord" href="/nlab/show/action+object">action object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+locale">internal locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+category">internal category</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/internal+infinity-categories+contents">more</a>)</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+groupoid">internal groupoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+site">internal site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+diagram">internal diagram</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/universal+algebra">universal algebra</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+a+Lawvere+theory">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/algebraic+theories">algebraic theories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+a+monad">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/monads">monads</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+an+operad">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/operads">operads</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+category+theory+and+type+theory">relation between category theory and type theory</a></p> </li> </ul> </div></div> <h4 id="topos_theory">Topos Theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Toposes">Toposes</a></li> </ul> <h2 id="background">Background</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> </ul> </li> </ul> <h2 id="toposes">Toposes</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+presheaves">category of presheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable presheaf</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/site">site</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sieve">sieve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/coverage">coverage</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+pretopology">pretopology</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+topology">topology</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheafification">sheafification</a></p> </li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quasitopos">quasitopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+topos">base topos</a>, <a class="existingWikiWord" href="/nlab/show/indexed+topos">indexed topos</a></p> </li> </ul> <h2 id="internal_logic">Internal Logic</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a></p> </li> </ul> </li> </ul> <h2 id="topos_morphisms">Topos morphisms</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/logical+morphism">logical morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/direct+image">direct image</a>/<a class="existingWikiWord" href="/nlab/show/inverse+image">inverse image</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/global+section">global sections</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/surjective+geometric+morphism">surjective geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/essential+geometric+morphism">essential geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+geometric+morphism">locally connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected+geometric+morphism">connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/totally+connected+geometric+morphism">totally connected geometric morphism</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%C3%A9tale+geometric+morphism">étale geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+geometric+morphism">open geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proper+geometric+morphism">proper geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/compact+topos">compact topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/separated+geometric+morphism">separated geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/Hausdorff+topos">Hausdorff topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+geometric+morphism">local geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bounded+geometric+morphism">bounded geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+change">base change</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+geometric+morphism">localic geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperconnected+geometric+morphism">hyperconnected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/atomic+geometric+morphism">atomic geometric morphism</a></p> </li> </ul> </li> </ul> <h2 id="extra_stuff_structure_properties">Extra stuff, structure, properties</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+locale">topological locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+topos">localic topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/petit+topos">petit topos/gros topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+topos">locally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/connected+topos">connected topos</a>, <a class="existingWikiWord" href="/nlab/show/totally+connected+topos">totally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/strongly+connected+topos">strongly connected topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+topos">local topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+topos">cohesive topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/smooth+topos">smooth topos</a></p> </li> </ul> <h2 id="cohomology_and_homotopy">Cohomology and homotopy</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+groups+in+an+%28infinity%2C1%29-topos">homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/abelian+sheaf+cohomology">abelian sheaf cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+structure+on+simplicial+presheaves">model structure on simplicial presheaves</a></p> </li> </ul> <h2 id="in_higher_category_theory">In higher category theory</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-site">(0,1)-site</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-topos">2-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-site">2-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-sheaf">2-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/stack">stack</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-site">(∞,1)-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf">(∞,1)-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stack">∞-stack</a>, <a class="existingWikiWord" href="/nlab/show/derived+stack">derived stack</a></p> </li> </ul> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Diaconescu%27s+theorem">Diaconescu's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Barr%27s+theorem">Barr's theorem</a></p> </li> </ul> <div> <p> <a href="/nlab/edit/topos+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <ul> <li><a href='#kinds_of_internal_logics_in_different_categories'>Kinds of internal logics in different categories</a></li> </ul> <li><a href='#internal_firstorder_logic'>Internal first-order logic</a></li> <ul> <li><a href='#theories'>Theories</a></li> <li><a href='#CategoricalSemantics'>Categorical semantics</a></li> <li><a href='#the_internal_logic_as_a_functor'>The internal logic as a functor</a></li> </ul> <li><a href='#soundness_and_internal_reasoning'>Soundness and internal reasoning</a></li> <li><a href='#syntactic_categories'>Completeness, syntactic categories, and Morita equivalence</a></li> <li><a href='#kripkejoyal_semantics'>Kripke–Joyal semantics</a></li> <li><a href='#dependent_type_theory'>Dependent type theory</a></li> <li><a href='#higherorder_logic'>Higher-order logic</a></li> <li><a href='#examples'>Examples</a></li> <ul> <li><a href='#LogicOfSet'>Internal logic in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math></a></li> <li><a href='#LogicOfPresheaves'>Internal logic in a sheaf topos on open subsets</a></li> </ul> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> <ul> <li><a href='#general'>General</a></li> <li><a href='#Applications'>Applications</a></li> </ul> </ul> </div> <h2 id="idea">Idea</h2> <p>One of the most important observations of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> is that large parts of mathematics can be <a class="existingWikiWord" href="/nlab/show/internalization">internalized</a> in any <a class="existingWikiWord" href="/nlab/show/category">category</a> with sufficient structure. The most basic examples of this involve algebraic structures; for instance, a <a class="existingWikiWord" href="/nlab/show/group">group</a> can be defined in any category with finite products, and an <a class="existingWikiWord" href="/nlab/show/internal+category">internal</a> <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a> can be defined in any ambient category with <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a>s. For such <a class="existingWikiWord" href="/nlab/show/algebraic+theory">algebraic</a> (or even <a class="existingWikiWord" href="/nlab/show/essentially+algebraic+theory">essentially algebraic</a>) structures, which are defined by <em>operations</em> with <em>equational axioms</em> imposed, it suffices for the ambient category to have (usually finite) limits.</p> <p>However, if we assume that the ambient category has additional structure, then much more of mathematics can be internalized, potentially including <a class="existingWikiWord" href="/nlab/show/field">field</a>s, <a class="existingWikiWord" href="/nlab/show/local+ring">local ring</a>s, <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a>s, <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>s, even the field of <a class="existingWikiWord" href="/nlab/show/real+number">real number</a>s. The idea is to exploit the fact that all mathematics can be written in the language of <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, and seek a way to internalize logic in a category with sufficient structure.</p> <p>The basic ideas of the internal logic induced by a given <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> are:</p> <ul> <li> <p>the <a class="existingWikiWord" href="/nlab/show/object">object</a>s <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> are regarded as collections of things of a given <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math></p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\to B</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> are regarded as terms of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> containing a free <a class="existingWikiWord" href="/nlab/show/variable">variable</a> of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> (i.e. in a <a class="existingWikiWord" href="/nlab/show/context">context</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math>)</p> </li> <li> <p>a <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mo>↪</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\phi \hookrightarrow A</annotation></semantics></math> is regarded as a <em>proposition</em> (<a class="existingWikiWord" href="/nlab/show/predicate">predicate</a>): by thinking of it as the sub-collection of all those things of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> for which the statement <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi></mrow><annotation encoding="application/x-tex">\phi</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/true">true</a></p> <ul> <li> <p>the maximal subobject is hence the proposition that is always true; this is the logical object of <a class="existingWikiWord" href="/nlab/show/truth">truth</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo>↪</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\top \hookrightarrow A</annotation></semantics></math></p> </li> <li> <p>the minimal subobject is hence the proposition that is always false; this is the logical object of <a class="existingWikiWord" href="/nlab/show/falsity">falsity</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo><mo>↪</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\bottom \hookrightarrow A</annotation></semantics></math></p> </li> <li> <p>one proposition <a class="existingWikiWord" href="/nlab/show/implication">implies</a> another if as subobjects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> they are connected by a morphism in the <a class="existingWikiWord" href="/nlab/show/poset">poset</a> of subobjects: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mo>⇒</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\phi \Rightarrow \psi</annotation></semantics></math> means <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mo>↪</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\phi \hookrightarrow \psi</annotation></semantics></math></p> </li> </ul> </li> <li> <p>Logical operations are implemented by <a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a>s on <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a>s.</p> <ul> <li> <p>the conjunction <a class="existingWikiWord" href="/nlab/show/and">and</a> is the <a class="existingWikiWord" href="/nlab/show/product">product</a> of subobjects (their <a class="existingWikiWord" href="/nlab/show/meet">meet</a>)</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> <a class="existingWikiWord" href="/nlab/show/or">or</a> is the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> of subobjects (their <a class="existingWikiWord" href="/nlab/show/join">join</a>)</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a> is the <a class="existingWikiWord" href="/nlab/show/support">support</a> of the <a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> of subobjects</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a> is the <a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> of subobjects</p> </li> </ul> </li> </ul> <p>and so on.</p> <ul> <li>A <a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a> over an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> may be interpreted as a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">B\to A</annotation></semantics></math> whose “fibers” represent the types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(x)</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math>. This morphism might be restricted to be a <a class="existingWikiWord" href="/nlab/show/display+map">display map</a> or a <a class="existingWikiWord" href="/nlab/show/fibration">fibration</a>.</li> </ul> <p>Once we formalize the notion of “logical <a class="existingWikiWord" href="/nlab/show/theory">theory</a>”, the construction of the internal logic can be interpreted as a <a class="existingWikiWord" href="/nlab/show/functor">functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi></mrow><annotation encoding="application/x-tex">Lang</annotation></semantics></math> from suitably structured categories to theories. The morphisms of theories are “interpretations”, and so an internalization of some theory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> (such as the “theory of groups”) into a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a morphism of theories <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>→</mo><mi>Lang</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T\to Lang(C)</annotation></semantics></math>.</p> <p>Moreover, the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi></mrow><annotation encoding="application/x-tex">Lang</annotation></semantics></math> has a left <a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a>: the <a class="existingWikiWord" href="/nlab/show/syntactic+category">syntactic category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Syn</mi></mrow><annotation encoding="application/x-tex">Syn</annotation></semantics></math> of a theory. Thus, a model of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is equally well a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Syn</mi><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">Syn(T)\to C</annotation></semantics></math>. Frequently, this adjunction is even an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>; see <a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a>.</p> <h3 id="kinds_of_internal_logics_in_different_categories">Kinds of internal logics in different categories</h3> <p>There are many different kinds of of “logical theories”, each of which corresponds to a type of category in which such theories can be internalized (and yields a corresponding adjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Syn</mi><mo>⊣</mo><mi>Lang</mi></mrow><annotation encoding="application/x-tex">Syn \dashv Lang</annotation></semantics></math>).</p> <table><thead><tr><th>Theory</th><th></th><th>Category</th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Lawvere+theory">Lawvere</a> (or “finite product”)</td><td style="text-align: left;"></td><td style="text-align: left;">category with <a class="existingWikiWord" href="/nlab/show/finite+products">finite products</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+logic">cartesian</a>/<a class="existingWikiWord" href="/nlab/show/essentially+algebraic+theory">essentially algebraic</a> (or “left exact” or “finite limit”)</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/finitely+complete+category">finitely complete category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/minimal+logic">minimal logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+logic">regular</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+logic">coherent</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+category">coherent category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunctive+logic">disjunctive</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/pre-lextensive+category">pre-lextensive category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+logic">geometric</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+category">infinitary coherent category</a> (aka <a class="existingWikiWord" href="/nlab/show/geometric+category">geometric category</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive</a> <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/classical+logic">classical</a> <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Boolean+category">Boolean category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/extensional+type+theory">extensional</a> <a class="existingWikiWord" href="/nlab/show/dependent+types">dependent types</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive</a> <a class="existingWikiWord" href="/nlab/show/higher+order+logic">higher order</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/topos">elementary topos</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/classical+logic">classical</a> <a class="existingWikiWord" href="/nlab/show/higher+order+logic">higher order</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Boolean+topos">Boolean topos</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric monoidal category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive modal logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cohesive+topos">cohesive topos</a></td></tr> </tbody></table> <p>Each type of logic up to and including “geometric” can also be described in terms of <a class="existingWikiWord" href="/nlab/show/sketch">sketches</a>. Not coincidentally, the corresponding types of category up to and including “geometric” fit into the framework of <a class="existingWikiWord" href="/nlab/show/familial+regularity+and+exactness">familial regularity and exactness</a>. Sketches can also describe theories applicable to categories not even having finite products, such as finite sum sketches, but the type-theoretic approach taken on this page requires at least finite products (or else something closely akin, such as a <a class="existingWikiWord" href="/nlab/show/cartesian+multicategory">cartesian multicategory</a>).</p> <p>However, there are other sorts of <a class="existingWikiWord" href="/nlab/show/internalization">internalization</a> that do not fit in this framework. For instance, to describe a <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a> internal to a <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a>, one needs an internal <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a>. See <a class="existingWikiWord" href="/nlab/show/internalization">internalization</a> for a discussion of the more general notion in the context of <a class="existingWikiWord" href="/nlab/show/doctrine">doctrine</a>s.</p> <h2 id="internal_firstorder_logic">Internal first-order logic</h2> <p>We begin with the interpretation of internal first-order logic, which is the most used in <a class="existingWikiWord" href="/nlab/show/toposes">toposes</a> and related categories.</p> <h3 id="theories">Theories</h3> <p>In this section, what we mean by a <em>theory</em> is a <em><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></em> without dependent types, but with a dependent logic. This entails the following.</p> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/signature+%28in+logic%29">signature</a> of the theory consists of</p> <ul> <li> <p>Various <em><a class="existingWikiWord" href="/nlab/show/types">types</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">A,B,C</annotation></semantics></math>. For example, the theory of a group has only one type (group elements), but the theory of a-ring-and-a-module has two types (ring elements and module elements). There are also generally <em>type constructors</em> that build new types from basic ones, such as product types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\times B</annotation></semantics></math> and the unit type <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>.</p> </li> <li> <p>The theory will also generally contain <em><a class="existingWikiWord" href="/nlab/show/function+symbol">function symbol</a>s</em> such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math>, each with a source and target that are types. For example, the theory of a monoid has one type <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>, one function symbol <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>M</mi><mo>×</mo><mi>M</mi><mo>→</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">m:M\times M\to M</annotation></semantics></math>, and one function symbol <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>M</mi></mrow><annotation encoding="application/x-tex">e:1\to M</annotation></semantics></math>. Function symbols of source <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> are also called <em>constants</em>.</p> </li> <li> <p>The theory may also contain <em><a class="existingWikiWord" href="/nlab/show/relation+symbol">relation symbol</a>s</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">R:A</annotation></semantics></math>, each equipped with a type. For example, the theory of a <a class="existingWikiWord" href="/nlab/show/partial+order">poset</a> has one type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> and one relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo><mo>:</mo><mi>P</mi><mo>×</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\le:P\times P</annotation></semantics></math>. The most basic relation symbol, which most theories contain, is <em><a class="existingWikiWord" href="/nlab/show/equality">equality</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>=</mo> <mi>A</mi></msub><mo>:</mo><mi>A</mi><mo>×</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">=_A:A\times A</annotation></semantics></math> on a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> </li> </ul> </li> <li> <p>Finally the theory may contain <em>logical <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a>s</em> of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo stretchy="false">|</mo><mi>φ</mi><mo>⊢</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\Gamma | \varphi \vdash \psi</annotation></semantics></math>. Here <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math> are first-order formulas built up from terms and relation symbols using logical connectives and quantifiers such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo>,</mo><mo>⊥</mo><mo>,</mo><mo>∧</mo><mo>,</mo><mo>∨</mo><mo>,</mo><mo>⇒</mo><mo>,</mo><mo>¬</mo><mo>,</mo><mo>∀</mo><mo>,</mo><mo>∃</mo></mrow><annotation encoding="application/x-tex">\top,\bot,\wedge,\vee,\Rightarrow,\neg,\forall,\exists</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi></mrow><annotation encoding="application/x-tex">\Gamma</annotation></semantics></math> is a <em><a class="existingWikiWord" href="/nlab/show/context">context</a></em> which declares the type of every variable occurring in <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math>.</p> </li> </ul> <p>For example, the theory of a group has one type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>, three function symbols <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">m:G\times G\to G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">i:G\to G</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">e:1\to G</annotation></semantics></math>, and axioms</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>x</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>G</mi><mo stretchy="false">|</mo><mo>⊤</mo><mo>⊢</mo><mi>m</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>m</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>x</mi><mo>:</mo><mi>G</mi><mo stretchy="false">|</mo><mo>⊤</mo><mo>⊢</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>e</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>m</mi><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>e</mi></mtd></mtr> <mtr><mtd><mi>x</mi><mo>:</mo><mi>G</mi><mo stretchy="false">|</mo><mo>⊤</mo><mo>⊢</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>e</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>m</mi><mo stretchy="false">(</mo><mi>e</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi><mo>.</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ x:G,y:G,z:G | \top \vdash m(m(x,y),z) = m(x,m(y,z))\\ x:G | \top \vdash m(x,i(x)) = e \;\wedge\; m(i(x),x) = e\\ x:G | \top \vdash m(x,e) = x \;\wedge\; m(e,x) = x. } </annotation></semantics></math></div> <p>This is an <em><a class="existingWikiWord" href="/nlab/show/equational+theory">equational theory</a></em>, meaning that each axiom is just one or more equations between terms that must hold in a given context. For a different sort of example, the theory of a poset has one type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>, one relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo><mo>:</mo><mi>P</mi><mo>×</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\le:P\times P</annotation></semantics></math>, and axioms</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>x</mi><mo>:</mo><mi>P</mi><mo stretchy="false">|</mo><mo>⊤</mo><mo>⊢</mo><mi>x</mi><mo>≤</mo><mi>x</mi></mtd></mtr> <mtr><mtd><mi>x</mi><mo>:</mo><mi>P</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>P</mi><mo stretchy="false">|</mo><mi>x</mi><mo>≤</mo><mi>y</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>y</mi><mo>≤</mo><mi>x</mi><mo>⊢</mo><mi>x</mi><mo>=</mo><mi>y</mi></mtd></mtr> <mtr><mtd><mi>x</mi><mo>:</mo><mi>P</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>P</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>P</mi><mo stretchy="false">|</mo><mi>x</mi><mo>≤</mo><mi>y</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>y</mi><mo>≤</mo><mi>z</mi><mo>⊢</mo><mi>x</mi><mo>≤</mo><mi>z</mi><mo>.</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ x:P | \top \vdash x\le x\\ x:P,y:P | x\le y \;\wedge\; y\le x \vdash x=y\\ x:P,y:P,z:P | x\le y \;\wedge\; y\le z \vdash x\le z. } </annotation></semantics></math></div> <h3 id="CategoricalSemantics">Categorical semantics</h3> <p>Now suppose that we have a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> with <a class="existingWikiWord" href="/nlab/show/finite+limit">finite limit</a>s and we want to interpret such a theory internally in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. We identify the aspects of the theory with structures in the category by what is called <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a>:</p> <p>First, for each <em>type</em> in the theory we choose an <a class="existingWikiWord" href="/nlab/show/object">object</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. Then for each <em>function symbol</em> in the theory we choose a <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. And finally, for each <em>relation</em> in the theory we choose a <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. (We always interpret the relation of <em>equality</em> on a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> by the diagonal <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↪</mo><mi>A</mi><mo>×</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">A\hookrightarrow A\times A</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>.) Thus, for example, to interpret the theory of a group in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> we must choose an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> and morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">m:G\times G\to G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">i:G\to G</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">e:1\to G</annotation></semantics></math>, while to interpret the theory of a poset, we must choose an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> and a subobject <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mo>≤</mo><mo stretchy="false">]</mo><mo>↪</mo><mi>P</mi><mo>×</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">[\le] \hookrightarrow P\times P</annotation></semantics></math>.</p> <p>Of course, this is not enough; we need to say somehow that <em>the axioms are satisfied</em>. We first define, inductively, an interpretation of every <em>term</em> that can be constructed from the theory by a morphism in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. For example, given an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> and a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">m:G\times G\to G</annotation></semantics></math>, there are two evident morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>×</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">G\times G\times G \to G</annotation></semantics></math> which are the interpretations of the two terms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m(m(x,y),z)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>m</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">m(x,m(y,z))</annotation></semantics></math>.</p> <p>We then define, inductively, an interpretation of every <em><span class="newWikiWord">logical formula<a href="/nlab/new/logical+formula">?</a></span></em> that can be constructed from the theory by a <em>subobject</em> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. The idea is that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math> is a variable of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x)</annotation></semantics></math> is a formula with <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> as its free variable, then the interpretation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x)</annotation></semantics></math> should be the “subset” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>A</mi><mo stretchy="false">|</mo><mi>φ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x\in A | \varphi(x)\}</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. The base case of this induction is that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math> is a term interpreted by a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A\to B</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">R:B</annotation></semantics></math> is a relation symbol, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(t)</annotation></semantics></math> is interpreted by the pullback of the chosen subobject <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">R\hookrightarrow B</annotation></semantics></math> representing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> along the morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">t:A\to B</annotation></semantics></math>. The building blocks of logical formulas then correspond to operations on the posets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math> of subobjects in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, as follows.</p> <table><thead><tr><th>Logical operator</th><th></th><th>Operation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">conjunction</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/intersection">intersection</a> (pullback)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/truth">truth</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/top+element">top element</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> itself)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∨</mo></mrow><annotation encoding="application/x-tex">\vee</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/union">union</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/falsity">falsity</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\bot</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bottom+element">bottom element</a> (<a class="existingWikiWord" href="/nlab/show/initial+object">strict initial object</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting implication</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo></mrow><annotation encoding="application/x-tex">\exists</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a> to <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo></mrow><annotation encoding="application/x-tex">\forall</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/right+adjoint">right adjoint</a> to <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a></td></tr> </tbody></table> <p>The fact that existential and universal quantifiers can be interpreted as left and right adjoints to pullbacks was first realized by <a class="existingWikiWord" href="/nlab/show/Bill+Lawvere">Bill Lawvere</a>. One way to realize that it makes sense is to notice that in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>, the image of a subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo>⊂</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">R\subset A</annotation></semantics></math> under a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> can be defined as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>b</mi><mo>∈</mo><mi>B</mi><mo stretchy="false">|</mo><mo stretchy="false">(</mo><mo>∃</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>a</mi><mo>∈</mo><mi>R</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>,</mo></mrow><annotation encoding="application/x-tex">\{b\in B | (\exists a\in A)(a\in R \;\wedge\; f(a)=b)\},</annotation></semantics></math></div> <p>while its “dual image” (the right adjoint to pullback) can be defined as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>b</mi><mo>∈</mo><mi>B</mi><mo stretchy="false">|</mo><mo stretchy="false">(</mo><mo>∀</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>b</mi><mo>⇒</mo><mi>a</mi><mo>∈</mo><mi>R</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">\{b\in B | (\forall a \in A)(f(a)=b \Rightarrow a\in R)\}.</annotation></semantics></math></div> <p>Of course, not in all finitely complete categories <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> do all these operations on subobjects exist. Moreover, in order for the relationship with logic to be well-behaved, any of the operations we make use of must be <em><a class="existingWikiWord" href="/nlab/show/pullback+stability">stable</a> under</em> (preserved by) pullbacks. (Pullbacks of subobjects correspond to “innocuous” logical operations such as adding extra unused variables, duplicating variables, and so on, so they should definitely not affect the meaning of the logical connectives. However, in <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a> such operations become less innocuous.)</p> <p>In any category with finite limits, the posets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math> always have finite intersections (given by pullback), including a top element (given by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> itself). Thus in any such category, we can interpret logical theories that use only the connectives <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math>. This includes both the theories of groups and posets considered above.<br />In a <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a>, the existence of pullback-stable <a class="existingWikiWord" href="/nlab/show/image">image</a>s implies that the <a class="existingWikiWord" href="/nlab/show/base+change">base change</a> functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo>:</mo><mi>Sub</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*:Sub(B)\to Sub(A)</annotation></semantics></math> along any map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A\to B</annotation></semantics></math> has a left adjoint, usually written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∃</mo> <mi>f</mi></msub></mrow><annotation encoding="application/x-tex">\exists_f</annotation></semantics></math>, and that these adjoints “commute with pullbacks” in an appropriate sense (given by the <a class="existingWikiWord" href="/nlab/show/Beck-Chevalley+condition">Beck-Chevalley condition</a>). Thus, in a regular category we can interpret any theory in so-called <em><a class="existingWikiWord" href="/nlab/show/regular+logic">regular logic</a></em>, which uses only <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo></mrow><annotation encoding="application/x-tex">\exists</annotation></semantics></math>.</p> <p>Actually, some instances of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo></mrow><annotation encoding="application/x-tex">\exists</annotation></semantics></math> can be interpreted in any category with finite limits: if <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 itself a monomorphism, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">f^*</annotation></semantics></math> always has a left adjoint, given simply by composition with <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>. On the logical side, this means that we can interpret “provably unique existence” in any category with finite limits. Logic with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math>, and “provably unique existence” is called <em>cartesian logic</em> or <em>finite-limit logic</em>.</p> <p>A <a class="existingWikiWord" href="/nlab/show/coherent+category">coherent category</a> is basically defined to be a <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a> in which the subobject posets additionally have pullback-stable finite unions. Thus, in a coherent category we can interpret so-called <em>coherent logic</em>, which adds <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∨</mo></mrow><annotation encoding="application/x-tex">\vee</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\bot</annotation></semantics></math> to <a class="existingWikiWord" href="/nlab/show/regular+logic">regular logic</a>. Likewise, in an infinitary-coherent (or “geometric”) category we can interpret <em>geometric logic</em>, which adds infinitary disjunctions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>i</mi></msub><msub><mi>φ</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">\bigvee_i \varphi_i</annotation></semantics></math> to coherent logic. Geometric logic is especially important because it is preserved by the inverse image parts of <a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a>s, and because any geometric theory has a <a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a>.</p> <p>On the other hand, in a <a class="existingWikiWord" href="/nlab/show/extensive+category">lextensive category</a>, we do not have images or all unions, but if we have two subobjects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> which are <em>disjoint</em> (their intersection is initial), then their coproduct is also their union in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math>. Therefore, in a lextensive category we can interpret <em>disjunctive logic</em>, which is cartesian logic plus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\bot</annotation></semantics></math> and “provably disjoint disjunction.” Likewise, in an infinitary-lextensive category we can interpret “infinitary-disjunctive logic.”</p> <p>Finally, in a <a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting category</a> the base change functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo>:</mo><mi>Sub</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*:Sub(B)\to Sub(A)</annotation></semantics></math> also have right adjoints, usually written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∀</mo> <mi>f</mi></msub></mrow><annotation encoding="application/x-tex">\forall_f</annotation></semantics></math>, and it is easy to see that this implies that each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math> is also a <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, hence has an “implication” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math> as well. (We define “negation” by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>φ</mi><mo>≡</mo><mi>φ</mi><mo>⇒</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\neg \varphi \equiv \varphi \Rightarrow \bot</annotation></semantics></math>.) Thus, in a Heyting category we can interpret all of (finitary, first-order) <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>.</p> <p>Now that we know how to interpret logic, we can say that a <strong>model</strong> of a given theory in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> consists of a choice of objects, morphisms, and subobjects for the types, function symbols, and relation symbols as above, such that for each axiom <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo stretchy="false">|</mo><mi>φ</mi><mo>⊢</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\Gamma | \varphi \vdash \psi</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>φ</mi><mo stretchy="false">]</mo><mo>≤</mo><mo stretchy="false">[</mo><mi>ψ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\varphi]\le [\psi]</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mo stretchy="false">[</mo><mi>Γ</mi><mo stretchy="false">]</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub([\Gamma])</annotation></semantics></math>. Here, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Γ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\Gamma]</annotation></semantics></math> is the product of the objects that correspond to the types of the variables in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi></mrow><annotation encoding="application/x-tex">\Gamma</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>φ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\varphi]</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>ψ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\psi]</annotation></semantics></math> are the interpretations of the formulas <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math> as subobjects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Γ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\Gamma]</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> is the relation of subobject inclusion.</p> <p>It is easy to verify that a model of the theory of a group in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is precisely an internal <a class="existingWikiWord" href="/nlab/show/group">group</a> object in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, as usually defined. For instance, the validity of the axiom</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>G</mi><mo stretchy="false">|</mo><mo>⊤</mo><mo>⊢</mo><mi>m</mi><mo stretchy="false">(</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>m</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:G,y:G,z:G | \top \vdash m(m(x,y),z) = m(x,m(y,z))</annotation></semantics></math></div> <p>means that the <a class="existingWikiWord" href="/nlab/show/equalizer">equalizer</a> of the two morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>×</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">G\times G\times G \to G</annotation></semantics></math> must be all of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>×</mo><mi>G</mi><mo>×</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">G\times G\times G</annotation></semantics></math>, or equivalently that those two morphisms must be equal. The same happens in most other cases.</p> <h3 id="the_internal_logic_as_a_functor">The internal logic as a functor</h3> <p>As described above, a model of a given theory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> in a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> consists of an assignment</p> <table><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td style="text-align: left;">types of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math></td><td style="text-align: left;">objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">function symbols of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math></td><td style="text-align: left;">morphisms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">relation symbols of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math></td><td style="text-align: left;">subobjects in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math></td><td style="text-align: left;">containments in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math></td></tr> </tbody></table> <p>This is a sort of <a class="existingWikiWord" href="/nlab/show/heteromorphism">heteromorphism</a> in that it changes the name of things as it operates on them. We can describe it more simply as a “translation of theories” as follows.</p> <p>Given a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> (which may be regular, coherent, geometric, Heyting, etc.), we define its <strong>internal type theory (with first-order logic)</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Lang(C)</annotation></semantics></math> to be the theory whose</p> <ul> <li>types are the objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>;</li> <li>function symbols are the morphisms on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>;</li> <li>relation symbols are the subobjects in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>;</li> <li>axioms are the containments in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>.</li> </ul> <p>Now a model of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> can be described simply as a morphism of theories (a “translation” or “interpretation”)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>→</mo><mi>Lang</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">T \to Lang(C).</annotation></semantics></math></div> <p>The functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi><mo>:</mo><mi>Categories</mi><mo>→</mo><mi>Theories</mi></mrow><annotation encoding="application/x-tex">Lang : Categories \to Theories</annotation></semantics></math> has a left adjoint, the <a class="existingWikiWord" href="/nlab/show/syntactic+category">syntactic category</a> of a theory. Thus we have a chain of natural isomorphisms</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Theories</mi><mo stretchy="false">(</mo><mi>T</mi><mo>,</mo><mi>Lang</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≅</mo><mi>Models</mi><mo stretchy="false">(</mo><mi>T</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>≅</mo><mi>Categories</mi><mo stretchy="false">(</mo><mi>Syn</mi><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">)</mo><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> Theories(T,Lang(C)) \cong Models(T,C) \cong Categories(Syn(T),C)). </annotation></semantics></math></div> <h2 id="soundness_and_internal_reasoning">Soundness and internal reasoning</h2> <p>Internal logic is not just a way to concisely describe internal structures in a category, but also gives us a way to <em>prove</em> things about them by “internal reasoning.” We simply need to verify that the “usual” methods of logical reasoning (for example, from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>⊢</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi\vdash \psi</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo>⊢</mo><mi>χ</mi></mrow><annotation encoding="application/x-tex">\psi\vdash \chi</annotation></semantics></math> deduce <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>⊢</mo><mi>χ</mi></mrow><annotation encoding="application/x-tex">\varphi\vdash\chi</annotation></semantics></math>) are <em>internally valid</em>, in the sense that if the premises are satisfied in some model <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> (in the example, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>φ</mi><mo stretchy="false">]</mo><mo>≤</mo><mo stretchy="false">[</mo><mi>ψ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\varphi]\le [\psi]</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>ψ</mi><mo stretchy="false">]</mo><mo>≤</mo><mo stretchy="false">[</mo><mi>χ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\psi]\le [\chi]</annotation></semantics></math>) then so is the conclusion (in the example, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>φ</mi><mo stretchy="false">]</mo><mo>≤</mo><mo stretchy="false">[</mo><mi>χ</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\varphi]\le [\chi]</annotation></semantics></math>). This is called the <em>Soundness Theorem</em>.</p> <p>It then follows that if we start from the axioms of a theory and “reason normally” within type theory, which in practice amounts to pretending that the types are sets, the function symbols are functions, and the relation symbols are subsets, then anything we prove will still be true when the theory is interpreted in an <em>arbitrary</em> category, not just <a class="existingWikiWord" href="/nlab/show/Set">Set</a>. For example, by easy equational reasoning from the theory of a group, we can prove that inverses are unique, which is expressed by the logical sequent</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>G</mi><mo>,</mo><mi>z</mi><mo>:</mo><mi>G</mi><mo stretchy="false">|</mo><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>e</mi><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>m</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><mi>e</mi><mo>⊢</mo><mi>y</mi><mo>=</mo><mi>z</mi><mo>.</mo></mrow><annotation encoding="application/x-tex">x:G,y:G,z:G | m(x,y)=e \;\wedge\; m(x,z)=e \vdash y=z.</annotation></semantics></math></div> <p>It follows that this is also true, suitably interpreted, as a statement about internal group objects in <em>any</em> category.</p> <p>There are (at least) three caveats. Firstly, we must take care to use only the rules appropriate to the fragment of logic that is valid in the particular categories we are interested in. For example, if we want our conclusions to be valid in any <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a>, we must restrict ourselves to reasoning “within regular logic.” Most mathematicians are not familiar with making such distinctions in their reasoning, but in practice most things one would want to say about a regular theory turn out to be provable in regular logic. (We will not spell out the details of what this means.) And once we are in a Heyting category, and in particular in a topos, this problem goes away and we can use full first-order logic.</p> <p>The second, more important, caveat is that the internal logic of all these categories is, in general, <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a>. This means that, among other things, the interpretation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>¬</mo><mi>φ</mi></mrow><annotation encoding="application/x-tex">\neg\neg\varphi</annotation></semantics></math> is, in general, distinct from that of <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>, and that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>∨</mo><mo>¬</mo><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi\vee \neg\varphi</annotation></semantics></math> is not always valid. So even if we believe that <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a> (including the principle of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> and even the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>) is “true,” as many mathematicians do, there is still a reason to look for proofs that are constructively acceptable, since it is only these which are valid in the internal logic of most categories. If the category is <a class="existingWikiWord" href="/nlab/show/Boolean+category">Boolean</a> and/or satisfies the internal <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, however, then this problem goes away, but these fail in many categories in which one wants to internalize (such as many <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a>es).</p> <p>The third caveat is that one must take care to distinguish the <em>internal</em> logic of a category from what is <em>externally</em> true about it. In general, internal validity is “local” truth, meaning things which become true “after passing to a <a class="existingWikiWord" href="/nlab/show/cover">cover</a>.” This is particularly important for formulas involving <em>disjunction</em> and <em>existence</em>. For example, an object’s being <a class="existingWikiWord" href="/nlab/show/projective+object">projective</a> in the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a different statement from its being <em>internally</em> projective, meaning that “<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 projective” is true in the internal logic. Another good example can be found in the different notions of <a class="existingWikiWord" href="/nlab/show/finite+object">finite object</a> in a topos. This problem goes away if the ambient category is <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed</a>, but well-pointed categories are even rarer than Boolean ones satisfying choice; the only well-pointed Grothendieck topos is <a class="existingWikiWord" href="/nlab/show/Set">Set</a> itself.</p> <h2 id="syntactic_categories">Completeness, syntactic categories, and Morita equivalence</h2> <p>The converse of the Soundness Theorem is called the <em>Completeness Theorem</em>, and states that if a sequent <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>⊢</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi\vdash\psi</annotation></semantics></math> is valid in every model of a theory, then it is <em>provable</em> from that theory. This is noticeably less trivial. In classical first-order logic, where the only models considered are set-valued ones, the completeness theorem is usually proven using <a class="existingWikiWord" href="/nlab/show/ultraproduct">ultraproduct</a>s. However, in categorical logic there is a more elegant approach (which additionally no longer depends on any form of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>).</p> <p>The <strong><a class="existingWikiWord" href="/nlab/show/syntactic+category">syntactic category</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub><mo>=</mo><mi>Syn</mi><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C_T = Syn(T)</annotation></semantics></math> of a theory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> was mentioned above, as the left adjoint to the “internal logic functor” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi></mrow><annotation encoding="application/x-tex">Lang</annotation></semantics></math>. By the <a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a>, the syntactic category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> contains a “generic” model of the theory. Moreover, by the construction of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> (see <a class="existingWikiWord" href="/nlab/show/syntactic+category">syntactic category</a>), the valid sequents in this model are <em>precisely</em> those provable from the theory. Therefore, if a sequent is valid in all models, it is in particular valid in the generic model in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>, and hence provable from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>.</p> <p>The universal property of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> is also sometimes useful for semantic conclusions. For instance, sometimes one can prove something about the generic model and then carry it over to all models.</p> <p>Furthermore, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> lives in a sub-fragment of geometric logic (such as regular, coherent, lextensive, or geometric logic), then the <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a> of <a class="existingWikiWord" href="/nlab/show/sheaf">sheaves</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> for its appropriate (regular, coherent, extensive, or geometric) <a class="existingWikiWord" href="/nlab/show/coverage">coverage</a> contains a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>-model which is generic for models in Grothendieck toposes: any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>-model in a Grothendieck topos is its image under the inverse image of a unique <a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a>. This topos is called the <strong><a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a></strong> of the theory.</p> <p>The <a class="existingWikiWord" href="/nlab/show/syntactic+category">syntactic category</a> of a theory can be considered as the “extensional essence” of that theory, since functors out of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> completely determine the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>-models in any category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> with suitable structure. It therefore makes sense, in some contexts, to define a <em>morphism</em> of theories to be a functor between their <a class="existingWikiWord" href="/nlab/show/syntactic+categories">syntactic categories</a>, and an <em>equivalence</em> of theories (sometimes called a <em>Morita equivalence</em>) to be an equivalence between their syntactic categories.</p> <p>A morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>→</mo><mi>T</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">T\to T'</annotation></semantics></math> between theories, in this sense, induces a functor from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">T'</annotation></semantics></math>-models in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>-models in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>, for any category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> with suitable structure, in a way which is natural in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>. In particular, theories which are “Morita equivalent” in this sense have naturally equivalent categories of models in all categories <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> with suitable structure; so they have the same “meaning” even though they may be presented quite differently. (Note that this is a much stronger sort of equivalence than merely having equivalent categories of models in some particular category, such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.) Moreover, the fact that the syntactic category is defined “syntactically” means that a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>→</mo><mi>T</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">T\to T'</annotation></semantics></math> actually induces a “translation” of the types, functions, and relations of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> into those of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">T'</annotation></semantics></math>.</p> <p>By first applying various “completion” processes to syntactic categories before asking about equivalence, we obtain coarser notions of equivalence, which only induce equivalences of models in more restricted sorts of categories. For instance, if we compare the <a class="existingWikiWord" href="/nlab/show/exact+completion">exact completion</a>s of syntactic categories of regular theories, we obtain a notion of equivalence that induces equivalences of categories of models in all exact categories (not necessarily all regular ones). Likewise for coherent theories and <a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a>es, and for geometric theories and infinitary pretoposes. Note, though, that the infinitary-pretopos completion of a (small) geometric theory is in fact already a (Grothendieck) topos, and coincides with the classifying topos considered above. Thus, passage to classifying toposes is also an instance of this construction, and an equivalence of classifying toposes means that two theories have equivalent categories of models in all toposes. (This is still much stronger than just having equivalent categories of models in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.)</p> <h2 id="kripkejoyal_semantics">Kripke–Joyal semantics</h2> <p>To be written, but see <a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a>.</p> <h2 id="dependent_type_theory">Dependent type theory</h2> <p>We now consider the internal language of a <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed category</a> as a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>.</p> <div class="standout"> <p>Material to be moved here from <a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a>.</p> </div> <h2 id="higherorder_logic">Higher-order logic</h2> <p>To be written, but see <a class="existingWikiWord" href="/nlab/show/Mitchell%E2%80%93B%C3%A9nabou+language">Mitchell–Bénabou language</a> for the version in a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>.</p> <h2 id="examples">Examples</h2> <h3 id="LogicOfSet">Internal logic in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math></h3> <p>The <a class="existingWikiWord" href="/nlab/show/topos">topos</a> <a class="existingWikiWord" href="/nlab/show/Set">Set</a> in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a> of course has as its internal logic the “ordinary” logic. This is reproduced by following the abstract nonsense as follows:</p> <p>the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> of <a class="existingWikiWord" href="/nlab/show/Set">Set</a> is <a class="existingWikiWord" href="/nlab/show/generalized+the">the</a> one-element set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">{*}</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a> in <a class="existingWikiWord" href="/nlab/show/Set">Set</a> is the two-element set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi><mo>=</mo><mo stretchy="false">{</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\Omega = \{true, false\}</annotation></semantics></math> equipped with the map</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>:</mo><mo>*</mo><mo>→</mo><mi>Ω</mi></mrow><annotation encoding="application/x-tex"> T : {*} \to \Omega </annotation></semantics></math></div> <p>that picks the element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>true</mi></mrow><annotation encoding="application/x-tex">true</annotation></semantics></math> in <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>. The <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a> of <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a>s of the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> is the <a class="existingWikiWord" href="/nlab/show/poset">poset</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>=</mo><mo stretchy="false">{</mo><mi>∅</mi><mo>↪</mo><mo>*</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex"> L = \{ \emptyset \hookrightarrow {*} \} </annotation></semantics></math></div> <p>consisting only of the two trivial subobjects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">*</annotation></semantics></math>, the point itself and the empty set, and the unique inclusion morphism between them. These are classified, respectively, by the <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a>s <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo><mover><mo>→</mo><mi>true</mi></mover><mi>Ω</mi></mrow><annotation encoding="application/x-tex">{*} \stackrel{true}{\to} \Omega</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo><mover><mo>→</mo><mi>false</mi></mover><mi>Ω</mi></mrow><annotation encoding="application/x-tex">{*} \stackrel{false}{\to} \Omega</annotation></semantics></math>, so that we can also write our <a class="existingWikiWord" href="/nlab/show/poset">poset</a> of <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a>s of the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>=</mo><mo stretchy="false">{</mo><mi>false</mi><mo>→</mo><mi>true</mi><mo stretchy="false">}</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> L = \{ false \to true \} \,. </annotation></semantics></math></div> <p>The logical operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo><mo>=</mo><mi>AND</mi></mrow><annotation encoding="application/x-tex">\wedge = AND</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/product">product</a> in the <a class="existingWikiWord" href="/nlab/show/poset">poset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math>. Indeed we find pullback diagrams in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>true</mi><mo>×</mo><mo lspace="0em" rspace="thinmathspace">true</mo><mo>=</mo><mi>true</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>true</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>true</mi></mtd></mtr></mtable></mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mrow><mtable><mtr><mtd><mi>true</mi><mo>×</mo><mi>false</mi><mo>=</mo><mi>false</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>false</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>true</mi></mtd></mtr></mtable></mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mrow><mtable><mtr><mtd><mi>false</mi><mo>×</mo><mi>false</mi><mo>=</mo><mi>false</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>false</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>false</mi></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ true \times \true = true &\to& true \\ \downarrow \\ true } \;\;\; \;\;\; \;\;\; \array{ true \times false = false &\to& false \\ \downarrow \\ true } \;\;\; \;\;\; \;\;\; \array{ false \times false = false &\to& false \\ \downarrow \\ false } \,. </annotation></semantics></math></div> <p>The logical operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∨</mo><mo>=</mo><mi>OR</mi></mrow><annotation encoding="application/x-tex">\vee = OR</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> in the <a class="existingWikiWord" href="/nlab/show/poset">poset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math>. Indeed we find <a class="existingWikiWord" href="/nlab/show/pushout">pushout</a> diagrams in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><mi>true</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>true</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>true</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mo lspace="0em" rspace="thinmathspace">true</mo><mo>=</mo><mi>true</mi></mtd></mtr></mtable></mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><mi>false</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>true</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>true</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mi>false</mi><mo>=</mo><mi>true</mi></mtd></mtr></mtable></mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><mi>false</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>false</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>false</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mi>false</mi><mo>=</mo><mi>false</mi></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ && true \\ && \downarrow \\ true &\to& true \coprod \true = true } \;\;\;\; \;\;\; \;\;\; \array{ && false \\ && \downarrow \\ true &\to& true \coprod false = true } \;\;\;\; \;\;\; \;\;\; \array{ && false \\ && \downarrow \\ false &\to& false \coprod false = false } \,. </annotation></semantics></math></div> <p>The logical operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>=</mo><mi>NOT</mi></mrow><annotation encoding="application/x-tex">\not = NOT</annotation></semantics></math> is given by the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into the <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>=</mo><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>:</mo><msup><mi>L</mi> <mi>op</mi></msup><mo>→</mo><mi>L</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \not = hom(-, false) : L^{op} \to L \,. </annotation></semantics></math></div> <p>We find the value of the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> by its defining <a class="existingWikiWord" href="/nlab/show/adjunction">adjunction</a>. For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">hom(true,false)</annotation></semantics></math> we have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>true</mi><mo>×</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mi>∅</mi></mrow><annotation encoding="application/x-tex"> Hom_L(true, hom(true,false)) \simeq Hom_L(true \times true, false) = Hom_L(true, false) = \emptyset </annotation></semantics></math></div> <p>and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>×</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mo>*</mo></mrow><annotation encoding="application/x-tex"> Hom_L(false, hom(true,false)) \simeq Hom_L(false \times true, false) = Hom_L(false, false) = {*} </annotation></semantics></math></div> <p>from which we deduce that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mi>false</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> hom(true,false) = false\,. </annotation></semantics></math></div> <p>Similarly for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">hom(false,false)</annotation></semantics></math> we have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>true</mi><mo>,</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>true</mi><mo>×</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mo>*</mo></mrow><annotation encoding="application/x-tex"> Hom_L(true, hom(false,false)) \simeq Hom_L(true \times false, false) = Hom_L(false, false) = {*} </annotation></semantics></math></div> <p>and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>×</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>Hom</mi> <mi>L</mi></msub><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mo>*</mo></mrow><annotation encoding="application/x-tex"> Hom_L(false, hom(false,false)) \simeq Hom_L(false \times false, false) = Hom_L(false, false) = {*} </annotation></semantics></math></div> <p>from which we deduce that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>false</mi><mo>,</mo><mi>false</mi><mo stretchy="false">)</mo><mo>=</mo><mi>true</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> hom(false,false) = true \,. </annotation></semantics></math></div> <p>This way all the familiar logical operations are recovered from the internal logic of the <a class="existingWikiWord" href="/nlab/show/topos">topos</a> <a class="existingWikiWord" href="/nlab/show/Set">Set</a>.</p> <h3 id="LogicOfPresheaves">Internal logic in a sheaf topos on open subsets</h3> <p>Let <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> be a <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Op(X)</annotation></semantics></math> its <a class="existingWikiWord" href="/nlab/show/category+of+open+subsets">category of open subsets</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>:</mo><mo>=</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(X) := Sh(Op(X))</annotation></semantics></math> the <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a> of <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">sheaves</a> on <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>.</p> <p>We discuss the internal logic of this sheaf topos (originally <a href="#Tarski">Tarski, 1938</a>).</p> <p>The <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> is the sheaf <a class="existingWikiWord" href="/nlab/show/representable+functor">represented by</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>: the one that is constant on the one-element set</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>:</mo><mi>U</mi><mo>↦</mo><mo>*</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> X : U \mapsto {*} \,. </annotation></semantics></math></div> <p>The <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a>s of this object are the <a class="existingWikiWord" href="/nlab/show/representable+functor">representable presheaves</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>V</mi><mo stretchy="false">)</mo><mo>:</mo><mi>U</mi><mo>↦</mo><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mo>*</mo></mtd> <mtd><mo stretchy="false">|</mo><mi>if</mi><mi>U</mi><mo>⊂</mo><mi>V</mi></mtd></mtr> <mtr><mtd><mi>∅</mi></mtd> <mtd><mi>otherwise</mi></mtd></mtr></mtable></mrow></mrow></mrow><annotation encoding="application/x-tex"> hom(-,V) : U \mapsto \left\{ \array{ {*} & | if U \subset V \\ \emptyset & otherwise } \right. </annotation></semantics></math></div> <p>for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi><mo>∈</mo><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">V \in Op(X)</annotation></semantics></math>.</p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>In the <em><a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a></em> topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSh</mi><mo stretchy="false">(</mo><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>Func</mi><mo stretchy="false">(</mo><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><msup><mo stretchy="false">)</mo> <mi>op</mi></msup><mo>,</mo><mi>Set</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">PSh(Op(X))= Func(Op(X)^{op},Set)</annotation></semantics></math>, the subobjects of <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> are arbitrary <a class="existingWikiWord" href="/nlab/show/sieves">sieves</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Op(X)</annotation></semantics></math>, not just representables. For instance, for any two open sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> there is a sieve consisting of all open sets contained in either <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>, which doesn’t necessarily contain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>∪</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">U\cup V</annotation></semantics></math>. It’s only in the <em>sheaf</em> topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(X)</annotation></semantics></math> that the representables are precisely the subobjects of <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>.</p> </div> <p>The <a class="existingWikiWord" href="/nlab/show/poset">poset</a> of <a class="existingWikiWord" href="/nlab/show/subobject">subobject</a>s formed by these is just the <a class="existingWikiWord" href="/nlab/show/category+of+open+subsets">category of open subsets</a> itself:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo>=</mo><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> L = Op(X) \,. </annotation></semantics></math></div> <ul> <li> <p>The logical operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>AND</mi></mrow><annotation encoding="application/x-tex">AND</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/product">product</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Op(X)</annotation></semantics></math>: this is the <strong>intersection</strong> of open subsets.</p> </li> <li> <p>The logical operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>OR</mi></mrow><annotation encoding="application/x-tex">OR</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Op(X)</annotation></semantics></math>: this is the <strong>union</strong> of open subsets.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Op</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Op(X)</annotation></semantics></math> is given by</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>U</mi><mo>,</mo><mi>V</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><msup><mi>U</mi> <mi>c</mi></msup><mo>∨</mo><mi>V</mi><msup><mo stretchy="false">)</mo> <mo>∘</mo></msup></mrow><annotation encoding="application/x-tex"> hom(U,V) = (U^c \vee V)^\circ </annotation></semantics></math></div> <p>(the interior of the union of the complement of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> with V).</p> <p>So <strong>negation</strong> is given by sending an open subset to the interior of its complement:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>U</mi><mo>=</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>U</mi><mo>,</mo><mi>∅</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><msup><mi>U</mi> <mi>c</mi></msup><mo>∨</mo><mi>∅</mi><msup><mo stretchy="false">)</mo> <mo>∘</mo></msup><mo>=</mo><mo stretchy="false">(</mo><msup><mi>U</mi> <mi>c</mi></msup><msup><mo stretchy="false">)</mo> <mo>∘</mo></msup><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \not U = hom(U,\emptyset) = (U^c \vee \emptyset)^\circ = (U^c)^\circ \,. </annotation></semantics></math></div></li> </ul> <p>In particular we find that in the internal logic of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">PSh(X)</annotation></semantics></math> the law of the <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a> fails in general, as in general we do not have that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo>¬</mo><mi>U</mi><mo stretchy="false">)</mo><mo>∨</mo><mi>U</mi><mo>=</mo><mi>true</mi></mrow><annotation encoding="application/x-tex"> (\not U) \vee U = true </annotation></semantics></math></div> <p>because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>U</mi><mo>∨</mo><mi>U</mi><mo>=</mo><mo stretchy="false">(</mo><msup><mi>U</mi> <mi>c</mi></msup><msup><mo stretchy="false">)</mo> <mo>∘</mo></msup><mo>∪</mo><mi>U</mi><mo>=</mo><mi>X</mi><mo>\</mo><mo>∂</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">\not U \vee U = (U^c)^\circ \cup U = X \backslash \partial U</annotation></semantics></math> is the total 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> without the boundary (frontier) of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>, and not <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>true</mi><mo>=</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">true = X</annotation></semantics></math>, all of the total space.</p> <p>Thus, the internal logic of this <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">sheaf topos</a> is (in general) <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>. As remarked above, this is the case in many toposes.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic of set theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+category+theory+and+type+theory">relation between category theory and type theory</a></p> </li> </ul> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>Most books on topos theory develop some internal logic, at least in the context of a topos. For example:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Saunders+Mac+Lane">Saunders Mac Lane</a><a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a>, <em><a class="existingWikiWord" href="/nlab/show/Sheaves+in+Geometry+and+Logic">Sheaves in Geometry and Logic</a></em></p> </li> <li> <p>Goldblatt, <em>Topoi: the categorial analysis of logic</em></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Francis+Borceux">Francis Borceux</a>, Section 6 of: <em><a class="existingWikiWord" href="/nlab/show/Handbook+of+Categorical+Algebra">Handbook of Categorical Algebra</a></em>, Vol 3: <em>Categories of Sheaves</em>, Encyclopedia of Mathematics and its Applications <strong>50</strong></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, Part D of: <em><a class="existingWikiWord" href="/nlab/show/Sketches+of+an+Elephant">Sketches of an Elephant</a></em></p> </li> </ul> <p>is comprehensive.</p> <p>Phoa has a presentation of the internal logic of a topos over a dependent type theory, as opposed to other systems which use simple type theory. This is system is not minimal, but close to what is used in practice <a href="http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz">PS</a>.</p> <p>The book</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Bart+Jacobs">Bart Jacobs</a>, <em>Categorical Logic and Type Theory</em></li> </ul> <p>works in the even more general context of <a class="existingWikiWord" href="/nlab/show/Grothendieck+fibration">fibrations</a>, allowing us to associate to each object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> an arbitrary poset instead of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(A)</annotation></semantics></math>.</p> <p>The book</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Paul+Taylor">Paul Taylor</a>, <em><a class="existingWikiWord" href="/nlab/show/Practical+Foundations+of+Mathematics">Practical Foundations of Mathematics</a></em></li> </ul> <p>is arguably all about this subject (although you wouldn't know it until about Chapter VIII), but from a different perspective. In particular, Taylor allows us to replace having <em>all</em> pullbacks with pullbacks along a pullback-stable class of <a class="existingWikiWord" href="/nlab/show/display+morphisms">display morphisms</a>.</p> <p>A discussion of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> as the <a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a> of <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+categories">locally cartesian closed categories</a> is in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/R.+A.+G.+Seely">R. A. G. Seely</a>, <em>Locally cartesian closed categories and type theory</em>, Math. Proc. Camb. Phil. Soc. (1984) 95 (<a href="http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf">pdf</a>)</li> </ul> <p>The observation that the poset of open subsets of a topological space serve as a model for <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a> is apparently originally due to</p> <ul> <li id="Tarski"><a class="existingWikiWord" href="/nlab/show/Alfred+Tarski">Alfred Tarski</a>, <em>Der Aussagenkalkül und die Topologie</em>, Fundamenta Mathemeticae 31 (1938), pp. 103–134.</li> </ul> <h3 id="Applications">Applications</h3> <p>Discussion of fundamental constructions of <a class="existingWikiWord" href="/nlab/show/algebraic+geometry">algebraic geometry</a> from the perspective of the internal logic of the <a class="existingWikiWord" href="/nlab/show/sheaf+topos">sheaf topos</a> over a <a class="existingWikiWord" href="/nlab/show/scheme">scheme</a> (<a class="existingWikiWord" href="/nlab/show/Zariski+topos">Zariski topos</a>, <a class="existingWikiWord" href="/nlab/show/etale+topos">etale topos</a>) is in</p> <ul> <li id="Blechschmidt15"> <p><a class="existingWikiWord" href="/nlab/show/Ingo+Blechschmidt">Ingo Blechschmidt</a>, <em>Using the internal language of toposes in algebraic geometry</em>, talk at <a href="https://indico.math.cnrs.fr/event/747/">Toposes at IHES</a>, November 2015 (<a href="https://github.com/iblech/internal-methods/blob/master/slides-ihes2015.pdf">pdf</a>, <a href="https://www.youtube.com/watch?v=7S8--bIKaWQ">recording</a>)</p> </li> <li id="Blechschmidt16"> <p><a class="existingWikiWord" href="/nlab/show/Ingo+Blechschmidt">Ingo Blechschmidt</a>, <em>Using the internal language of toposes in algebraic geometry</em>, thesis (<a href="http://rawgit.com/iblech/internal-methods/master/notes.pdf">pdf</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Ingo+Blechschmidt">Ingo Blechschmidt</a>, <em>Internal methods</em> <a href="https://github.com/iblech/internal-methods">github repository</a></p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on January 27, 2024 at 14:37:26. See the <a href="/nlab/history/internal+logic" 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/internal+logic" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/500/#Item_30">Discuss</a><span class="backintime"><a href="/nlab/revision/internal+logic/81" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/internal+logic" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/internal+logic" accesskey="S" class="navlink" id="history" rel="nofollow">History (81 revisions)</a> <a href="/nlab/show/internal+logic/cite" style="color: black">Cite</a> <a href="/nlab/print/internal+logic" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/internal+logic" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>