CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> classical logic in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> classical 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/7720/#Item_13" 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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#details'>Details</a></li> <li><a href='#classical_propositional_logic'>Classical propositional logic</a></li> <li><a href='#related_concepts'>Related concepts</a></li> </ul> </div> <h2 id="Idea">Idea</h2> <p>There are many systems of <em><a class="existingWikiWord" href="/nlab/show/formal+logic">formal logic</a></em>. By “classical logic” one broadly refers to those such systems which reflect the kind of logic as understood, quite literally, by the classics, say starting with <a href="excluded+middle#AristotleMetaphysics">Aristotle, Metaphysics 1011b24</a>. If you have never heard of any alternative system of logic, then classical logic is just the kind of logic that you have heard about.</p> <p>There is some variance in what exactly counts as classical and as non-classical in <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, but one main characteristic of classical logic is its use of the <em><a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a></em>. Informally this says that every <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> is either <a class="existingWikiWord" href="/nlab/show/true">true</a> or <a class="existingWikiWord" href="/nlab/show/false">false</a>. (Slightly more carefully it says that for any proposition <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>, either it or its <a class="existingWikiWord" href="/nlab/show/negation">negation</a> is true, where the ‘or’ is to be read in an ‘internal’ sense, i.e., as a formal <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>∨</mo><mo>¬</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">P \vee \neg P</annotation></semantics></math>.)</p> <p>It is the apparent self-evidence of this principle of excluded middle that made people take it for granted for a long period of human civilization, so that it became “classical”.</p> <p>One consequence of the <a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a> in classical logic is the possibility to obtain <a class="existingWikiWord" href="/nlab/show/proof">proof</a> of a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> by showing that its <a class="existingWikiWord" href="/nlab/show/negation">negation</a> is <a class="existingWikiWord" href="/nlab/show/false">false</a> (<a class="existingWikiWord" href="/nlab/show/proof+by+contradiction">proof by contradiction</a>). Evident as this may superficially seem, it has the noteworthy consequence that one may for instance prove <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existence</a> of mathematical objects without having any way to actually construct an example.</p> <p>This “non-constructive” nature of classical logic eventually led people to consider alternative and hence <em>non-classical</em> systems of logic, such as <a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive logic</a>/<a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>, where the <a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a>, and possibly other principle of classical logic, are not considered by default. There is still a close relation between classical and <a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive logic</a>. For example a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> is provable in classical logic precisely if its <a class="existingWikiWord" href="/nlab/show/double+negation">double negation</a> is provable in <a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive logic</a> (“<a class="existingWikiWord" href="/nlab/show/double+negation+translation">double negation translation</a>”).</p> <p>Other considerations such as the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of <a class="existingWikiWord" href="/nlab/show/categories">categories</a> also led to constructive/intuitionistic logics. More recently, other “nonclassical” logics such as <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a>, <a class="existingWikiWord" href="/nlab/show/paraconsistent+logic">paraconsistent logic</a>, <a class="existingWikiWord" href="/nlab/show/relevance+logic">relevance logic</a>, <a class="existingWikiWord" href="/nlab/show/quantum+logic">quantum logic</a>, and so on have also gained prominence.</p> <p>There are other principles that are often associated with classical logic, which still seemed self-evident at a time, but maybe less so than the principle of excluded middle. One such is the <a class="existingWikiWord" href="/nlab/show/set+theory">set-theoretic</a> <em><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></em> or one of its equivalent incarnations, such as <a class="existingWikiWord" href="/nlab/show/Zorn%27s+lemma">Zorn's lemma</a>. The presently most popular formal <a class="existingWikiWord" href="/nlab/show/foundation+of+mathematics">foundation of mathematics</a> via the <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, called <em><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></em>, includes both the <a class="existingWikiWord" href="/nlab/show/principle+of+excluded+middle">principle of excluded middle</a> as well as the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. In this form classical logic serves as the foundation for <em><a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a></em>.</p> <h2 id="details">Details</h2> <p>Classical logic is the form of <a class="existingWikiWord" href="/nlab/show/logic">logic</a> usually accepted and taught as standard among working mathematicians, and traced back (at least) to Aristotle. Some particular features that distinguish classical logic are (perhaps not a complete list):</p> <ul> <li>a <a class="existingWikiWord" href="/nlab/show/distributive+lattice">distributive lattice</a> of logical operations (<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>);</li> <li>the <a class="existingWikiWord" href="/nlab/show/structural+rule">structural rule</a>s of weakening, contraction, and (where meaningful) exchange;</li> <li>an involutory <a class="existingWikiWord" href="/nlab/show/negation">negation</a>.</li> </ul> <p>In contrast, <a class="existingWikiWord" href="/nlab/show/minimal+logic">minimal</a>, <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic</a>, and (some forms of) <a class="existingWikiWord" href="/nlab/show/paraconsistent+logic">paraconsistent</a> logics have the distributive lattice and the structural rules but no involutory negation. On the other hand, <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a> (at least, “classical” linear logic) and (other forms of) paraconsistent logic have logical operations with at least some distributive properties and an involutory negation, but lack some structural rules. Then again, <a class="existingWikiWord" href="/nlab/show/quantum+logic">quantum logic</a> and (yet other forms of) paraconsistent logic have the structural rules and the involutory negation, but lack any sort of distributivity.</p> <p>In <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> (and in the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of mathematics generally), it is intuitionistic logic that is most often contrasted to classical logic; the difference is given by the law of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, which holds classically but not intuitionistically.</p> <h2 id="classical_propositional_logic">Classical propositional logic</h2> <p>Before describing what makes a <a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a> ‘classical’, let us quickly recall what propositional logic is in the first place.</p> <p>In general, a (deductive) <a class="existingWikiWord" href="/nlab/show/logic">logic</a> specifies rules of <a class="existingWikiWord" href="/nlab/show/syntax">syntax</a> for forming well-formed <a class="existingWikiWord" href="/nlab/show/formulas">formulas</a> which can be considered as assertions, and rules of inference for deriving one formula (called a ‘conclusion’) from other formulas (called ‘premises’), in such a way that truth of the conclusion follows on the assumption of truth of the premises. In short, a <a class="existingWikiWord" href="/nlab/show/formal+logic">formal logic</a> specifies a mode of reasoning that is considered valid for a particular mathematical context.</p> <p>In <a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a>, one forms a formula by applying basic logical operations 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">\wedge</annotation></semantics></math> (’<a class="existingWikiWord" href="/nlab/show/logical+conjunction">and</a>’), <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∨</mo></mrow><annotation encoding="application/x-tex">\vee</annotation></semantics></math> (’<a class="existingWikiWord" href="/nlab/show/logical+disjunction">or</a>’), 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">\Rightarrow</annotation></semantics></math> (’<a class="existingWikiWord" href="/nlab/show/implication">implies</a>’) to simpler formulas. The simplest formulas are called atomic formulas, and usually take the form of an <a class="existingWikiWord" href="/nlab/show/equation">equation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>=</mo><mi>t</mi></mrow><annotation encoding="application/x-tex">s = t</annotation></semantics></math> between two <a class="existingWikiWord" href="/nlab/show/terms">terms</a> (and underneath there are rules for term formation as well), or something like <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><msub><mi>a</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>a</mi> <mi>n</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(a_1, \ldots, a_n)</annotation></semantics></math> where <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> stands for some basic relation (between terms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" 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></mrow><annotation encoding="application/x-tex">a_1, \ldots, a_n</annotation></semantics></math>) belonging to whatever language one is working with. A standard list of <em>propositional</em> operations would be</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo><mo>,</mo><mo>∨</mo><mo>,</mo><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\wedge, \vee, \Rightarrow</annotation></semantics></math> (binary operations), <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo></mrow><annotation encoding="application/x-tex">\neg</annotation></semantics></math> (‘not’, an unary operator), and <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">\top, \bot</annotation></semantics></math> (‘true’ and ‘false’, basic logical constants or nullary operators).</li> </ul> <p>Missing from propositional logic <em>per se</em> are <a class="existingWikiWord" href="/nlab/show/quantifiers">quantifiers</a> 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">\exists</annotation></semantics></math> (<a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a>) 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> (<a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a>), which properly speaking belong to <a class="existingWikiWord" href="/nlab/show/predicate+logic">predicate logic</a>. (One way of thinking about propositional logic is that it treats formulas as assertions “all of the same type”, whereas quantifiers allow one to shift between classes of assertions of one type to assertions of another type.)</p> <p>As we said, there are also rules of inference. There are various styles in which these are presented, such as <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a> or <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>. But a simple example might look like this:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>P</mi><mo>∧</mo><mi>Q</mi></mrow><mi>P</mi></mfrac></mrow><annotation encoding="application/x-tex">\frac{P \wedge Q}{P}</annotation></semantics></math></div> <p>(“from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>∧</mo><mi>Q</mi></mrow><annotation encoding="application/x-tex">P \wedge Q</annotation></semantics></math> we may infer <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>”). This might also be written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>∧</mo><mi>Q</mi><mo>⊢</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">P \wedge Q \vdash P</annotation></semantics></math> (“pronounced <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>∧</mo><mi>Q</mi></mrow><annotation encoding="application/x-tex">P \wedge Q</annotation></semantics></math> entails <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>”), thought of as asserting a relation between propositions called entailment. Two of the universal rules of propositional logic (whether classical or intuitionistic or quantum or whatever) is that the entailment relation should be <a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexive</a> and <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a>: the rules of inference allow an entailment <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 any formula <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 if they allow entailments <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>C</mi></mrow><annotation encoding="application/x-tex">B \vdash C</annotation></semantics></math>, then they allow <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⊢</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">A \vdash C</annotation></semantics></math>.</p> <p>Thus, in a propositional logic, formulas together with the entailment relation that is provided for by the rules of inference form a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a>. Sometimes one goes a little further: in situations where one can derive <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>, one says 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> 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 provably equivalent (often abbreviated as <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>), and one may pass to the <a class="existingWikiWord" href="/nlab/show/poset">poset</a> of provable equivalence classes (the usual way in which a poset is associated with a preorder).</p> <p>One knows that one is in the realm of <em>classical</em> propositional logic if the poset of provable equivalence classes is a <a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a>, in which <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> induces the meet operation 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> the join operation. Here the rules of inference allow bi-entailments such as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>⇒</mo><mi>B</mi><mo>≡</mo><mo>¬</mo><mi>A</mi><mo>∨</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \Rightarrow B \equiv \neg A \vee B</annotation></semantics></math></div> <p>and in fact the different types of propositional logic are usually conveniently described by specifying what type of algebraic structure we get on the poset of provable equivalence classes. For example, in <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a> this poset forms a <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/logic">logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive logic</a> / <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a></li> </ul> <div> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category">category</a></th><th><a class="existingWikiWord" href="/nlab/show/functor">functor</a></th><th><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></th><th><a class="existingWikiWord" href="/nlab/show/theory">theory</a></th><th><a class="existingWikiWord" href="/nlab/show/hyperdoctrine">hyperdoctrine</a></th><th><a class="existingWikiWord" href="/nlab/show/subobject+poset">subobject poset</a></th><th><a class="existingWikiWord" href="/nlab/show/coverage">coverage</a></th><th><a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/finitely+complete+category">finitely complete category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+functor">cartesian functor</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+logic">cartesian logic</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/essentially+algebraic+theory">essentially algebraic theory</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/lextensive+category">lextensive category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunctive+logic">disjunctive logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+functor">regular functor</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+logic">regular logic</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+theory">regular theory</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+hyperdoctrine">regular hyperdoctrine</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/infimum">infimum</a>-<a class="existingWikiWord" href="/nlab/show/semilattice">semilattice</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+coverage">regular coverage</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/regular+topos">regular topos</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+category">coherent category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+functor">coherent functor</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+logic">coherent logic</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+theory">coherent theory</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+hyperdoctrine">coherent hyperdoctrine</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/distributive+lattice">distributive lattice</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+coverage">coherent coverage</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coherent+topos">coherent topos</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+category">geometric category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+functor">geometric functor</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+logic">geometric logic</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+theory">geometric theory</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+hyperdoctrine">geometric hyperdoctrine</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/frame">frame</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/geometric+coverage">geometric coverage</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Heyting+category">Heyting category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Heyting+functor">Heyting functor</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic</a> <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></td><td style="text-align: left;">intuitionistic <a class="existingWikiWord" href="/nlab/show/first-order+theory">first-order theory</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/first-order+hyperdoctrine">first-order hyperdoctrine</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/De+Morgan+Heyting+category">De Morgan Heyting category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic</a> <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a> with <a class="existingWikiWord" href="/nlab/show/weak+excluded+middle">weak excluded middle</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/De+Morgan+Heyting+algebra">De Morgan Heyting algebra</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Boolean+category">Boolean category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/classical+logic">classical</a> <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></td><td style="text-align: left;">classical <a class="existingWikiWord" href="/nlab/show/first-order+theory">first-order theory</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Boolean+hyperdoctrine">Boolean hyperdoctrine</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/star-autonomous+category">star-autonomous category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/multiplicative+classical+linear+logic">multiplicative classical linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+closed+category">symmetric monoidal closed category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/multiplicative+intuitionistic+linear+logic">multiplicative intuitionistic linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/fragment">fragment</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>&</mi><mo>,</mo><mo>⊤</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\&, \top\}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cocartesian+monoidal+category">cocartesian monoidal category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/fragment">fragment</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⊕</mo><mo>,</mo><mn>0</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\oplus, 0\}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/simply+typed+lambda+calculus">simply typed lambda calculus</a></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> </tbody></table> </div></body></html> </div> <div class="revisedby"> <p> Last revised on November 16, 2022 at 06:10:32. See the <a href="/nlab/history/classical+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/classical+logic" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/7720/#Item_13">Discuss</a><span class="backintime"><a href="/nlab/revision/classical+logic/15" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/classical+logic" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/classical+logic" accesskey="S" class="navlink" id="history" rel="nofollow">History (15 revisions)</a> <a href="/nlab/show/classical+logic/cite" style="color: black">Cite</a> <a href="/nlab/print/classical+logic" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/classical+logic" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>