CINXE.COM
linear logic in nLab
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> linear 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[/*><!--*/ .toc ul {margin: 0; padding: 0;} .toc ul ul {margin: 0; padding: 0 0 0 10px;} .toc li > p {margin: 0} .toc ul li {list-style-type: none; position: relative;} .toc div {border-top:1px dotted #ccc;} .rightHandSide h2 {font-size: 1.5em;color:#008B26} table.plaintable { border-collapse:collapse; margin-left:30px; border:0; } .plaintable td {border:1px solid #000; padding: 3px;} .plaintable th {padding: 3px;} .plaintable caption { font-weight: bold; font-size:1.1em; text-align:center; margin-left:30px; } /* Query boxes for questioning and answering mechanism */ div.query{ background: #f6fff3; border: solid #ce9; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; max-height: 20em; overflow: auto; } /* Standout boxes for putting important text */ div.standout{ background: #fff1f1; border: solid black; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; overflow: auto; } /* Icon for links to n-category arXiv documents (commented out for now i.e. disabled) a[href*="http://arxiv.org/"] { background-image: url(../files/arXiv_icon.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 22px; } */ /* Icon for links to n-category cafe posts (disabled) a[href*="http://golem.ph.utexas.edu/category"] { background-image: url(../files/n-cafe_5.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pdf files (disabled) a[href$=".pdf"] { background-image: url(../files/pdficon_small.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pages, etc. -inside- pdf files (disabled) a[href*=".pdf#"] { background-image: url(../files/pdf_entry.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ a.existingWikiWord { color: #226622; } a.existingWikiWord:visited { color: #226622; } a.existingWikiWord[title] { border: 0px; color: #aa0505; text-decoration: none; } a.existingWikiWord[title]:visited { border: 0px; color: #551111; text-decoration: none; } a[href^="http://"] { border: 0px; color: #003399; } a[href^="http://"]:visited { border: 0px; color: #330066; } a[href^="https://"] { border: 0px; color: #003399; } a[href^="https://"]:visited { border: 0px; color: #330066; } div.dropDown .hide { display: none; } div.dropDown:hover .hide { display:block; } div.clickDown .hide { display: none; } div.clickDown:focus { outline:none; } div.clickDown:focus .hide, div.clickDown:hover .hide { display: block; } div.clickDown .clickToReveal, div.clickDown:focus .clickToHide { display:block; } div.clickDown:focus .clickToReveal, div.clickDown .clickToHide { display:none; } div.clickDown .clickToReveal:after { content: "A(Hover to reveal, click to "hold")"; font-size: 60%; } div.clickDown .clickToHide:after { content: "A(Click to hide)"; font-size: 60%; } div.clickDown .clickToHide, div.clickDown .clickToReveal { white-space: pre-wrap; } .un_theorem, .num_theorem, .un_lemma, .num_lemma, .un_prop, .num_prop, .un_cor, .num_cor, .un_defn, .num_defn, .un_example, .num_example, .un_note, .num_note, .un_remark, .num_remark { margin-left: 1em; } span.theorem_label { margin-left: -1em; } .proof span.theorem_label { margin-left: 0em; } :target { background-color: #BBBBBB; border-radius: 5pt; } /*]]>*/--></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <!--//--><![CDATA[//><!-- MathJax.Ajax.config.path["Contrib"] = "/MathJax"; MathJax.Hub.Config({ MathML: { useMathMLspacing: true }, "HTML-CSS": { scale: 90, extensions: ["handle-floats.js"] } }); MathJax.Hub.Queue( function () { var fos = document.getElementsByTagName('foreignObject'); for (var i = 0; i < fos.length; i++) { MathJax.Hub.Typeset(fos[i]); } }); //--><!]]> </script> <script type="text/javascript"> <!--//--><![CDATA[//><!-- window.addEventListener("DOMContentLoaded", function () { var div = document.createElement('div'); var math = document.createElementNS('http://www.w3.org/1998/Math/MathML', 'math'); document.body.appendChild(div); div.appendChild(math); // Test for MathML support comparable to WebKit version https://trac.webkit.org/changeset/203640 or higher. div.setAttribute('style', 'font-style: italic'); var mathml_unsupported = !(window.getComputedStyle(div.firstChild).getPropertyValue('font-style') === 'normal'); div.parentNode.removeChild(div); if (mathml_unsupported) { // MathML does not seem to be supported... var s = document.createElement('script'); s.src = "https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=MML_HTMLorMML-full"; document.querySelector('head').appendChild(s); } else { document.head.insertAdjacentHTML("beforeend", '<style>svg[viewBox] {max-width: 100%}</style>'); } }); //--><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> linear 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/7830/#Item_43" 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="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+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> <h4 id="monoidal_categories">Monoidal categories</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/monoidal+categories">monoidal categories</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+monoidal+category">enriched monoidal category</a>, <a class="existingWikiWord" href="/nlab/show/tensor+category">tensor category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a>, <a class="existingWikiWord" href="/nlab/show/tensor+network">tensor network</a></p> </li> </ul> <p><strong>With braiding</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/braided+monoidal+category">braided monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/balanced+monoidal+category">balanced monoidal category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/twist">twist</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric monoidal category</a></p> </li> </ul> <p><strong>With duals for objects</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+with+duals">category with duals</a> (list of them)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dualizable+object">dualizable object</a> (what they have)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/rigid+monoidal+category">rigid monoidal category</a>, a.k.a. <a class="existingWikiWord" href="/nlab/show/autonomous+category">autonomous category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pivotal+category">pivotal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spherical+category">spherical category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ribbon+category">ribbon category</a>, a.k.a. <a class="existingWikiWord" href="/nlab/show/tortile+category">tortile category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+closed+category">compact closed category</a></p> </li> </ul> <p><strong>With duals for morphisms</strong></p> <ul> <li> <p><span class="newWikiWord">monoidal dagger-category<a href="/nlab/new/monoidal+dagger-category">?</a></span></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+dagger-category">symmetric monoidal dagger-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dagger+compact+category">dagger compact category</a></p> </li> </ul> <p><strong>With traces</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/trace">trace</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/traced+monoidal+category">traced monoidal category</a></p> </li> </ul> <p><strong>Closed structure</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+category">closed category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/star-autonomous+category">star-autonomous category</a></p> </li> </ul> <p><strong>Special sorts of products</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/semicartesian+monoidal+category">semicartesian monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+category+with+diagonals">monoidal category with diagonals</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/multicategory">multicategory</a></p> </li> </ul> <p><strong>Semisimplicity</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/semisimple+category">semisimple category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fusion+category">fusion category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/modular+tensor+category">modular tensor category</a></p> </li> </ul> <p><strong>Morphisms</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+functor">monoidal functor</a></p> <p>(<a class="existingWikiWord" href="/nlab/show/lax+monoidal+functor">lax</a>, <a class="existingWikiWord" href="/nlab/show/oplax+monoidal+functor">oplax</a>, <a class="existingWikiWord" href="/nlab/show/strong+monoidal+functor">strong</a> <a class="existingWikiWord" href="/nlab/show/bilax+monoidal+functor">bilax</a>, <a class="existingWikiWord" href="/nlab/show/Frobenius+monoidal+functor">Frobenius</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/braided+monoidal+functor">braided monoidal functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+functor">symmetric monoidal functor</a></p> </li> </ul> <p><strong>Internal monoids</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoid+in+a+monoidal+category">monoid in a monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/commutative+monoid+in+a+symmetric+monoidal+category">commutative monoid in a symmetric monoidal category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/module+over+a+monoid">module over a monoid</a></p> </li> </ul> <p><strong id="_examples">Examples</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+monoidal+structure+on+presheaves">closed monoidal structure on presheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Day+convolution">Day convolution</a></p> </li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/coherence+theorem+for+monoidal+categories">coherence theorem for monoidal categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+Dold-Kan+correspondence">monoidal Dold-Kan correspondence</a></p> </li> </ul> <p><strong>In higher category theory</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+2-category">monoidal 2-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/braided+monoidal+2-category">braided monoidal 2-category</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+bicategory">monoidal bicategory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/cartesian+bicategory">cartesian bicategory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/k-tuply+monoidal+n-category">k-tuply monoidal n-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/little+cubes+operad">little cubes operad</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monoidal+%28%E2%88%9E%2C1%29-category">monoidal (∞,1)-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+%28%E2%88%9E%2C1%29-category">symmetric monoidal (∞,1)-category</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+double+category">compact double category</a></p> </li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <ul> <li><a href='#AbsenceOfWeakeningAndContraction'>Absence of weakening and contraction</a></li> <li><a href='#AsAQuantumLogic'>As a quantum logic</a></li> <li><a href='#ResourceAvailability'>As a logic of resource availability</a></li> <li><a href='#game_semantics'>Game semantics</a></li> <li><a href='#as_a_relevance_logic'>As a relevance logic</a></li> </ul> <li><a href='#definition'>Definition</a></li> <li><a href='#variants'>Variants</a></li> <li><a href='#categorical_semantics'>Categorical semantics</a></li> <ul> <li><a href='#autonomous_categories'><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>-autonomous categories</a></li> <li><a href='#polycategories'>Polycategories</a></li> </ul> <li><a href='#game_semantics_2'>Game semantics</a></li> <li><a href='#multiple_exponential_operators'>Multiple exponential operators</a></li> <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='#in_relation_to_quantum_computing'>In relation to quantum computing</a></li> </ul> </ul> </div> <h2 id="idea">Idea</h2> <p><strong>Linear logic</strong> is a <a class="existingWikiWord" href="/nlab/show/substructural+logic">substructural logic</a> in which the <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a> and the <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening rule</a> are omitted, or at least have their applicability restricted.</p> <h3 id="AbsenceOfWeakeningAndContraction">Absence of weakening and contraction</h3> <p>Notice that <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction</a> and <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening</a> are the two <a class="existingWikiWord" href="/nlab/show/structural+rule">structural</a> <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a> which exhibit <a class="existingWikiWord" href="/nlab/show/context+extensions">context extensions</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mspace width="thinmathspace"></mspace><mo>↦</mo><mspace width="thinmathspace"></mspace><mi>Γ</mi><mo>,</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\Gamma \,\mapsto\, \Gamma, P</annotation></semantics></math> as admitting <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural</a> <a class="existingWikiWord" href="/nlab/show/diagonal+map">diagonal</a> and <a class="existingWikiWord" href="/nlab/show/projection">projection</a> <a class="existingWikiWord" href="/nlab/show/maps">maps</a>, respectively, hence as admitting <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpretation</a> as <em><a class="existingWikiWord" href="/nlab/show/cartesian+products">cartesian products</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>×</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\Gamma \times P</annotation></semantics></math> (cf. <a href="structural+rule#Jacobs94">Jacobs 1994</a>):</p> <div style="margin: -40px 0px 20px 10px"> <img src="/nlab/files/WeakeningContractionRules-230330d.jpg" width="600px" /> </div> <p>Therefore, when these <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a> are dropped then the resulting <a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative 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">\otimes</annotation></semantics></math> of contexts may still have <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpretation</a> as a <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric monoidal</a> <a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a> (such as known from the <a class="existingWikiWord" href="/nlab/show/tensor+product+of+vector+spaces">tensor product of vector spaces</a>) but not necessarily as a <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal</a> <a class="existingWikiWord" href="/nlab/show/product">product</a> (such as known from the <a class="existingWikiWord" href="/nlab/show/topological+product+space">product of topological spaces</a>).</p> <p>Accordingly, if <a class="existingWikiWord" href="/nlab/show/implication">implication</a> still follows the usual <a class="existingWikiWord" href="/nlab/show/inference+rule">inference rule</a> of <a class="existingWikiWord" href="/nlab/show/function+types">function types</a> but now with respect to a non-cartesian <a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative 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">\otimes</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊗</mo><mi>P</mi><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>⊢</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><msub><mi>t</mi> <mi>p</mi></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>T</mi></mrow><mrow><mi>Γ</mi><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>⊢</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo stretchy="false">(</mo><mi>p</mi><mo>↦</mo><msub><mi>t</mi> <mi>p</mi></msub><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>P</mi><mo>⊸</mo><mi>T</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{ \Gamma \otimes P \;\;\vdash\;\; t_p \,\colon\, T } { \Gamma \;\;\vdash\;\; (p \mapsto t_p) \,\colon\, P \multimap T } </annotation></semantics></math></div> <p>etc., then the <a class="existingWikiWord" href="/nlab/show/function+type">function type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>⊸</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">P \multimap T</annotation></semantics></math> may be <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpreted</a> as an <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> in a non-<a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian</a> <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed monoidal category</a> with <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric monoidal</a> <em><a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> — such as the category of <a class="existingWikiWord" href="/nlab/show/finite-dimensional+vector+spaces">finite-dimensional vector spaces</a>, in which case the <a class="existingWikiWord" href="/nlab/show/terms">terms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>P</mi><mo>⊸</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash f \colon P \multimap T</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpret</a> as <em><a class="existingWikiWord" href="/nlab/show/linear+functions">linear functions</a></em> — whence the <a class="existingWikiWord" href="/nlab/show/logical+connective">logical connective</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">\multimap</annotation></semantics></math>” is also called <em><a class="existingWikiWord" href="/nlab/show/linear+implication">linear implication</a></em>.</p> <p>Which exact flavour of <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a> provides <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> for linear logic depends on exactly which further <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a> are considered (see also at <em><a class="existingWikiWord" href="/nlab/show/bunched+logic">bunched logic</a></em>): In the original definition of <a href="#Girard1987">Girard (1987)</a>, linear logic is the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of/has <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> in <a class="existingWikiWord" href="/nlab/show/star-autonomous+categories">star-autonomous categories</a> (<a href="#Seely">Seely 89, prop. 1.5</a>). But more generally <em>linear logic</em> came to refer to the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of any possibly-non-<a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian</a> <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a> <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed monoidal category</a> (then usually called <em>multiplicative intuitionistic linear logic</em> – <em>MILL</em>) or even <a class="existingWikiWord" href="/nlab/show/polycategory">polycategory</a> (<a href="#Szabo78">Szabo 78</a> see the <a href="linear%20type%20theory#HistoryCategoricalSemantics">history section</a> and see also <a href="#dePaiva89">de Paiva 89</a>, <a href="#Blute91">Blute 91</a>, <a href="#BentonBiermanPaivaHyland92">Benton–Bierman–de Paiva–Hyland 92</a>, <a href="#HylandPaiva93">Hyland–de Paiva 93</a>, <a href="#Bierman95">Bierman 95</a>, <a href="#Barber97">Barber 97</a>, <a href="#Schalk04">Schalk 04</a>, <a href="#Mellies09">Melliès 09</a>). Under this interpretation, <em><a class="existingWikiWord" href="/nlab/show/proof+nets">proof nets</a></em> (or the associated <a class="existingWikiWord" href="/nlab/show/Kelly%E2%80%93Mac+Lane+graphs">Kelly–Mac Lane graphs</a>) of linear logic are similar to <a class="existingWikiWord" href="/nlab/show/string+diagrams">string diagrams</a> for monoidal categories.</p> <p>Indeed, these more general senses of linear logic still faithfully follow the original motivation for the term “linear” as connoting “resource availability” explained <a href="#ResourceAvailability">below</a>, since the non-cartesianness of the <a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a> means the absence of a <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a> map and hence the impossibility of <a class="existingWikiWord" href="/nlab/show/functions">functions</a> to depend on more than a single (linear) copy of their <a class="existingWikiWord" href="/nlab/show/variables">variables</a>.</p> <p>In addition to these usual “<a class="existingWikiWord" href="/nlab/show/denotational+semantics">denotational</a>” categorical semantics, linear logic also has an “<a class="existingWikiWord" href="/nlab/show/operational+semantics">operational</a>” categorical semantics, called the <em><a class="existingWikiWord" href="/nlab/show/Geometry+of+Interaction">Geometry of Interaction</a></em>, in <a class="existingWikiWord" href="/nlab/show/traced+monoidal+categories">traced monoidal categories</a>.</p> <p>Although linear logic is traditionally presented in terms of <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a>, it was apparently discovered by Girard while studying <a class="existingWikiWord" href="/nlab/show/coherence+spaces">coherence spaces</a>.</p> <h3 id="AsAQuantumLogic">As a quantum logic</h3> <p>With the archetypical <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of linear logic in the <a class="existingWikiWord" href="/nlab/show/compact+closed+category">compact closed category</a> of <a class="existingWikiWord" href="/nlab/show/finite+dimensional+vector+spaces">finite dimensional vector spaces</a> in mind, which is the habitat of <a class="existingWikiWord" href="/nlab/show/quantum+information+theory">quantum information theory</a> (see <a class="existingWikiWord" href="/nlab/show/quantum+information+theory+via+dagger-compact+categories">there</a> for more), one may naturally understand linear logic as a form of <a class="existingWikiWord" href="/nlab/show/quantum+logic">quantum logic</a> [<a href="#Pratt92">Pratt (1992)</a>] and in its natural <a class="existingWikiWord" href="/nlab/show/propositions+as+types">enhancement</a> to <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a> also as a <a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a>-<a class="existingWikiWord" href="/nlab/show/quantum+programming+language">language</a> [<a href="#AbramskyDuncan06">Abramsky & Duncan (2006)</a>; <a href="#Duncan06">Duncan (2006)</a>].</p> <blockquote> <p id="DalLagoFaggianQuote"> [<a href="#DalLagoFaggian12">Dal Lago & Faggian (2012)</a>]: “It’s more and more clear that strong relationships exist between <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a> and <a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a>. This seems to go well beyond the easy observation that the intrinsic resource-consciousness of linear logic copes well with the <a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">impossibility of cloning and erasing</a> qubits.”</p> <p>[<a href="#Staton15">Staton (2015), p. 1</a>]: “A <a class="existingWikiWord" href="/nlab/show/quantum+programming+language">quantum programming language</a> captures the ideas of <a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a> in a <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>.”</p> </blockquote> <p>Indeed:</p> <ol> <li> <p>the absence of the <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a> <a href="#AbsenceOfWeakeningAndContraction">above</a>, whose <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> is the <em>duplication</em> of <a class="existingWikiWord" href="/nlab/show/data">data</a>, exactly reflects the <em><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></em> of <a class="existingWikiWord" href="/nlab/show/quantum+physics">quantum physics</a></p> </li> <li> <p>the absence of the <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening rule</a> <a href="#AbsenceOfWeakeningAndContraction">above</a>, whose <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> is the <em>erasure</em> of <a class="existingWikiWord" href="/nlab/show/data">data</a>, exactly reflects the <a class="existingWikiWord" href="/nlab/show/no-deleting+theorem">no-deleting theorem</a>,</p> </li> <li> <p>the non-cartesian <a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative 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">\otimes</annotation></semantics></math>, whose <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> is given by <a class="existingWikiWord" href="/nlab/show/tensor+products">tensor products</a> (such as <a class="existingWikiWord" href="/nlab/show/tensor+product+of+Hilbert+spaces">of Hilbert spaces</a>), reflects the existence of <a class="existingWikiWord" href="/nlab/show/quantum+entanglement">entangled</a> <a class="existingWikiWord" href="/nlab/show/terms">terms</a> [<a href="#Baez04">Baez (2004)</a>].</p> </li> </ol> <p>Historically, linear logic was not explicitly motivated as a <a class="existingWikiWord" href="/nlab/show/quantum+logic">quantum logic</a> this way, but as a logic keeping track of “<em>resource availability</em>” (see <a href="#ResourceAvailability">below</a>), where (again due to the absence of the <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a>) a <a class="existingWikiWord" href="/nlab/show/variable">variable</a> could, a priori, be “only used once” and in fact (due to the absence of the <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening rule</a>) “exacty once”. However, meanwhile the resource concept has also (independently) penetrated <a class="existingWikiWord" href="/nlab/show/quantum+information+theory">quantum information theory</a> (for example, the <a class="existingWikiWord" href="/nlab/show/quantum+teleportation">quantum teleportation</a>-protocol uses <a class="existingWikiWord" href="/nlab/show/Bell+states">Bell states</a> as a resource that allow for and are consumed by the intended “teleportation” operation), see the references <a href="quantum+information#ReferencesQuantumResources">there</a>.</p> <h3 id="ResourceAvailability">As a logic of resource availability</h3> <p>Unlike many traditional formal systems of <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, which deal with the <em><a class="existingWikiWord" href="/nlab/show/truth">truth</a></em> of <em><a class="existingWikiWord" href="/nlab/show/propositions">propositions</a></em>, linear logic is often described and was originally motivated [<a href="#Girard1987">Girard (1987)</a>] as dealing with the <em>availability</em> of <em>resources</em>.</p> <p>A proposition, if it is true, remains true no matter how we use that fact in proving other propositions. By contrast, in using a resource <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> to make available a resource <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>, <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 may be consumed or otherwise modified. Linear logic deals with this by restricting our ability to duplicate or discard resources freely.</p> <p>For example:</p> <blockquote> <p>Let’s please add a better example!</p> </blockquote> <p>We have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtext>have cake</mtext><mo>⊢</mo><mtext>eat cake</mtext></mrow><annotation encoding="application/x-tex">\text{have cake} \vdash \text{eat cake}</annotation></semantics></math></div> <p>from which we can prove</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtext>have cake</mtext><mo>,</mo><mspace width="thickmathspace"></mspace><mtext>have cake</mtext><mo>⊢</mo><mtext>have cake</mtext><mo>∧</mo><mtext>eat cake</mtext></mrow><annotation encoding="application/x-tex">\text{have cake},\; \text{have cake} \vdash \text{have cake} \wedge \text{eat cake} </annotation></semantics></math></div> <p>which by left <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction</a> (duplication of inputs) in <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a> yields</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtext>have cake</mtext><mo>⊢</mo><mtext>have cake</mtext><mo>∧</mo><mtext>eat cake</mtext></mrow><annotation encoding="application/x-tex">\text{have cake} \vdash \text{have cake} \wedge \text{eat cake}</annotation></semantics></math></div> <p>Linear logic would disallow the <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction</a> step and treat <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mtext>have cake</mtext><mo>,</mo><mspace width="thickmathspace"></mspace><mtext>have cake</mtext><mo>⊢</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\text{have cake},\; \text{have cake} \vdash A</annotation></semantics></math> as explicitly meaning that <em>two</em> slices of cake yield <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>. Disallowing contraction then corresponds to the fact that we can’t turn one slice of cake into two (more’s the pity), so you can't have your cake and eat it too.</p> <h3 id="game_semantics">Game semantics</h3> <p>Linear logic can also be interpreted using a semantics of “games” or “interactions”. Under this interpretation, each proposition in a sequent represents a game being played or a transaction protocol being executed. An assertion of, for instance,</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>,</mo><mi>Q</mi><mo>⊢</mo><mi>R</mi></mrow><annotation encoding="application/x-tex"> P, Q \vdash R </annotation></semantics></math></div> <p>means roughly that if I am playing three simultaneous games of <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Q</mi></mrow><annotation encoding="application/x-tex">Q</annotation></semantics></math>, and <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>, in which I am the left player in <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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Q</mi></mrow><annotation encoding="application/x-tex">Q</annotation></semantics></math> and the right player in <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>, then I have a strategy which will enable me to win at least one of them. Now the above statements about “resources” translate into saying that I have to play in all the games I am given and can’t invent new ones on the fly.</p> <p>For example, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>⊢</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">P \vdash P</annotation></semantics></math> can be won by using the copycat strategy where one makes the two games identical except with left and right players reversed.</p> <h3 id="as_a_relevance_logic">As a relevance logic</h3> <p>Linear logic is closely related to notions of <a class="existingWikiWord" href="/nlab/show/relevance+logic">relevance logic</a>, which have been studied for much longer. The goal of relevance logic is to disallow statements like “if pigs can fly, then grass is green” which are true, under the usual logical interpretation of <a class="existingWikiWord" href="/nlab/show/implication">implication</a>, but in which the hypothesis has nothing to do with the conclusion. Clearly there is a relationship with the “resource semantics”: if we want to require that all hypotheses are “used” in a proof then we need to disallow weakening. In linear logic, all hypotheses must be used <em>exactly once</em>, whereas in relevance logic(s), all hypotheses must be used <em>at least</em> once.</p> <h2 id="definition">Definition</h2> <p>Linear logic is usually given in terms of <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>. There is a set of <strong><a class="existingWikiWord" href="/nlab/show/propositions">propositions</a></strong> (although as remarked above, to be thought of more as resources to be acquired than as statements to be proved) which we construct through <a class="existingWikiWord" href="/nlab/show/recursion">recursion</a>. Each pair of <a class="existingWikiWord" href="/nlab/show/lists">lists</a> of propositions is a <strong>sequent</strong> (written as usual 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">\vdash</annotation></semantics></math>’ between the lists), some of which are <strong>valid</strong>; we determine which are valid also through recursion. Technically, the <a class="existingWikiWord" href="/nlab/show/propositional+calculus">propositional calculus</a> of linear logic also requires a set of <strong>propositional variables</strong> from which to start; this is usually identified with the set of <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> (so the variables are <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>p</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">p_0</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>p</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">p_1</annotation></semantics></math>, etc), although one can also consider the linear logic <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>LL</mi><mo stretchy="false">(</mo><mi>V</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">LL(V)</annotation></semantics></math> where <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> is any initial <a class="existingWikiWord" href="/nlab/show/set">set</a> of propositional variables.</p> <p>Here we define the set of propositions:</p> <ul> <li> <p>Every propositional variable is a proposition.</p> </li> <li> <p>For each proposition <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>, there is a proposition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>A</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">A^\perp</annotation></semantics></math>, the <strong><a class="existingWikiWord" href="/nlab/show/negation">negation</a></strong> 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>.</p> </li> <li> <p>For each proposition <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 proposition <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>, there are four additional propositions:</p> <ul> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mi>&</mi><mi>B</mi></mrow><annotation encoding="application/x-tex">A \& B</annotation></semantics></math> (read ‘with’), the <strong><a class="existingWikiWord" href="/nlab/show/additive+conjunction">additive conjunction</a></strong> 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> and <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>;</p> </li> <li> <p><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 \oplus B</annotation></semantics></math> (read ‘plus’), the <strong><a class="existingWikiWord" href="/nlab/show/additive+disjunction">additive disjunction</a></strong> 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> and <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>;</p> </li> <li> <p><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 \otimes B</annotation></semantics></math> (read ‘times’), the <strong><a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative conjunction</a></strong> 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> and <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>;</p> </li> <li> <p><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 \parr B</annotation></semantics></math> (read ‘par’), the <strong><a class="existingWikiWord" href="/nlab/show/multiplicative+disjunction">multiplicative disjunction</a></strong> 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> and <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> (sometimes written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo lspace="mediummathspace" rspace="mediummathspace">∣</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \mid B</annotation></semantics></math>).</p> </li> </ul> </li> <li> <p>There are also four constants to go with the four binary operations above:</p> <ul> <li> <p><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> (read ‘top’), the <strong>additive <a class="existingWikiWord" href="/nlab/show/truth">truth</a></strong>;</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0}</annotation></semantics></math> (read ‘zero’), the <strong>additive <a class="existingWikiWord" href="/nlab/show/falsity">falsity</a></strong>;</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math> (read ‘one’), the <strong>multiplicative truth</strong>;</p> </li> <li> <p><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> (read ‘bottom’), the <strong>multiplicative falsity</strong>.</p> </li> </ul> </li> <li> <p>For each proposition <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>, there are two additional propositions:</p> <ul> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!{A}</annotation></semantics></math> (read ‘<a class="existingWikiWord" href="/nlab/show/of+course">of course</a>’), the <strong><a class="existingWikiWord" href="/nlab/show/exponential+conjunction">exponential conjunction</a></strong> 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>;</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">?{A}</annotation></semantics></math> (read ‘<a class="existingWikiWord" href="/nlab/show/why+not">why not</a>’), the <strong><a class="existingWikiWord" href="/nlab/show/exponential+disjunction">exponential disjunction</a></strong> 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>.</p> </li> </ul> </li> </ul> <p>The terms “exponential”, “multiplicative”, and “additive” come from the fact that “exponentiation converts addition to multiplication”: we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mrow><mo stretchy="false">(</mo><mi>A</mi><mi>&</mi><mi>B</mi><mo stretchy="false">)</mo></mrow><mo>≡</mo><mo>!</mo><mi>A</mi><mo>⊗</mo><mo>!</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">!{(A \& B)}\equiv !{A} \otimes !{B}</annotation></semantics></math> and so on (see below).</p> <p>However, the connectives and constants can also be grouped in different ways. For instance, the multiplicative conjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> and additive disjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊕</mo></mrow><annotation encoding="application/x-tex">\oplus</annotation></semantics></math> are both <a class="existingWikiWord" href="/nlab/show/positive+types">positive types</a>, while the additive conjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</annotation></semantics></math> and multiplicative disjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/negative+types">negative types</a>. Similarly, the multiplicative truth <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math> and the additive falsity <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0}</annotation></semantics></math> are positive, while the additive truth <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 multiplicative falsity <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> are negative. This grouping has the advantage that the similarity of symbols matches the adjective used (because the symbols were chosen with this grouping in mind).</p> <p>But conversely, the natural grouping by multiplicative/additive, or equivalently by de Morgan dual pairs, has led many authors to alter Girard’s notation, in particular reverting to the category-theoretic <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>×</mo></mrow><annotation encoding="application/x-tex">\times</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace" rspace="0em">+</mo></mrow><annotation encoding="application/x-tex">+</annotation></semantics></math> for the additives <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</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">\oplus</annotation></semantics></math>, and introducing a different symbol such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊙</mo></mrow><annotation encoding="application/x-tex">\odot</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">\bullet</annotation></semantics></math> or (confusingly) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊕</mo></mrow><annotation encoding="application/x-tex">\oplus</annotation></semantics></math> for Girard’s <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math>. But on this page we will stick to Girard’s conventions for consistency.</p> <p>In <a class="existingWikiWord" href="/nlab/show/relevance+logic">relevance logic</a>, the terms “conjunction” and “disjunction” are often reserved for the additive versions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</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">\oplus</annotation></semantics></math>, which are written with the traditional notations <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">\vee</annotation></semantics></math>. In this case, the multiplicative conjunction <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\otimes B</annotation></semantics></math> is called <strong>fusion</strong> and denoted <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\circ B</annotation></semantics></math>, while the multiplicative disjunction <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\parr B</annotation></semantics></math> is called <strong>fission</strong> and denoted <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+B</annotation></semantics></math> (or sometimes, confusingly, <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\oplus B</annotation></semantics></math>). In relevance logic the symbol <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> may also be used for the <em>additive</em> falsity, here denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0}</annotation></semantics></math>. Also, sometimes the additive connectives are called <strong>extensional</strong> and the multiplicatives <strong>intensional</strong>.</p> <p>Sometimes one does not define the operation of negation, defining only <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">p^\perp</annotation></semantics></math> for a propositional variable <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>. It is a theorem that every proposition above is equivalent (in the sense defined below) to a proposition in which negation is applied only to propositional variables.</p> <p>We now define the valid sequents, where we write <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><mo>⊢</mo><mi>D</mi><mo>,</mo><mi>E</mi><mo>,</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">A, B, C \vdash D, E, F</annotation></semantics></math> to state the validity of the sequent consisting of the list <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A,B,C)</annotation></semantics></math> and the list <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>D</mi><mo>,</mo><mi>E</mi><mo>,</mo><mi>F</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(D,E,F)</annotation></semantics></math> and use Greek letters for sublists:</p> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/structural+rules">structural rules</a>:</p> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/exchange+rule">exchange rule</a>: If a sequent is valid, then any <a class="existingWikiWord" href="/nlab/show/permutation">permutation</a> of it (created by permuting its left and right sides independently) is valid.</p> </li> <li> <p>The restricted <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening rule</a>: If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, !{A}, \Delta \vdash \Theta</annotation></semantics></math>, for any <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>; conversely and dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, ?{A}, \Theta</annotation></semantics></math> for any <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 restricted <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a>: If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, !{A}, !{A}, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, !{A}, \Delta \vdash \Theta</annotation></semantics></math>; conversely and dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, ?{A}, ?{A}, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, ?{A}, \Theta</annotation></semantics></math>.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/variable+rule">variable rule</a>: Always, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊢</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">A \vdash A</annotation></semantics></math>;</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a>: If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>,</mo><mi>Φ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash A, \Phi</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>A</mi><mo>⊢</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Psi,A \vdash \Delta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ψ</mi><mo>,</mo><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>Φ</mi></mrow><annotation encoding="application/x-tex">\Psi,\Gamma \vdash \Delta,\Phi</annotation></semantics></math>.</p> </li> </ul> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a> for each operation:</p> <ul> <li> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>,</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash A, \Delta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><msup><mi>A</mi> <mo>⊥</mo></msup><mo>⊢</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A^\perp \vdash \Delta</annotation></semantics></math>; conversely and dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>⊢</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \vdash \Delta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><msup><mi>A</mi> <mo>⊥</mo></msup><mo>,</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash A^\perp, \Delta</annotation></semantics></math>.</p> </li> <li> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A, \Delta \vdash \Theta</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, B, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mi>&</mi><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \& B, \Delta \vdash \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A, \Theta</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><mo>,</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, B, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mi>&</mi><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A \& B, \Theta</annotation></semantics></math>.</p> </li> <li> <p>Dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A, \Theta</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, B, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>⊕</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A \oplus B, \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A, \Delta \vdash \Theta</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>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, B, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>⊕</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \oplus B, \Delta \vdash \Theta</annotation></semantics></math>.</p> </li> <li> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A, B, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \otimes B, \Delta \vdash \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A</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>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Lambda \vdash B, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>Λ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, \Lambda \vdash \Delta, A \otimes B, \Theta</annotation></semantics></math>.</p> </li> <li> <p>Dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A, B, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>⅋</mo><mi>B</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A \parr B, \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>⊢</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \vdash \Delta</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>,</mo><mi>Θ</mi><mo>⊢</mo><mi>Λ</mi></mrow><annotation encoding="application/x-tex">B, \Theta \vdash \Lambda</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>⅋</mo><mi>B</mi><mo>,</mo><mi>Θ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>Λ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \parr B, \Theta \vdash \Delta, \Lambda</annotation></semantics></math>.</p> </li> <li> <p>Always <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>⊤</mo><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, \top, \Theta</annotation></semantics></math>; dually (there is no converse), <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, \mathbf{0}, \Delta \vdash \Theta</annotation></semantics></math>.</p> </li> <li> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, \mathbf{1}, \Delta \vdash \Theta</annotation></semantics></math>; conversely, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\vdash \mathbf{1}</annotation></semantics></math>.</p> </li> <li> <p>Dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>⊥</mo><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, \bot, \Theta</annotation></semantics></math>; conversely, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\bot \vdash</annotation></semantics></math>.</p> </li> <li> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, !{A}, \Delta \vdash \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>!</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, !{A}, \Theta</annotation></semantics></math>, whenever <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> consists entirely of propositions of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo lspace="verythinmathspace" rspace="0em">−</mo></mrow><annotation encoding="application/x-tex">!{-}</annotation></semantics></math> while <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\Delta</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">\Theta</annotation></semantics></math> consist entirely of propositions of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mo lspace="verythinmathspace" rspace="0em">−</mo></mrow><annotation encoding="application/x-tex">?{-}</annotation></semantics></math>.</p> </li> <li> <p>Dually, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, A, \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>Δ</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash \Delta, ?{A}, \Theta</annotation></semantics></math>; conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, A, \Delta \vdash \Theta</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mo>?</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Gamma, ?{A}, \Delta \vdash \Theta</annotation></semantics></math>, whenever <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> 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">\Delta</annotation></semantics></math> consist entirely of propositions of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo lspace="verythinmathspace" rspace="0em">−</mo></mrow><annotation encoding="application/x-tex">!{-}</annotation></semantics></math> while <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Θ</mi></mrow><annotation encoding="application/x-tex">\Theta</annotation></semantics></math> consists entirely of propositions of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mo lspace="verythinmathspace" rspace="0em">−</mo></mrow><annotation encoding="application/x-tex">?{-}</annotation></semantics></math>.</p> </li> </ul> </li> </ul> <p>The main point of linear logic is the restricted use of the weakening and contraction rules; if these were universally valid (applying to any <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> rather than only to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!{A}</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">?{A}</annotation></semantics></math>), then the additive and multiplicative operations would be equivalent (in the sense defined below) and similarly <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><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><mo>?</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">?{A}</annotation></semantics></math> would be equivalent to <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 would give us <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>. On the other hand, one can also remove the exchange rule to get a variety of <span class="newWikiWord">noncommutative logic<a href="/nlab/new/noncommutative+logic">?</a></span>; one must then be careful about how to write the other rules (which we have been above).</p> <p>As usual, there is a theorem of <a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> showing that the cut rule and identity rule follow from all other rules and the special cases of the identity rule of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>⊢</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">p \vdash p</annotation></semantics></math> for a propositional variable <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>.</p> <p>The propositions <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>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> are (propositionally) <strong>equivalent</strong> if <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 \vdash B</annotation></semantics></math> and <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 \vdash A</annotation></semantics></math> are both valid, which we express by writing <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 \equiv B</annotation></semantics></math>. It is then a theorem that either may be swapped for the other anywhere in a sequent without affecting its validity. Up to equivalence, negation is an <a class="existingWikiWord" href="/nlab/show/involution">involution</a>, and the operations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</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">\oplus</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">\otimes</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">\parr</annotation></semantics></math> are all <a class="existingWikiWord" href="/nlab/show/associative">associative</a>, with respective <a class="existingWikiWord" href="/nlab/show/identity+elements">identity elements</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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</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>. These operations are also <a class="existingWikiWord" href="/nlab/show/commutative+operation">commutative</a> (although this fails for the multiplicative connectives if we drop the exchange rule). The additive connectives are also <a class="existingWikiWord" href="/nlab/show/idempotent">idempotent</a> (but the multiplicative ones are not).</p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>There is a more refined notion of equivalence, where we pay attention to specific derivations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\pi: A \vdash B</annotation></semantics></math> of sequents, and deem two derivations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo>,</mo><mi>π</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">\pi, \pi'</annotation></semantics></math> of <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 \vdash B</annotation></semantics></math> <em>Lambek-equivalent</em> if they map to the same morphism under any categorical semantics <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>; see below. Given a pair of derivations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\pi: A \vdash B</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>B</mi><mo>⊢</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\rho: B \vdash A</annotation></semantics></math>, it then makes sense to ask whether they are Lambek-inverse to one another (i.e., whether <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">(</mo><mi>ρ</mi><mo stretchy="false">)</mo><mo>=</mo><mi>S</mi><mo stretchy="false">(</mo><mi>π</mi><msup><mo stretchy="false">)</mo> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup></mrow><annotation encoding="application/x-tex">S(\rho) = S(\pi)^{-1}</annotation></semantics></math> under any semantics), so that the derivations exhibit an isomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo>≅</mo><mi>S</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">S(A) \cong S(B)</annotation></semantics></math> under any semantics <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>. This equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><msub><mo>≡</mo> <mi>Lambek</mi></msub><mi>B</mi></mrow><annotation encoding="application/x-tex">A \equiv_{Lambek} B</annotation></semantics></math> is strictly stronger than propositional equivalence. It should be observed that all equivalences <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 \equiv B</annotation></semantics></math> listed below are in fact Lambek equivalences.</p> </div> <p>We also have <a class="existingWikiWord" href="/nlab/show/distributive+law">distributive laws</a> that explain the adjectives ‘additive’, ‘multiplicative’, and ‘exponential’:</p> <ul> <li>Multiplication distributes over addition if one is a conjunction and one is a disjunction: <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>B</mi><mo>⊕</mo><mi>C</mi><mo stretchy="false">)</mo><mo>≡</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo stretchy="false">)</mo><mo>⊕</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A \otimes (B \oplus C) \equiv (A \otimes B) \oplus (A \otimes C)</annotation></semantics></math> (and on the other side);</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mo stretchy="false">(</mo><mi>B</mi><mi>&</mi><mi>C</mi><mo stretchy="false">)</mo><mo>≡</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⅋</mo><mi>B</mi><mo stretchy="false">)</mo><mi>&</mi><mo stretchy="false">(</mo><mi>A</mi><mo>⅋</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A \parr (B \& C) \equiv (A \parr B) \& (A \parr C)</annotation></semantics></math> (and on the other side);</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊗</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle><mo>≡</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">A \otimes \mathbf{0} \equiv \mathbf{0}</annotation></semantics></math> (and on the other side);</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mo>⊤</mo><mo>≡</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">A \parr \top \equiv \top</annotation></semantics></math> (and on the other side).</li> </ul> </li> <li>Exponentiation converts addition into multiplication if all are conjunctions or all are disjunctions: <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mrow><mo stretchy="false">(</mo><mi>A</mi><mi>&</mi><mi>B</mi><mo stretchy="false">)</mo></mrow><mo>≡</mo><mo>!</mo><mi>A</mi><mo>⊗</mo><mo>!</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">!{(A \& B)} \equiv !{A} \otimes !{B}</annotation></semantics></math>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>⊕</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><mo>≡</mo><mo>?</mo><mi>A</mi><mo>⅋</mo><mo>?</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">?{(A \oplus B)} \equiv ?{A} \parr ?{B}</annotation></semantics></math>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>⊤</mo><mo>≡</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">!{\top} \equiv \mathbf{1}</annotation></semantics></math>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle><mo>≡</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">?{\mathbf{0}} \equiv \bot</annotation></semantics></math>.</li> </ul> </li> </ul> <p>It is also a theorem that negation (except for the negations of propositional variables) can be defined (up to equivalence) recursively as follows:</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msup><mi>A</mi> <mo>⊥</mo></msup><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup><mo>≡</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">(A^\perp)^\perp \equiv A</annotation></semantics></math>;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mi>&</mi><mi>B</mi><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup><mo>≡</mo><msup><mi>A</mi> <mo>⊥</mo></msup><mo>⊕</mo><msup><mi>B</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">(A \& B)^\perp \equiv A^\perp \oplus B^\perp</annotation></semantics></math> and vice versa;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup><mo>≡</mo><msup><mi>A</mi> <mo>⊥</mo></msup><mo>⅋</mo><msup><mi>B</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">(A \otimes B)^\perp \equiv A^\perp \parr B^\perp</annotation></semantics></math> and vice versa;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>⊤</mo> <mo>⊥</mo></msup><mo>≡</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\top^\perp \equiv \mathbf{0}</annotation></semantics></math> and vice versa;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mstyle mathvariant="bold"><mn>1</mn></mstyle> <mo>⊥</mo></msup><mo>≡</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\mathbf{1}^\perp \equiv \bot</annotation></semantics></math> and vice versa;</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo>!</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup><mo>≡</mo><mo>?</mo><mrow><msup><mi>A</mi> <mo>⊥</mo></msup></mrow></mrow><annotation encoding="application/x-tex">(!{A})^\perp \equiv ?{A^\perp}</annotation></semantics></math> and vice versa.</li> </ul> <p>The logical rules for <a class="existingWikiWord" href="/nlab/show/negation">negation</a> can then be proved.</p> <p>In this way, linear logic in the original sense (interpreted in <a class="existingWikiWord" href="/nlab/show/star-autonomous+categories">star-autonomous categories</a>) has a perfect <a class="existingWikiWord" href="/nlab/show/de+Morgan+duality">de Morgan duality</a>. But observe that more general variants (interpreted in more general <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+categories">symmetric monoidal categories</a>) need not, see for instance (<a href="#HylandPaiva93">Hyland–de Paiva 93</a>).</p> <p>We can also restrict attention to sequents with one term on either side as follows: <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">\Gamma \vdash \Delta</annotation></semantics></math> is valid if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⨂</mo><mi>Γ</mi><mo>⊢</mo><mo>⅋</mo><mi>Δ</mi></mrow><annotation encoding="application/x-tex">\bigotimes \Gamma \vdash \parr \Delta</annotation></semantics></math> is valid, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⨂</mo><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>≔</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo>⊗</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">\bigotimes(A, B, C) \coloneqq A \otimes B \otimes C</annotation></semantics></math>, etc, and similarly for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math> (using implicitly that these are associative, with identity elements to handle the <a class="existingWikiWord" href="/nlab/show/empty+sequence">empty sequence</a>).</p> <p>We can even restrict attention to sequents with no term on the left side and one term on the right; <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 \vdash B</annotation></semantics></math> is valid if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>A</mi><mo>⊸</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\vdash A \multimap B</annotation></semantics></math> is valid, where <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><msup><mi>A</mi> <mo>⊥</mo></msup><mo>⅋</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \multimap B \coloneqq A^\perp \parr B</annotation></semantics></math>. In this way, it's possible to ignore sequents entirely and speak only of propositions and valid propositions, eliminating half of the logical rules in the process. However, this approach is not as beautifully symmetric as the full sequent calculus.</p> <h2 id="variants">Variants</h2> <p>The logic described above is full classical linear logic. There are many important <a class="existingWikiWord" href="/nlab/show/fragments">fragments</a> and variants of linear logic, such as:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/multiplicative+linear+logic">multiplicative linear logic</a> (MLL), which contains only <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>,</mo><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\otimes,\parr</annotation></semantics></math> and their units <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>,</mo><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\mathbf{1},\bot</annotation></semantics></math> as well as the negation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">(-)^\perp</annotation></semantics></math>.</p> </li> <li> <p>multiplicative-exponential linear logic (MELL), which contains only <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>,</mo><mo>⅋</mo><mo>,</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>,</mo><mo>⊥</mo><mo>,</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">\otimes,\parr,\mathbf{1},\bot,(-)^\perp</annotation></semantics></math> and the exponential modalities <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>,</mo><mo>?</mo></mrow><annotation encoding="application/x-tex">!,?</annotation></semantics></math>.</p> </li> <li> <p>multiplicative-additive linear logic (MALL), which contains everything <em>except</em> the exponential modalities <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>,</mo><mo>?</mo></mrow><annotation encoding="application/x-tex">!,?</annotation></semantics></math>.</p> </li> <li> <p>multiplicative intuitionistic linear logic (MILL), which contains only <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>,</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>,</mo><mo>⊸</mo></mrow><annotation encoding="application/x-tex">\otimes,\mathbf{1},\multimap</annotation></semantics></math> (the latter now as a primitive operation); in particular there is no longer the involutive negation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">(-)^\perp</annotation></semantics></math>. The sequents are also restricted to have only one formula on the right.</p> </li> <li> <p>intuitionistic linear logic (ILL), which contains all the additive connectives <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi><mo>,</mo><mo>⊕</mo><mo>,</mo><mstyle mathvariant="bold"><mn>0</mn></mstyle><mo>,</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\&,\oplus,\mathbf{0},\top</annotation></semantics></math> as well as the intutionistic multiplicatives <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo><mo>,</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>,</mo><mo>⊸</mo></mrow><annotation encoding="application/x-tex">\otimes,\mathbf{1},\multimap</annotation></semantics></math> and the exponential <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>, with one formula on the right as above. In this case all connectives are all independent of each other.</p> </li> <li> <p>full intuitionistic linear logic (FILL), which in addition to ILL contains the multiplicative disjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math>, and perhaps the exponential <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>. (Sometimes ILL without <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo><mo>,</mo><mo>?</mo></mrow><annotation encoding="application/x-tex">\parr,?</annotation></semantics></math> is also called “full” intuitionistic linear logic.)</p> </li> <li> <p>non-commutative linear logics (braided or not)</p> </li> <li> <p>“light” and “soft” linear logics, which limit the use of ! to constrain the computational complexity of proofs</p> </li> <li> <p>first-order linear logic, which adds quantifiers <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> 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">\forall</annotation></semantics></math> (sometimes denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo></mrow><annotation encoding="application/x-tex">\bigvee</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">⋀</mo></mrow><annotation encoding="application/x-tex">\bigwedge</annotation></semantics></math>), either over a fixed domain or over varying types. These quantifiers are usually considered “additive”; for a theory that has a certain kind of “multiplicative quantifier” see <a class="existingWikiWord" href="/nlab/show/bunched+implication">bunched implication</a>.</p> </li> </ul> <p>One can also consider adding additional rules to linear logic. For instance, by adding the <a class="existingWikiWord" href="/nlab/show/weakening+rule">weakening rule</a> (but not the <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a>) one obtains <a class="existingWikiWord" href="/nlab/show/affine+logic">affine logic</a>, whereas by adding contraction but not weakening one obtains <a class="existingWikiWord" href="/nlab/show/relevance+logic">relevance logic</a>. Another rule that is sometimes considered is the <a class="existingWikiWord" href="/nlab/show/mix+rule">mix rule</a>.</p> <p><a class="existingWikiWord" href="/nlab/show/linear-non-linear+logic">Linear-non-linear logic</a> is an equivalent presentation of intuitionistic linear logic that decomposes the <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> modality into an adjunction between a cartesian logic and a linear one in which cartesian variables can also appear.</p> <p>Some models of linear logic allow for a <em>codereliction</em> operation, which allows for one to take the “linear approximation” of a proof <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">!(A) \to B</annotation></semantics></math>. These models lead to the development of <em>differential linear logic</em>, the categorical semantics of which was laid out in (<a href="#Blute-Cockett-Seely06">Blute–Cockett–Seely</a>).</p> <h2 id="categorical_semantics">Categorical semantics</h2> <p>We discuss the <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of linear logic. See also at <em><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></em>.</p> <h3 id="autonomous_categories"><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>-autonomous categories</h3> <p>One way to explain linear logic to a category theorist is to say that its models are <a class="existingWikiWord" href="/nlab/show/%2A-autonomous+categories">*-autonomous categories</a> with extra structure (<a href="#Seely">Seely, 1989, prop. 1.5</a>). (If the underlying category is a <a class="existingWikiWord" href="/nlab/show/suplattice">suplattice</a> then these are commutative <a class="existingWikiWord" href="/nlab/show/quantales">quantales</a>, (<a href="#Yetter90">Yetter 90</a>))</p> <p>Firstly, there is a monoidal ‘<a class="existingWikiWord" href="/nlab/show/tensor+product">tensor</a>’ connective <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 \otimes B</annotation></semantics></math>. <a class="existingWikiWord" href="/nlab/show/negation">Negation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>A</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">A^\bot</annotation></semantics></math> is modelled by the <a class="existingWikiWord" href="/nlab/show/dual+object">dual object</a> involution <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">(-)^*</annotation></semantics></math>, while <a class="existingWikiWord" href="/nlab/show/linear+implication">linear implication</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\multimap B</annotation></semantics></math> corresponds to the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a>, which can be defined as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><msup><mi>B</mi> <mo>⊥</mo></msup><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">(A\otimes B^\bot)^\bot</annotation></semantics></math>. There is a <a class="existingWikiWord" href="/nlab/show/de+Morgan+dual">de Morgan dual</a> of the tensor called ‘par’, with <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><mo stretchy="false">(</mo><msup><mi>A</mi> <mo>⊥</mo></msup><mo>⊗</mo><msup><mi>B</mi> <mo>⊥</mo></msup><msup><mo stretchy="false">)</mo> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">A \parr B = (A^\bot\otimes B^\bot)^\bot</annotation></semantics></math>. Tensor and par are the ‘multiplicative’ connectives, which roughly speaking represent the parallel availability of resources.</p> <p>The ‘additive’ connectives <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</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">\oplus</annotation></semantics></math>, which correspond in another way to traditional <a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a> and <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a>, are modelled as usual by <a class="existingWikiWord" href="/nlab/show/products">products</a> and <a class="existingWikiWord" href="/nlab/show/coproducts">coproducts</a>. <a href="#Seely">Seely (1989)</a> notes that products are sufficient, as <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>-autonomy then guarantees the existence of coproducts; that is, they are also linked by <a class="existingWikiWord" href="/nlab/show/de+Morgan+duality">de Morgan duality</a>.</p> <p>Recall also that linear logic recaptures the notion of a resource that can be discarded or copied arbitrarily by the use of the <a class="existingWikiWord" href="/nlab/show/modal+logic">modal</a> operator <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/exponential+modality">exponential modality</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!A</annotation></semantics></math> denotes an ‘<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>-factory’, a resource that can produce zero or more <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>s on demand. It is modelled using a suitably monoidal <a class="existingWikiWord" href="/nlab/show/comonad">comonad</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">!</annotation></semantics></math> on the underlying <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>-autonomous category. There are various inequivalent ways to make this precise, however; see <a href="https://ncatlab.org/nlab/show/!-modality">!-modality</a> for discussion.</p> <p>An LL sequent</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>A</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>A</mi> <mi>n</mi></msub><mo>⊢</mo><msub><mi>B</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>B</mi> <mi>m</mi></msub></mrow><annotation encoding="application/x-tex">A_1,\ldots,A_n \vdash B_1,\ldots,B_m</annotation></semantics></math></div> <p>is interpreted as a morphism</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mo>⊗</mo> <mi>i</mi></msub><msub><mi>A</mi> <mi>i</mi></msub><mo>→</mo><msub><mo>⅋</mo> <mi>j</mi></msub><msub><mi>B</mi> <mi>j</mi></msub></mrow><annotation encoding="application/x-tex"> \otimes_i A_i \to \parr_j B_j </annotation></semantics></math></div> <p>The comonoid structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!A</annotation></semantics></math> then yields the weakening</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊗</mo><mo>!</mo><mi>A</mi><mo>→</mo><mi>Γ</mi><mo>⊗</mo><mi>I</mi><mo>→</mo><mi>Γ</mi></mrow><annotation encoding="application/x-tex"> \Gamma\otimes !A \to \Gamma \otimes I \to \Gamma</annotation></semantics></math></div> <p>and contraction</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊗</mo><mo>!</mo><mi>A</mi><mo>→</mo><mi>Γ</mi><mo>⊗</mo><mo>!</mo><mi>A</mi><mo>⊗</mo><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex"> \Gamma\otimes !A \to \Gamma \otimes !A \otimes !A </annotation></semantics></math></div> <p>maps. The corresponding rules are interpreted by precomposing the interpretation of a sequent with one of these maps.</p> <p>The (co)-<a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a> 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> is <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed</a>, and the product there coincides with the product in the base category. The <a class="existingWikiWord" href="/nlab/show/exponential+object">exponential</a> (unsurprisingly for a Kleisli category) is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>B</mi> <mi>A</mi></msup><mo>≅</mo><mo>!</mo><mi>A</mi><mo>⊸</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">B^A \cong !A\multimap B</annotation></semantics></math>.</p> <p>Particular monoidal 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">*</annotation></semantics></math>-autonomous <a class="existingWikiWord" href="/nlab/show/posets">posets</a> for modeling linear logic can be obtained by <a class="existingWikiWord" href="/nlab/show/Day+convolution">Day convolution</a> from <a class="existingWikiWord" href="/nlab/show/ternary+frames">ternary frames</a>. This includes Girard’s <em>phase spaces</em> as a particular example.</p> <p>First-order linear logic is correspondingly modeled in a <a class="existingWikiWord" href="/nlab/show/linear+hyperdoctrine">linear hyperdoctrine</a>.</p> <h3 id="polycategories">Polycategories</h3> <p>A different way to explain linear logic categorically (though equivalent, in the end) is to start with a categorical structure which lacks any of the connectives, but has sufficient structure to enable us to characterize them with universal properties. If we ignore the exponentials for now, such a structure is given by a <a class="existingWikiWord" href="/nlab/show/polycategory">polycategory</a>. The polymorphisms</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>A</mi><mo>,</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>D</mi><mo>,</mo><mi>E</mi><mo>,</mo><mi>F</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A,B,C) \to (D,E,F)</annotation></semantics></math></div> <p>in a polycategory correspond to sequents <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><mo>⊢</mo><mi>D</mi><mo>,</mo><mi>E</mi><mo>,</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">A,B,C \vdash D,E,F</annotation></semantics></math> in linear logic. The multiplicative connectives are then characterized by representability and corepresentability properties:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><mrow><mi>A</mi><mo>⊗</mo><mi>B</mi><mo>→</mo><mi>C</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{(A,B) \to C}{A\otimes B \to C}</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><mfrac><mrow><mi>A</mi><mo>→</mo><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><mrow><mi>A</mi><mo>→</mo><mi>B</mi><mo>⅋</mo><mi>C</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{A \to (B,C)}{A \to B\parr C}</annotation></semantics></math></div> <p>(Actually, we should allow arbitrarily many unrelated objects to carry through in both cases.) The additives are similarly characterized as categorical products and coproducts, in a polycategorically suitable sense.</p> <p>Finally, dual objects can be recovered as a sort of “adjoint”:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><mrow><mi>A</mi><mo>→</mo><mo stretchy="false">(</mo><msup><mi>B</mi> <mo>*</mo></msup><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{(A,B) \to C}{A \to (B^*,C)}</annotation></semantics></math></div> <p>If all these representing objects exist, then we recover 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">*</annotation></semantics></math>-autonomous category.</p> <p>One merit of the polycategory approach is that it makes the role of the structural rules clearer, and also helps explain why <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math> sometimes seems like a disjunction and sometimes like a conjunction. Allowing contraction and weakening on the left corresponds to our polycategory being “left <a class="existingWikiWord" href="/nlab/show/cartesian+multicategory">cartesian</a>”; that is, we have “diagonal” and “projection” operations such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>A</mi><mo>;</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Hom</mi><mo stretchy="false">(</mo><mi>A</mi><mo>;</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom(A,A; B) \to Hom(A;B)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo stretchy="false">(</mo><mo>;</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Hom</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom(;B) \to Hom(A,B)</annotation></semantics></math>. In the presence of these operations, a representing object is automatically a cartesian product; thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math> coincides with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</annotation></semantics></math>. Similarly, allowing contraction and weakening on the right makes the polycategory “right cocartesian”, which causes corepresenting objects to be coproducts and thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math> to coincide 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">\oplus</annotation></semantics></math>.</p> <p>On the other hand, if we allow “multi-composition” in our polycategory, i.e. we can compose a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A \to (B,C)</annotation></semantics></math> with one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">(B,C)\to D</annotation></semantics></math> to obtain a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">A\to D</annotation></semantics></math>, then our polycategory becomes a <a class="existingWikiWord" href="/nlab/show/PROP">PROP</a>, and representing and corepresenting objects must coincide; thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</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">\parr</annotation></semantics></math> become the same. This explains why <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\parr</annotation></semantics></math> has both a disjunctive and a conjunctive aspect. Of course, if in addition to multi-composition we have the left and right cartesian properties, then all four connectives coincide (including the categorical product and coproduct) and we have an <a class="existingWikiWord" href="/nlab/show/additive+category">additive category</a>.</p> <h2 id="game_semantics_2">Game semantics</h2> <p>We can interpret any proposition in linear logic as a game between two players: we and they. The overall rules are perfectly symmetric between us and them, although no individual game is. At any given moment in a game, exactly one of these four situations obtains: it is our turn, it is their turn, we have won, or they have won; the last two states continue forever afterwards (and the game is over). If it is our turn (or if they have won), then they are winning; if it is their turn (or if we have won), then we are winning. So there are two ways to win: because the game is over (and a winner has been decided), or because it is forever the other players’ turn (either because the other players have no move or because every move results in the other players’ turn again).</p> <p>This is a little complicated, but it's important in order to be able to distinguish the four constants:</p> <ul> <li>In <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>, it is their turn, but they have no moves; the game never ends, but we win.</li> <li>Dually, in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0}</annotation></semantics></math>, it is our turn, but we have no moves; the game never ends, but they win.</li> <li>In contrast, in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math>, the game ends immediately, and we have won.</li> <li>Dually, in <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>, the game ends immediately, and they have won.</li> </ul> <p>The binary operators show how to combine two games into a larger game:</p> <ul> <li>In <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mi>&</mi><mi>B</mi></mrow><annotation encoding="application/x-tex">A \& B</annotation></semantics></math>, it is their turn, and they must choose to play either <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> or <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>. Once they make their choice, play continues in the chosen game, with ending and winning conditions as in that game.</li> <li>Dually, in <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 \oplus B</annotation></semantics></math>, it is our turn, and we must choose to play either <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> or <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>. Once we make our choice, play continues in the chosen game, with ending and winning conditions as in that game.</li> <li>In <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 \otimes B</annotation></semantics></math>, play continues with both games in parallel. If it is our turn in either game, then it is our turn overall; if it is their turn in both games, then it is their turn overall. If either game ends, then play continues in the other game; if both games end, then the overall game ends. If we have won both games, then we have won overall; if they have won either game, then they have won overall.</li> <li>Dually, in <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 \parr B</annotation></semantics></math>, play continues with both games in parallel. If it is their turn in either game, then it is their turn overall; if it is our turn in both games, then it is our turn overall. If either game ends, then play continues in the other game; if both games end, then the overall game ends. If they have won both games, then they have won overall; if we have won either game, then we have won overall.</li> </ul> <p>So we can classify things as follows:</p> <ul> <li>In a conjunction, they choose what game to play; in a disjunction, we have control. Whoever has control must win at least one game to win overall.</li> <li>In an addition, one game must be played; in a multiplication, all games must be played.</li> </ul> <p>To further clarify the difference between <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><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math> (the additive and multiplicative versions of truth, both of which we win); consider <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">A \parr \top</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">A \parr \mathbf{1}</annotation></semantics></math>. In <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">A \parr \top</annotation></semantics></math>, it is always their move (since it is their move in <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>, hence their move in at least one game), so we win just as we win <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>. (In fact, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mo>⊤</mo><mo>≡</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">A \parr \top \equiv \top</annotation></semantics></math>.) However, in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⅋</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">A \parr \mathbf{1}</annotation></semantics></math>, the game <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math> ends immediately, so play continues as in <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>. We have won <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{1}</annotation></semantics></math>, so we only have to end the game to win overall, but there is no guarantee that this will happen. Indeed, in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>0</mn></mstyle><mo>⅋</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{0} \parr \mathbf{1}</annotation></semantics></math>, the game never ends and it is always our turn, so they win. (In <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo><mo>⅋</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">\bot \parr \mathbf{1}</annotation></semantics></math>, both games end immediately, and we win. In <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊗</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle></mrow><annotation encoding="application/x-tex">A \otimes \mathbf{1}</annotation></semantics></math>, we must win both games to win overall, so this reduces to <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>; indeed, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊗</mo><mstyle mathvariant="bold"><mn>1</mn></mstyle><mo>≡</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">A \otimes \mathbf{1} \equiv A</annotation></semantics></math>.)</p> <p>Negation is easy:</p> <ul> <li>To play <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>A</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">A^\perp</annotation></semantics></math>, simply swap roles and play <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>.</li> </ul> <p>There are several ways to think of the exponentials. As before, they have control in a conjunction, while we have control in a disjunction. Whoever has control of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!{A}</annotation></semantics></math> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">?{A}</annotation></semantics></math> chooses how many copies 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> to play and must win them all to win overall. There are many variations on whether the player in control can spawn new copies 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> or close old copies 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> prematurely, and whether the other player can play different moves in different copies (whenever the player in control plays the same moves).</p> <p>Other than the decisions made by the player in control of a game, all moves are made by transmitting resources. Ultimately, these come down to the propositional variables; in the game <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>, we must transmit a <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> to them, while they must transmit a <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> to us in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>p</mi> <mo>⊥</mo></msup></mrow><annotation encoding="application/x-tex">p^\perp</annotation></semantics></math>.</p> <p>A game is <strong>valid</strong> if we have a strategy to win (whether by putting the game in a state where we have won or by guaranteeing that it is forever their turn). The soundness and completeness of this interpretation is the theorem that <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> is a valid game if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\vdash A</annotation></semantics></math> is a valid sequent. (Recall that all questions of validity of sequents can be reduced to the validity of single propositions.)</p> <p>Game semantics for linear logic was first proposed by <a class="existingWikiWord" href="/nlab/show/Andreas+Blass">Andreas Blass</a>, in <a href="#Blass1992">Blass (1992)</a>. The semantics here is essentially the same as that proposed by Blass.</p> <h2 id="multiple_exponential_operators">Multiple exponential operators</h2> <p>Much as there are many <a class="existingWikiWord" href="/nlab/show/exponential+functions">exponential functions</a> (say from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℝ</mi></mrow><annotation encoding="application/x-tex">\mathbb{R}</annotation></semantics></math>), even though there is only one addition operation and one multiplication operation, so there can be many versions of the exponential operators <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> 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">?</annotation></semantics></math>. (However, there doesn't seem to be any analogue of the <a class="existingWikiWord" href="/nlab/show/logarithm">logarithm</a> to convert between them.)</p> <p>More precisely, if we add to the language of linear logic two more operators, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mo>′</mo></mrow><annotation encoding="application/x-tex">!'</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mo>′</mo></mrow><annotation encoding="application/x-tex">?'</annotation></semantics></math>, and postulate of them the same rules as for <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> 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">?</annotation></semantics></math>, we cannot prove that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi><mo>≡</mo><mo>!</mo><mo>′</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">!{A} \equiv !'{A}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>?</mo><mi>A</mi><mo>≡</mo><mo>?</mo><mo>′</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">?{A} \equiv ?'{A}</annotation></semantics></math>. In contrast, if we introduce <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">\&'</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo><mo>′</mo></mrow><annotation encoding="application/x-tex">\bot'</annotation></semantics></math>, etc, we <em>can</em> prove that the new operators are equivalent to the old ones.</p> <p>In terms of the categorial interpretation above, there may be many comonads <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>; it is not determined by the underlying <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>-autonomous category. In terms of game/resource semantics, there are several slightly different interpretations of the exponentials.</p> <p>One sometimes thinks of the exponentials as coming from infinitary applications of the other operations. For example:</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi><mo>≔</mo><mn>1</mn><mi>&</mi><mi>A</mi><mi>&</mi><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo stretchy="false">)</mo><mi>&</mi><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo stretchy="false">)</mo><mi>&</mi><mi>⋯</mi></mrow><annotation encoding="application/x-tex">!{A} \coloneqq 1 \& A \& (A \otimes A) \& (A \otimes A \otimes A) \& \cdots</annotation></semantics></math>,</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi><mo>≔</mo><mo stretchy="false">(</mo><mn>1</mn><mi>&</mi><mi>A</mi><mo stretchy="false">)</mo><mo>⊗</mo><mo stretchy="false">(</mo><mn>1</mn><mi>&</mi><mi>A</mi><mo stretchy="false">)</mo><mo>⊗</mo><mo stretchy="false">(</mo><mn>1</mn><mi>&</mi><mi>A</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>⋯</mi></mrow><annotation encoding="application/x-tex">!{A} \coloneqq (1 \& A) \otimes (1 \& A) \otimes (1 \& A) \otimes \cdots</annotation></semantics></math>,</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>!</mo><mi>A</mi><mo>≔</mo><mn>1</mn><mi>&</mi><mi>k</mi><mi>A</mi><mi>&</mi><mo stretchy="false">(</mo><msup><mi>k</mi> <mn>2</mn></msup><mo stretchy="false">/</mo><mn>2</mn><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo stretchy="false">)</mo><mi>&</mi><mo stretchy="false">(</mo><msup><mi>k</mi> <mn>3</mn></msup><mo stretchy="false">/</mo><mn>6</mn><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo>⊗</mo><mi>A</mi><mo stretchy="false">)</mo><mi>&</mi><mi>⋯</mi></mrow><annotation encoding="application/x-tex">!{A} \coloneqq 1 \& k A \& (k^2/2) (A \otimes A) \& (k^3/6) (A \otimes A \otimes A) \& \cdots</annotation></semantics></math> (which is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi mathvariant="normal">e</mi> <mrow><mi>k</mi><mi>A</mi></mrow></msup></mrow><annotation encoding="application/x-tex">\mathrm{e}^{k A}</annotation></semantics></math> in an appropriate sense), where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">n A</annotation></semantics></math> means an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-fold additive conjunction <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mi>&</mi><mi>⋯</mi><mi>&</mi><mi>A</mi></mrow><annotation encoding="application/x-tex">A \& \cdots \& A</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a>, and we pretend that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math> is a positive number such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>k</mi> <mi>n</mi></msup><mo stretchy="false">/</mo><mrow><mi>n</mi><mo>!</mo></mrow></mrow><annotation encoding="application/x-tex">k^n/{n!}</annotation></semantics></math> is always a natural number (which of course is impossible).</li> </ul> <p>All of these justify the rules for the exponentials, so again we see that there may be many ways to satisfy these rules.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/bounded+linear+logic">bounded linear logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/affine+logic">affine logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/coherence+space">coherence space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/game+semantics">game semantics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a></p> </li> <li> <p><span class="newWikiWord">light logic<a href="/nlab/new/light+logic">?</a></span></p> <ul> <li><span class="newWikiWord">light linear logic<a href="/nlab/new/light+linear+logic">?</a></span></li> <li><a class="existingWikiWord" href="/nlab/show/soft+linear+logic">soft linear logic</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/linearly+distributive+category">linearly distributive category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/transcendental+syntax">transcendental syntax</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+projections">propositions as projections</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/substructural+logic">substructural logic</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/structural+rule">structural rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/affine+logic">affine logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/relevance+logic">relevance logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/bunched+logic">bunched logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/separation+logic">separation logic</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/scale">scale</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Heyting+scale">Heyting scale</a></li> <li><a class="existingWikiWord" href="/nlab/show/minor+scale">minor scale</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/linear+lambda-calculus">linear lambda-calculus</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/antithesis+interpretation">antithesis interpretation</a></p> </li> </ul> <div> <table><thead><tr><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math>symbol<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math></th><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math>in <a class="existingWikiWord" href="/nlab/show/logic">logic</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math></th></tr></thead><tbody><tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\in</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/element">element</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace><mo>:</mo></mrow><annotation encoding="application/x-tex">\,:</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/type">typing</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">=</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\vdash</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/entailment">entailment</a> / <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/true">true</a> / <a class="existingWikiWord" href="/nlab/show/top">top</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\bot</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/false">false</a> / <a class="existingWikiWord" href="/nlab/show/bottom">bottom</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\Rightarrow</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\Leftrightarrow</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\not</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\neq</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a> of <a class="existingWikiWord" href="/nlab/show/equality">equality</a> / <a class="existingWikiWord" href="/nlab/show/apartness">apartness</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\notin</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a> of <a class="existingWikiWord" href="/nlab/show/element">element</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>¬</mo></mrow><annotation encoding="application/x-tex">\not \not</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/double+negation">negation of negation</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\exists</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\forall</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\wedge</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\vee</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+disjunction">logical disjunction</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><strong>symbol</strong></td><td style="text-align: left;"><strong>in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</strong></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\to</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (<a class="existingWikiWord" href="/nlab/show/implication">implication</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\times</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/product+type">product type</a> (<a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace" rspace="0em">+</mo></mrow><annotation encoding="application/x-tex">+</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a> (<a class="existingWikiWord" href="/nlab/show/false">false</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a> (<a class="existingWikiWord" href="/nlab/show/true">true</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">=</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> (<a class="existingWikiWord" href="/nlab/show/equality">equality</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\simeq</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> (<a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo></mrow><annotation encoding="application/x-tex">\sum</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo></mrow><annotation encoding="application/x-tex">\prod</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (<a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a>)</td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><strong>symbol</strong></td><td style="text-align: left;"><strong>in <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></strong></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\multimap</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/linear+implication">linear implication</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\otimes</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\oplus</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/additive+disjunction">additive disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/additive+conjunction">additive conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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">\invamp</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/multiplicative+disjunction">multiplicative disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mo>!</mo></mrow><annotation encoding="application/x-tex">\;!</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/exponential+conjunction">exponential conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mo>?</mo></mrow><annotation encoding="application/x-tex">\;?</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</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><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/exponential+disjunction">exponential disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> </tbody></table> </div> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>The original article:</p> <ul> <li id="Girard1987"><a class="existingWikiWord" href="/nlab/show/Jean-Yves+Girard">Jean-Yves Girard</a>, <em>Linear logic</em>, Theoretical Computer Science <strong>50</strong> 1 (1987) [<a href="https://doi.org/10.1016/0304-3975(87)90045-4">doi:10.1016/0304-3975(87)90045-4</a>, <a href="http://iml.univ-mrs.fr/~girard/linear.pdf">pdf</a>]</li> </ul> <p>Review:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Anne+Sjerp+Troelstra">Anne Sjerp Troelstra</a>, <em>Lectures on Linear Logic</em>, CSLI Lectures notes <strong>29</strong> (1992) [<a href="https://web.stanford.edu/group/cslipublications/cslipublications/site/0937073776.shtml">ISBN:0937073776</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Frank+Pfenning">Frank Pfenning</a>, <em>Linear Logic</em>, CSLI Lecture Notes <strong>29</strong> (1998) [<a href="https://www.cs.cmu.edu/~fp/courses/98-linear/handouts/notes.pdf">pdf</a>, <a href="https://www.cs.cmu.edu/~fp/courses/98-linear/handouts.html">webpage</a>, <a class="existingWikiWord" href="/nlab/files/Pfenning-LinearLogic98.pdf" title="pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Jean-Yves+Girard">Jean-Yves Girard</a>, <em>Linear logic, its syntax and semantics</em> (2006) [<a href="http://www.cs.brandeis.edu/~cs112/2006-cs112/docs/girard-intro.pdf">pdf</a>]</p> </li> <li id="Girard11"> <p><a class="existingWikiWord" href="/nlab/show/Jean-Yves+Girard">Jean-Yves Girard</a>, part III of <em><a class="existingWikiWord" href="/nlab/show/Lectures+on+Logic">Lectures on Logic</a></em>, European Mathematical Society 2011</p> </li> <li id="MihályiNovitzká13"> <p>Daniel Mihályi, Valerie Novitzká, <em>What about Linear Logic in Computer Science?</em>, Acta Polytechnica Hungarica <strong>10</strong> 4 (2013) 147-160 [<a href="http://acta.uni-obuda.hu/Mihalyi_Novitzka_42.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/MihalyiNovitzka-LinearLogic.pdf" title="pdf">pdf</a>]</p> </li> </ul> <p>and making explicit the <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of linear logic in the category <a class="existingWikiWord" href="/nlab/show/FinDimVect">FinDimVect</a> of <a class="existingWikiWord" href="/nlab/show/finite-dimensional+vector+spaces">finite-dimensional vector spaces</a>:</p> <ul> <li id="Pratt93"> <p><a class="existingWikiWord" href="/nlab/show/Vaughan+Pratt">Vaughan Pratt</a>, <em>The second calculus of binary relations</em>, Mathematical Foundations of Computer Science 1993. MFCS 1993, Lecture Notes in Computer Science <strong>711</strong>, Springer (1993) [<a href="https://doi.org/10.1007/3-540-57182-5_9">doi:10.1007/3-540-57182-5_9</a>]</p> <blockquote> <p>“Linear logic is seen in its best light as the realization of the <a class="existingWikiWord" href="/nlab/show/Curry-Howard+isomorphism">Curry-Howard isomorphism</a> for <a class="existingWikiWord" href="/nlab/show/linear+algebra">linear algebra</a>”</p> </blockquote> </li> <li id="ValironZdancewic14"> <p><a class="existingWikiWord" href="/nlab/show/Beno%C3%AEt+Valiron">Benoît Valiron</a>, <a class="existingWikiWord" href="/nlab/show/Steve+Zdancewic">Steve Zdancewic</a>, <em>Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi</em>, in: <em>Proc. of ICTAC’14</em>, Lecture Notes in Computer Science <strong>8687</strong>, Springer (2014) 442-459 [<a href="https://arxiv.org/abs/1406.1310">arXiv:1406.1310</a>, <a href="https://doi.org/10.1007/978-3-319-10882-7_26">doi:10.1007/978-3-319-10882-7_26</a>, slides:<a href="https://www.cs.bham.ac.uk/~drg/bll/steve.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Zdancewic-LinearLogicAlgebra.pdf" title="pdf">pdf</a>]</p> </li> <li id="Murfet14"> <p><a class="existingWikiWord" href="/nlab/show/Daniel+Murfet">Daniel Murfet</a>, <em>Logic and linear algebra: an introduction</em> [<a href="http://arxiv.org/abs/1407.2650">arXiv:1407.2650</a>]</p> </li> </ul> <p>following a remark in section 2.4.2 of <a href="#HylandSchalk03">Hyland & Schalk (2003)</a>.</p> <ul> <li id="HylandSchalk03"><a class="existingWikiWord" href="/nlab/show/Martin+Hyland">Martin Hyland</a>, Andrea Schalk, <em>Glueing and orthogonality for models of linear logic</em>, Theoretical Computer Science <strong>294</strong> 1–2 (2003) 183-231 [<a href="https://doi.org/10.1016/S0304-3975(01)00241-9">doi:10.1016/S0304-3975(01)00241-9</a>]</li> </ul> <p>The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of linear logic in general <a class="existingWikiWord" href="/nlab/show/star-autonomous+categories">star-autonomous categories</a> originally appeared in</p> <ul> <li id="Seely"> <p><a class="existingWikiWord" href="/nlab/show/R.+A.+G.+Seely">R. A. G. Seely</a>, <em>Linear logic, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">\ast</annotation></semantics></math>-autonomous categories and cofree coalgebras</em>, in <em>Categories in Computer Science and Logic</em>, Contemporary Mathematics <strong>92</strong> (1989) [<a class="existingWikiWord" href="/nlab/files/SeelyLinearLogic.pdf" title="pdf">pdf</a>, <a href="http://www.math.mcgill.ca/rags/nets/llsac.ps.gz">ps.gz</a>, <a href="https://bookstore.ams.org/conm-92">ISBN:978-0-8218-5100-5</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael+Barr">Michael Barr</a>, <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">\ast</annotation></semantics></math>-Autonomous categories and linear logic</em>, Math. Structures Comp. Sci. <strong>1</strong> 2 (1991) 159–178 [<a href="https://doi.org/10.1017/S0960129500001274">doi:10.1017/S0960129500001274</a>, <a href="https://www.math.mcgill.ca/barr/papers/scatll.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Barr-AutomomousCatAndLinLogic.pdf" title="pdf">pdf</a>]</p> </li> </ul> <p>and for the special case of <a class="existingWikiWord" href="/nlab/show/quantales">quantales</a> in</p> <ul> <li id="Yetter90"><a class="existingWikiWord" href="/nlab/show/David+Yetter">David Yetter</a>, <em>Quantales and (noncommutative) linear logic</em>, Journal of Symbolic Logic 55 (1990), 41–64.</li> </ul> <p>and further in view of the <a class="existingWikiWord" href="/nlab/show/Chu+construction">Chu construction</a>:</p> <ul> <li id="Pratt93"> <p><a class="existingWikiWord" href="/nlab/show/Vaughan+Pratt">Vaughan Pratt</a>, <em>The second calculus of binary relations</em>, Mathematical Foundations of Computer Science 1993. MFCS 1993, Lecture Notes in Computer Science <strong>711</strong>, Springer (1993) [<a href="https://doi.org/10.1007/3-540-57182-5_9">doi:10.1007/3-540-57182-5_9</a>]</p> </li> <li id="Pratt99"> <p><a class="existingWikiWord" href="/nlab/show/Vaughan+Pratt">Vaughan Pratt</a>, <em>Chu Spaces</em> (1999) [<a href="http://boole.stanford.edu/pub/coimbra.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Pratt-ChuSpaces.pdf" title="pdf">pdf</a>]</p> </li> </ul> <p>The more general case of of multiplicative intuitionistic linear logic interpreted more generally in <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+categories">symmetric monoidal categories</a> was systematically developed in</p> <ul> <li id="Szabo78">M.E. Szabo, <em>Algebra of Proofs</em>, Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland.</li> </ul> <p>(that was before Girard introduced the “linear” terminology).</p> <p>More recent articles exploring this include</p> <ul> <li id="dePaiva89"> <p><a class="existingWikiWord" href="/nlab/show/Valeria+de+Paiva">Valeria de Paiva</a>, <em>The Dialectica Categories</em>, <em>Contemporary Mathematics</em> 92, 1989. (<a href="http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf">web</a>)</p> </li> <li id="Blute91"> <p><a class="existingWikiWord" href="/nlab/show/Richard+Blute">Richard Blute</a>, <em>Linear logic, coherence, and dinaturality</em>, Dissertation, University of Pennsylvania 1991, published in Theoretical Computer Science archive</p> <p>Volume 115 Issue 1, July 5, 1993 Pages 3–41</p> </li> <li id="BentonBiermanPaivaHyland92"> <p><a class="existingWikiWord" href="/nlab/show/Nick+Benton">Nick Benton</a>, <a class="existingWikiWord" href="/nlab/show/Gavin+Bierman">Gavin Bierman</a>, <a class="existingWikiWord" href="/nlab/show/Valeria+de+Paiva">Valeria de Paiva</a>, <a class="existingWikiWord" href="/nlab/show/Martin+Hyland">Martin Hyland</a>, <em>Term assignments for intuitionistic linear logic</em>. Technical report 262, Cambridge 1992 (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8666">citeseer</a>, <a href="http://www.cs.bham.ac.uk/~vdp/publications/tr262.ps">ps</a>)</p> </li> <li id="HylandPaiva93"> <p><a class="existingWikiWord" href="/nlab/show/Martin+Hyland">Martin Hyland</a>, <a class="existingWikiWord" href="/nlab/show/Valeria+de+Paiva">Valeria de Paiva</a>, <em>Full Intuitionistic Linear Logic</em> (extended abstract). Annals of Pure and Applied Logic, 64(3), pp. 273–291, 1993. (<a href="http://www.cs.bham.ac.uk/~vdp/publications/fill.pdf">pdf</a>)</p> </li> <li id="Bierman95"> <p>G. Bierman, <em>On Intuitionistic Linear Logic</em> PhD thesis, Computing Laboratory, University of Cambridge, 1995 (<a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.114.588&rep=rep1&type=pdf">pdf</a>)</p> </li> <li id="Barber97"> <p>Andrew Graham Barber, <em>Linear Type Theories, Semantics and Action Calculi</em>, PhD thesis, Edinburgh 1997 (<a href="http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/&#8206;">web</a>, <a href="http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/ECS-LFCS-97-371.pdf">pdf</a>)</p> </li> </ul> <p>This is reviewed/further discussed in</p> <ul> <li id="Schalk04"> <p>Andrea Schalk, <em>What is a categorical model for linear logic?</em> (<a href="http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf">pdf</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Richard+Blute">Richard Blute</a>, Philip Scott, <em>Category theory for linear logicians</em>, 2004 (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.6250">citeseer</a>)</p> </li> <li id="Melliès02"> <p><a class="existingWikiWord" href="/nlab/show/Paul-Andr%C3%A9+Melli%C3%A8s">Paul-André Melliès</a>, <em>Categorical models of linear logic revisited</em> (2002) [<a href="https://hal.science/hal-00154229">hal:00154229</a>]</p> </li> <li id="Melliès09"> <p><a class="existingWikiWord" href="/nlab/show/Paul-Andr%C3%A9+Melli%C3%A8s">Paul-André Melliès</a>, <em>Categorical semantics of linear logic</em>, in <em><a href="https://smf.emath.fr/publications/modeles-interactifs-de-calcul-et-de-comportement-de-programme">Interactive models of computation and program behaviour</a></em>, Panoramas et synthèses <strong>27</strong> (2009) 1-196 [<a href="https://smf.emath.fr/publications/semantique-categorielle-de-la-logique-lineaire">web</a>, <a href="https://www.irif.fr/~mellies/papers/panorama.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Mellies-CategoricalSemanticsLinear.pdf" title="pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Paul-Andr%C3%A9+Melli%C3%A8s">Paul-André Melliès</a>, <em>A Functorial Excursion Between Algebraic Geometry and Linear Logic</em>, in 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ‘22), Haifa, Israel (2022). ACM, New York [<a href="https://doi.org/10.1145/3531130.3532488">doi:10.1145/3531130.3532488</a>, <a href="https://www.irif.fr/~mellies//papers/functorial-excursion.pdf">pdf</a>]</p> </li> </ul> <p>The relation of dual intuitionistic linear logic 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">\pi</annotation></semantics></math>-calculus is given in</p> <ul> <li>Luis Caires, <a class="existingWikiWord" href="/nlab/show/Frank+Pfenning">Frank Pfenning</a>. <em>Session Types as Intuitionistic Linear Propositions</em>.</li> </ul> <p>Noncommutative linear logic is discussed for instance in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Richard+Blute">Richard Blute</a>, F. Lamarche, Paul Ruet, <em>Entropic Hopf algebras and models of non-commutative logic</em>, Theory and Applications of Categories, Vol. 10, No. 17, 2002, pp. 424–460. (<a href="http://www.emis.ams.org/journals/TAC/volumes/10/17/10-17.pdf">pdf</a>)</li> </ul> <p>Further discussion of <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a> is for instance in</p> <ul> <li> <p><em>Chapter 7, Linear type theory</em> <a href="http://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf">pdf</a></p> </li> <li> <p>Anders Schack-Nielsen, Carsten Schürmann, <em>Linear contextual modal type theory</em> <a href="http://www.itu.dk/~carsten/papers/lcmtt.pdf">pdf</a></p> </li> </ul> <p>See also</p> <ul> <li id="Blass1992"> <p><a class="existingWikiWord" href="/nlab/show/Andreas+Blass">Andreas Blass</a>, 1992. <em>A game semantics for linear logic</em>. <em>Annals of Pure and Applied Logic</em> 56: 183–220. 1992.</p> </li> <li> <p>The <a href="https://secure.wikimedia.org/wikipedia/en/wiki/Linear_logic">article</a> on the English Wikipedia has good summaries of the meanings of the logical operators and of the commonly studied <a class="existingWikiWord" href="/nlab/show/fragments">fragments</a>.</p> </li> </ul> <p>Discussion of <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a> without <a class="existingWikiWord" href="/nlab/show/units">units</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Robin+Houston">Robin Houston</a>, <em>Linear Logic without Units</em> (<a href="http://arxiv.org/abs/1305.2231">arXiv:1305.2231</a>)</li> </ul> <p>Discussion of <a class="existingWikiWord" href="/nlab/show/inductive+types">inductive types</a> in the context of <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>:</p> <ul> <li>Stéphane Gimenez, <em>Towards Generic Inductive Constructions inSystems of Nets</em> [<a href="http://www.imn.htwk-leipzig.de/WST2013/papers/paper_16.pdf">pdf</a>]</li> </ul> <p>The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a>of differential linear logic is introduced in:</p> <ul> <li id="Blute-Cockett-Seely06"><a class="existingWikiWord" href="/nlab/show/Richard+Blute">Richard Blute</a>, <a class="existingWikiWord" href="/nlab/show/Robin+Cockett">Robin Cockett</a>, <a class="existingWikiWord" href="/nlab/show/Robert+Seely">Robert Seely</a>, <em>Differential Categories</em>, Mathematical structures in computer science 16.6 (2006): 1049–1083. (<a href="https://pdfs.semanticscholar.org/82b0/f9533b451d174f407b35e1c39e2376138ac2.pdf">pdf</a>)</li> </ul> <p>The antithesis interpretation is</p> <ul> <li id="Shulman2022"><a class="existingWikiWord" href="/nlab/show/Michael+Shulman">Michael Shulman</a>, <em>Affine logic for constructive mathematics</em>. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (<a href="https://doi.org/10.1017/bsl.2022.28">doi:10.1017/bsl.2022.28</a>, <a href="https://arxiv.org/abs/1805.07518">arXiv:1805.07518</a>.</li> </ul> <h3 id="in_relation_to_quantum_computing">In relation to quantum computing</h3> <p>Discussion of application of linear logic to <a class="existingWikiWord" href="/nlab/show/quantum+logic">quantum logic</a>, <a class="existingWikiWord" href="/nlab/show/quantum+computing">quantum computing</a> and generally to <a class="existingWikiWord" href="/nlab/show/quantum+physics">quantum physics</a> (See also at <em><a class="existingWikiWord" href="/nlab/show/quantum+programming+languages">quantum programming languages</a></em>):</p> <ul> <li id="Pratt92"> <p><a class="existingWikiWord" href="/nlab/show/Vaughan+Pratt">Vaughan Pratt</a>, <em>Linear logic for generalized quantum mechanics</em>, in Proc. of <em>Workshop on Physics and Computation (PhysComp’92)</em> (<a href="http://boole.stanford.edu/pub/ql.pdf">pdf</a>, <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.7817">web</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Beno%C3%AEt+Valiron">Benoît Valiron</a>, <em>A functional programming language for quantum computation with classical control</em>, MSc thesis, University of Ottawa (2004) [<a href="http://dx.doi.org/10.20381/ruor-18372">doi:10.20381/ruor-18372</a>, <a href="https://ruor.uottawa.ca/bitstream/10393/26790/1/MR01625.PDF">pdf</a>]</p> </li> <li id="SelingerValiron04"> <p><a class="existingWikiWord" href="/nlab/show/Peter+Selinger">Peter Selinger</a>, <a class="existingWikiWord" href="/nlab/show/Beno%C3%AEt+Valiron">Benoît Valiron</a>, <em>A lambda calculus for quantum computation with classical control</em>, Proc. of TLCA 2005 [<a href="https://arxiv.org/abs/cs/0404056">arXiv:cs/0404056</a>, <a href="https://doi.org/10.1007/11417170_26">doi:10.1007/11417170_26</a>]</p> </li> <li id="SelingerValiron09"> <p><a class="existingWikiWord" href="/nlab/show/Peter+Selinger">Peter Selinger</a>, <a class="existingWikiWord" href="/nlab/show/Beno%C3%AEt+Valiron">Benoît Valiron</a>, <em>Quantum Lambda Calculus</em>, in: <em>Semantic Techniques in Quantum Computation</em>, Cambridge University Press (2009) 135-172 [<a href="https://doi.org/10.1017/CBO9781139193313.005">doi:10.1017/CBO9781139193313.005</a>, <a href="https://www.mscs.dal.ca/~selinger/papers/qlambdabook.pdf">pdf</a>]</p> <blockquote> <p>(cf. <em><a class="existingWikiWord" href="/nlab/show/quantum+lambda-calculus">quantum lambda-calculus</a></em>)</p> </blockquote> </li> <li id="Baez04"> <p><a class="existingWikiWord" href="/nlab/show/John+Baez">John Baez</a>, <em>Quantum Quandaries: a Category-Theoretic Perspective</em>, in D. Rickles et al. (ed.) <em>The structural foundations of quantum gravity</em>, Clarendon Press (2006) 240-265 [<a href="https://arxiv.org/abs/quant-ph/0404040">arXiv:quant-ph/0404040</a>, <a href="https://global.oup.com/academic/product/the-structural-foundations-of-quantum-gravity-9780199269693">ISBN:9780199269693</a>]</p> </li> <li id="AbramskyDuncan06"> <p><a class="existingWikiWord" href="/nlab/show/Samson+Abramsky">Samson Abramsky</a>, <a class="existingWikiWord" href="/nlab/show/Ross+Duncan">Ross Duncan</a>, <em>A Categorical Quantum Logic</em>, Mathematical Structures in Computer Science <strong>16</strong> 3 (2006) [<a href="http://arxiv.org/abs/quant-ph/0512114">arXiv:quant-ph/0512114</a>, <a href="https://doi.org/10.1017/S0960129506005275">doi:10.1017/S0960129506005275</a>]</p> </li> <li id="Duncan06"> <p><a class="existingWikiWord" href="/nlab/show/Ross+Duncan">Ross Duncan</a>, <em>Types for quantum computation</em>, 2006 (<a href="http://www.cs.ox.ac.uk/files/2425/Types%20for%20Quantum%20Computation.pdf">pdf</a>)</p> </li> <li id="DalLagoFaggian12"> <p><a class="existingWikiWord" href="/nlab/show/Ugo+Dal+Lago">Ugo Dal Lago</a>, <a class="existingWikiWord" href="/nlab/show/Claudia+Faggian">Claudia Faggian</a>, <em>On Multiplicative Linear Logic, Modality and Quantum Circuits</em>, EPTCS 95 (2012) 55-66 [<a href="http://arxiv.org/abs/1210.0613">arXiv:1210.0613</a>, <a href="https://doi.org/10.4204/EPTCS.95.6">doi:10.4204/EPTCS.95.6</a>]</p> </li> <li id="Staton15"> <p><a class="existingWikiWord" href="/nlab/show/Sam+Staton">Sam Staton</a>, <em>Algebraic Effects, Linearity, and Quantum Programming Languages</em>, POPL ‘15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo></mrow><annotation encoding="application/x-tex">[</annotation></semantics></math><a href="https://doi.org/10.1145/2676726.2676999">doi:10.1145/2676726.2676999</a>, <a href="http://www.cs.ox.ac.uk/people/samuel.staton/papers/popl2015.pdf">pdf</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">]</annotation></semantics></math></p> </li> <li id="CCGP09"> <p>Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto Giuntini and Francesco Paoli, section 9 of <em>Quantum Logic and Nonclassical Logics</em>, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) <em>Handbook of Quantum Logic and Quantum Structures: Quantum Logic</em>, 2009 North Holland</p> </li> </ul> <p>Application of linear logic to <a class="existingWikiWord" href="/nlab/show/matrix+factorization">matrix factorization</a> in <a class="existingWikiWord" href="/nlab/show/Landau%E2%80%93Ginzburg+models">Landau–Ginzburg models</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Daniel+Murfet">Daniel Murfet</a>, <em>The cut operation on matrix factorisations</em>, Journal of Pure and Applied Algebra <p><strong>222</strong> 7 (2018) 1911-1955 [<a href="https://arxiv.org/abs/1402.4541">arXiv:1402.4541</a>, <a href="https://doi.org/10.1016/j.jpaa.2017.08.014">doi:10.1016/j.jpaa.2017.08.014</a>]</p> </li> </ul> <p>Relating linear logic to <a class="existingWikiWord" href="/nlab/show/quantum+error+correction">quantum error correction</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Daniel+Murfet">Daniel Murfet</a>, William Troiani, <em>Linear Logic and Quantum Error Correcting Codes</em> [<a href="https://arxiv.org/abs/2405.19051">arXiv:2405.19051</a>]</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on September 6, 2024 at 20:04:14. See the <a href="/nlab/history/linear+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/linear+logic" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/7830/#Item_43">Discuss</a><span class="backintime"><a href="/nlab/revision/linear+logic/133" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/linear+logic" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/linear+logic" accesskey="S" class="navlink" id="history" rel="nofollow">History (133 revisions)</a> <a href="/nlab/show/linear+logic/cite" style="color: black">Cite</a> <a href="/nlab/print/linear+logic" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/linear+logic" id="view_source" rel="nofollow">Source</a> </div> </div> <!-- Content --> </div> <!-- Container --> </body> </html>