CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Tautology (logic) - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"16762b6c-215e-4da4-b92a-2449162bad41","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Tautology_(logic)","wgTitle":"Tautology (logic)","wgCurRevisionId":1254124403,"wgRevisionId":1254124403,"wgArticleId":4495335,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Articles with short description","Short description is different from Wikidata","Articles containing Ancient Greek (to 1453)-language text","Pages that use a deprecated format of the math tags","Logical expressions","Logical truth","Mathematical logic","Propositional calculus","Propositions","Semantics","Sentences by type"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Tautology_(logic)","wgRelevantArticleId": 4495335,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":20000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q209555","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"], "GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.math.styles":"ready","ext.cite.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","ext.scribunto.logs","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher", "ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.math.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Tautology (logic) - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Tautology_(logic)"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Tautology_(logic)&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/Tautology_(logic)"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Tautology_logic rootpage-Tautology_logic skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Tautology+%28logic%29" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Tautology+%28logic%29" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Tautology+%28logic%29" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Tautology+%28logic%29" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-History" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#History"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>History</span> </div> </a> <ul id="toc-History-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Background" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Background"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>Background</span> </div> </a> <ul id="toc-Background-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Definition_and_examples" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Definition_and_examples"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Definition and examples</span> </div> </a> <ul id="toc-Definition_and_examples-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Verifying_tautologies" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Verifying_tautologies"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Verifying tautologies</span> </div> </a> <ul id="toc-Verifying_tautologies-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Tautological_implication" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Tautological_implication"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>Tautological implication</span> </div> </a> <ul id="toc-Tautological_implication-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Substitution" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Substitution"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>Substitution</span> </div> </a> <ul id="toc-Substitution-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Semantic_completeness_and_soundness" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Semantic_completeness_and_soundness"> <div class="vector-toc-text"> <span class="vector-toc-numb">7</span> <span>Semantic completeness and soundness</span> </div> </a> <ul id="toc-Semantic_completeness_and_soundness-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Efficient_verification_and_the_Boolean_satisfiability_problem" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Efficient_verification_and_the_Boolean_satisfiability_problem"> <div class="vector-toc-text"> <span class="vector-toc-numb">8</span> <span>Efficient verification and the Boolean satisfiability problem</span> </div> </a> <ul id="toc-Efficient_verification_and_the_Boolean_satisfiability_problem-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Tautologies_versus_validities_in_first-order_logic" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Tautologies_versus_validities_in_first-order_logic"> <div class="vector-toc-text"> <span class="vector-toc-numb">9</span> <span>Tautologies versus validities in first-order logic</span> </div> </a> <ul id="toc-Tautologies_versus_validities_in_first-order_logic-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Tautologies_in_Non-Classical_Logics" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Tautologies_in_Non-Classical_Logics"> <div class="vector-toc-text"> <span class="vector-toc-numb">10</span> <span>Tautologies in Non-Classical Logics</span> </div> </a> <ul id="toc-Tautologies_in_Non-Classical_Logics-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-See_also" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#See_also"> <div class="vector-toc-text"> <span class="vector-toc-numb">11</span> <span>See also</span> </div> </a> <button aria-controls="toc-See_also-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle See also subsection</span> </button> <ul id="toc-See_also-sublist" class="vector-toc-list"> <li id="toc-Normal_forms" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Normal_forms"> <div class="vector-toc-text"> <span class="vector-toc-numb">11.1</span> <span>Normal forms</span> </div> </a> <ul id="toc-Normal_forms-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Related_logical_topics" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Related_logical_topics"> <div class="vector-toc-text"> <span class="vector-toc-numb">11.2</span> <span>Related logical topics</span> </div> </a> <ul id="toc-Related_logical_topics-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">12</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Further_reading" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Further_reading"> <div class="vector-toc-text"> <span class="vector-toc-numb">13</span> <span>Further reading</span> </div> </a> <ul id="toc-Further_reading-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-External_links" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#External_links"> <div class="vector-toc-text"> <span class="vector-toc-numb">14</span> <span>External links</span> </div> </a> <ul id="toc-External_links-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Tautology (logic)</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 37 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-37" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">37 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-ar mw-list-item"><a href="https://ar.wikipedia.org/wiki/%D8%B7%D9%88%D8%B7%D9%88%D9%84%D9%88%D8%AC%D9%8A%D8%A7" title="طوطولوجيا – Arabic" lang="ar" hreflang="ar" data-title="طوطولوجيا" data-language-autonym="العربية" data-language-local-name="Arabic" class="interlanguage-link-target"><span>العربية</span></a></li><li class="interlanguage-link interwiki-bg mw-list-item"><a href="https://bg.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B2%D1%82%D0%BE%D0%BB%D0%BE%D0%B3%D0%B8%D1%8F_(%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0)" title="Тавтология (логика) – Bulgarian" lang="bg" hreflang="bg" data-title="Тавтология (логика)" data-language-autonym="Български" data-language-local-name="Bulgarian" class="interlanguage-link-target"><span>Български</span></a></li><li class="interlanguage-link interwiki-ca mw-list-item"><a href="https://ca.wikipedia.org/wiki/Tautologia_(l%C3%B2gica)" title="Tautologia (lògica) – Catalan" lang="ca" hreflang="ca" data-title="Tautologia (lògica)" data-language-autonym="Català" data-language-local-name="Catalan" class="interlanguage-link-target"><span>Català</span></a></li><li class="interlanguage-link interwiki-cs mw-list-item"><a href="https://cs.wikipedia.org/wiki/Tautologie" title="Tautologie – Czech" lang="cs" hreflang="cs" data-title="Tautologie" data-language-autonym="Čeština" data-language-local-name="Czech" class="interlanguage-link-target"><span>Čeština</span></a></li><li class="interlanguage-link interwiki-da mw-list-item"><a href="https://da.wikipedia.org/wiki/Tautologi" title="Tautologi – Danish" lang="da" hreflang="da" data-title="Tautologi" data-language-autonym="Dansk" data-language-local-name="Danish" class="interlanguage-link-target"><span>Dansk</span></a></li><li class="interlanguage-link interwiki-de mw-list-item"><a href="https://de.wikipedia.org/wiki/Tautologie_(Logik)" title="Tautologie (Logik) – German" lang="de" hreflang="de" data-title="Tautologie (Logik)" data-language-autonym="Deutsch" data-language-local-name="German" class="interlanguage-link-target"><span>Deutsch</span></a></li><li class="interlanguage-link interwiki-et mw-list-item"><a href="https://et.wikipedia.org/wiki/Tautoloogia" title="Tautoloogia – Estonian" lang="et" hreflang="et" data-title="Tautoloogia" data-language-autonym="Eesti" data-language-local-name="Estonian" class="interlanguage-link-target"><span>Eesti</span></a></li><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/Tautolog%C3%ADa" title="Tautología – Spanish" lang="es" hreflang="es" data-title="Tautología" data-language-autonym="Español" data-language-local-name="Spanish" class="interlanguage-link-target"><span>Español</span></a></li><li class="interlanguage-link interwiki-eo mw-list-item"><a href="https://eo.wikipedia.org/wiki/Ta%C5%ADtologio" title="Taŭtologio – Esperanto" lang="eo" hreflang="eo" data-title="Taŭtologio" data-language-autonym="Esperanto" data-language-local-name="Esperanto" class="interlanguage-link-target"><span>Esperanto</span></a></li><li class="interlanguage-link interwiki-eu mw-list-item"><a href="https://eu.wikipedia.org/wiki/Tautologia_(logika)" title="Tautologia (logika) – Basque" lang="eu" hreflang="eu" data-title="Tautologia (logika)" data-language-autonym="Euskara" data-language-local-name="Basque" class="interlanguage-link-target"><span>Euskara</span></a></li><li class="interlanguage-link interwiki-fa mw-list-item"><a href="https://fa.wikipedia.org/wiki/%D9%87%D9%85%D8%A7%D9%86%E2%80%8C%DA%AF%D9%88%DB%8C%DB%8C_(%D9%85%D9%86%D8%B7%D9%82)" title="همان‌گویی (منطق) – Persian" lang="fa" hreflang="fa" data-title="همان‌گویی (منطق)" data-language-autonym="فارسی" data-language-local-name="Persian" class="interlanguage-link-target"><span>فارسی</span></a></li><li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Tautologie_(logique)" title="Tautologie (logique) – French" lang="fr" hreflang="fr" data-title="Tautologie (logique)" data-language-autonym="Français" data-language-local-name="French" class="interlanguage-link-target"><span>Français</span></a></li><li class="interlanguage-link interwiki-gl mw-list-item"><a href="https://gl.wikipedia.org/wiki/Tautolox%C3%ADa_(l%C3%B3xica)" title="Tautoloxía (lóxica) – Galician" lang="gl" hreflang="gl" data-title="Tautoloxía (lóxica)" data-language-autonym="Galego" data-language-local-name="Galician" class="interlanguage-link-target"><span>Galego</span></a></li><li class="interlanguage-link interwiki-ko mw-list-item"><a href="https://ko.wikipedia.org/wiki/%ED%95%AD%EC%A7%84%EC%8B%9D" title="항진식 – Korean" lang="ko" hreflang="ko" data-title="항진식" data-language-autonym="한국어" data-language-local-name="Korean" class="interlanguage-link-target"><span>한국어</span></a></li><li class="interlanguage-link interwiki-id mw-list-item"><a href="https://id.wikipedia.org/wiki/Tautologi_(logika)" title="Tautologi (logika) – Indonesian" lang="id" hreflang="id" data-title="Tautologi (logika)" data-language-autonym="Bahasa Indonesia" data-language-local-name="Indonesian" class="interlanguage-link-target"><span>Bahasa Indonesia</span></a></li><li class="interlanguage-link interwiki-is mw-list-item"><a href="https://is.wikipedia.org/wiki/S%C3%ADsanna" title="Sísanna – Icelandic" lang="is" hreflang="is" data-title="Sísanna" data-language-autonym="Íslenska" data-language-local-name="Icelandic" class="interlanguage-link-target"><span>Íslenska</span></a></li><li class="interlanguage-link interwiki-it mw-list-item"><a href="https://it.wikipedia.org/wiki/Tautologia" title="Tautologia – Italian" lang="it" hreflang="it" data-title="Tautologia" data-language-autonym="Italiano" data-language-local-name="Italian" class="interlanguage-link-target"><span>Italiano</span></a></li><li class="interlanguage-link interwiki-he mw-list-item"><a href="https://he.wikipedia.org/wiki/%D7%98%D7%90%D7%95%D7%98%D7%95%D7%9C%D7%95%D7%92%D7%99%D7%94_(%D7%9C%D7%95%D7%92%D7%99%D7%A7%D7%94)" title="טאוטולוגיה (לוגיקה) – Hebrew" lang="he" hreflang="he" data-title="טאוטולוגיה (לוגיקה)" data-language-autonym="עברית" data-language-local-name="Hebrew" class="interlanguage-link-target"><span>עברית</span></a></li><li class="interlanguage-link interwiki-ky mw-list-item"><a href="https://ky.wikipedia.org/wiki/%D0%9A%D0%B0%D0%B9%D1%82%D0%B0%D0%BB%D0%B0%D0%BC%D0%B0" title="Кайталама – Kyrgyz" lang="ky" hreflang="ky" data-title="Кайталама" data-language-autonym="Кыргызча" data-language-local-name="Kyrgyz" class="interlanguage-link-target"><span>Кыргызча</span></a></li><li class="interlanguage-link interwiki-lt mw-list-item"><a href="https://lt.wikipedia.org/wiki/Tautologija" title="Tautologija – Lithuanian" lang="lt" hreflang="lt" data-title="Tautologija" data-language-autonym="Lietuvių" data-language-local-name="Lithuanian" class="interlanguage-link-target"><span>Lietuvių</span></a></li><li class="interlanguage-link interwiki-hu mw-list-item"><a href="https://hu.wikipedia.org/wiki/Tautol%C3%B3gia_(logika)" title="Tautológia (logika) – Hungarian" lang="hu" hreflang="hu" data-title="Tautológia (logika)" data-language-autonym="Magyar" data-language-local-name="Hungarian" class="interlanguage-link-target"><span>Magyar</span></a></li><li class="interlanguage-link interwiki-mk mw-list-item"><a href="https://mk.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B2%D1%82%D0%BE%D0%BB%D0%BE%D0%B3%D0%B8%D1%98%D0%B0_(%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0)" title="Тавтологија (логика) – Macedonian" lang="mk" hreflang="mk" data-title="Тавтологија (логика)" data-language-autonym="Македонски" data-language-local-name="Macedonian" class="interlanguage-link-target"><span>Македонски</span></a></li><li class="interlanguage-link interwiki-arz mw-list-item"><a href="https://arz.wikipedia.org/wiki/%D8%AA%D9%88%D8%AA%D9%88%D9%84%D9%88%D8%AC%D9%8A%D8%A7" title="توتولوجيا – Egyptian Arabic" lang="arz" hreflang="arz" data-title="توتولوجيا" data-language-autonym="مصرى" data-language-local-name="Egyptian Arabic" class="interlanguage-link-target"><span>مصرى</span></a></li><li class="interlanguage-link interwiki-nl mw-list-item"><a href="https://nl.wikipedia.org/wiki/Tautologie_(logica)" title="Tautologie (logica) – Dutch" lang="nl" hreflang="nl" data-title="Tautologie (logica)" data-language-autonym="Nederlands" data-language-local-name="Dutch" class="interlanguage-link-target"><span>Nederlands</span></a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/%E6%81%92%E7%9C%9F%E5%BC%8F" title="恒真式 – Japanese" lang="ja" hreflang="ja" data-title="恒真式" data-language-autonym="日本語" data-language-local-name="Japanese" class="interlanguage-link-target"><span>日本語</span></a></li><li class="interlanguage-link interwiki-no mw-list-item"><a href="https://no.wikipedia.org/wiki/Tautologi_(logikk)" title="Tautologi (logikk) – Norwegian Bokmål" lang="nb" hreflang="nb" data-title="Tautologi (logikk)" data-language-autonym="Norsk bokmål" data-language-local-name="Norwegian Bokmål" class="interlanguage-link-target"><span>Norsk bokmål</span></a></li><li class="interlanguage-link interwiki-pl mw-list-item"><a href="https://pl.wikipedia.org/wiki/Tautologia_(logika)" title="Tautologia (logika) – Polish" lang="pl" hreflang="pl" data-title="Tautologia (logika)" data-language-autonym="Polski" data-language-local-name="Polish" class="interlanguage-link-target"><span>Polski</span></a></li><li class="interlanguage-link interwiki-pt mw-list-item"><a href="https://pt.wikipedia.org/wiki/Tautologia_(l%C3%B3gica)" title="Tautologia (lógica) – Portuguese" lang="pt" hreflang="pt" data-title="Tautologia (lógica)" data-language-autonym="Português" data-language-local-name="Portuguese" class="interlanguage-link-target"><span>Português</span></a></li><li class="interlanguage-link interwiki-ru mw-list-item"><a href="https://ru.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B2%D1%82%D0%BE%D0%BB%D0%BE%D0%B3%D0%B8%D1%8F_(%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0)" title="Тавтология (логика) – Russian" lang="ru" hreflang="ru" data-title="Тавтология (логика)" data-language-autonym="Русский" data-language-local-name="Russian" class="interlanguage-link-target"><span>Русский</span></a></li><li class="interlanguage-link interwiki-simple mw-list-item"><a href="https://simple.wikipedia.org/wiki/Tautology_(logic)" title="Tautology (logic) – Simple English" lang="en-simple" hreflang="en-simple" data-title="Tautology (logic)" data-language-autonym="Simple English" data-language-local-name="Simple English" class="interlanguage-link-target"><span>Simple English</span></a></li><li class="interlanguage-link interwiki-sk mw-list-item"><a href="https://sk.wikipedia.org/wiki/Toto%C5%BEnostno-pravdiv%C3%BD_v%C3%BDrok" title="Totožnostno-pravdivý výrok – Slovak" lang="sk" hreflang="sk" data-title="Totožnostno-pravdivý výrok" data-language-autonym="Slovenčina" data-language-local-name="Slovak" class="interlanguage-link-target"><span>Slovenčina</span></a></li><li class="interlanguage-link interwiki-sr mw-list-item"><a href="https://sr.wikipedia.org/wiki/%D0%A2%D0%B0%D1%83%D1%82%D0%BE%D0%BB%D0%BE%D0%B3%D0%B8%D1%98%D0%B0_(%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0)" title="Таутологија (логика) – Serbian" lang="sr" hreflang="sr" data-title="Таутологија (логика)" data-language-autonym="Српски / srpski" data-language-local-name="Serbian" class="interlanguage-link-target"><span>Српски / srpski</span></a></li><li class="interlanguage-link interwiki-sv mw-list-item"><a href="https://sv.wikipedia.org/wiki/Tautologi_(logik)" title="Tautologi (logik) – Swedish" lang="sv" hreflang="sv" data-title="Tautologi (logik)" data-language-autonym="Svenska" data-language-local-name="Swedish" class="interlanguage-link-target"><span>Svenska</span></a></li><li class="interlanguage-link interwiki-tr mw-list-item"><a href="https://tr.wikipedia.org/wiki/Totoloji_(mant%C4%B1k)" title="Totoloji (mantık) – Turkish" lang="tr" hreflang="tr" data-title="Totoloji (mantık)" data-language-autonym="Türkçe" data-language-local-name="Turkish" class="interlanguage-link-target"><span>Türkçe</span></a></li><li class="interlanguage-link interwiki-uk mw-list-item"><a href="https://uk.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B2%D1%82%D0%BE%D0%BB%D0%BE%D0%B3%D1%96%D1%8F_(%D0%BB%D0%BE%D0%B3%D1%96%D0%BA%D0%B0)" title="Тавтологія (логіка) – Ukrainian" lang="uk" hreflang="uk" data-title="Тавтологія (логіка)" data-language-autonym="Українська" data-language-local-name="Ukrainian" class="interlanguage-link-target"><span>Українська</span></a></li><li class="interlanguage-link interwiki-ur mw-list-item"><a href="https://ur.wikipedia.org/wiki/%D8%AA%D8%B7%D9%88%DB%8C%D9%84_(%D9%85%D9%86%D8%B7%D9%82)" title="تطویل (منطق) – Urdu" lang="ur" hreflang="ur" data-title="تطویل (منطق)" data-language-autonym="اردو" data-language-local-name="Urdu" class="interlanguage-link-target"><span>اردو</span></a></li><li class="interlanguage-link interwiki-zh mw-list-item"><a href="https://zh.wikipedia.org/wiki/%E6%81%86%E7%9C%9F%E5%BC%8F" title="恆真式 – Chinese" lang="zh" hreflang="zh" data-title="恆真式" data-language-autonym="中文" data-language-local-name="Chinese" class="interlanguage-link-target"><span>中文</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q209555#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Tautology_(logic)" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Tautology_(logic)" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Tautology_(logic)"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Tautology_(logic)"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Tautology_(logic)" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Tautology_(logic)" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages" title="A list of all special pages [q]" accesskey="q"><span>Special pages</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&oldid=1254124403" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Tautology_%28logic%29&id=1254124403&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FTautology_%28logic%29"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FTautology_%28logic%29"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Tautology_%28logic%29&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Tautology_(logic)&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q209555" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><div class="shortdescription nomobile noexcerpt noprint searchaux" style="display:none">In logic, a statement which is always true</div> <style data-mw-deduplicate="TemplateStyles:r1236090951">.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}</style><div role="note" class="hatnote navigation-not-searchable">This article is about tautology in formal logic. For other uses, see <a href="/wiki/Tautology_(disambiguation)" class="mw-redirect mw-disambig" title="Tautology (disambiguation)">Tautology (disambiguation)</a>.</div> <p>In <a href="/wiki/Mathematical_logic" title="Mathematical logic">mathematical logic</a>, a <b>tautology</b> (from <a href="/wiki/Ancient_Greek_language" class="mw-redirect" title="Ancient Greek language">Ancient Greek</a>: <span lang="grc">ταυτολογία</span>) is a <a href="/wiki/Well-formed_formula" title="Well-formed formula">formula</a> that is true regardless of the interpretation of its component <a href="/wiki/Term_(logic)" title="Term (logic)"> terms</a>, with only the <a href="/wiki/Logical_constant" title="Logical constant">logical constants</a> having a fixed meaning. For example, a formula that states, "the ball is green or the ball is not green," is always true, regardless of what a ball is and regardless of its colour. Tautology is usually, though not always, used to refer to valid formulas of <a href="/wiki/Propositional_logic" class="mw-redirect" title="Propositional logic">propositional logic</a>. </p><p>The philosopher <a href="/wiki/Ludwig_Wittgenstein" title="Ludwig Wittgenstein">Ludwig Wittgenstein</a> first applied the term to redundancies of <a href="/wiki/Propositional_logic" class="mw-redirect" title="Propositional logic">propositional logic</a> in 1921, borrowing from <a href="/wiki/Rhetoric" title="Rhetoric">rhetoric</a>, where a <a href="/wiki/Tautology_(rhetoric)" class="mw-redirect" title="Tautology (rhetoric)">tautology</a> is a repetitive statement. In logic, a formula is <a href="/wiki/Satisfiability_and_validity" class="mw-redirect" title="Satisfiability and validity">satisfiable</a> if it is true under at least one interpretation, and thus a tautology is a formula whose negation is unsatisfiable. In other words, it cannot be false. </p><p>Unsatisfiable statements, both through negation and affirmation, are known formally as <a href="/wiki/Contradiction" title="Contradiction">contradictions</a>. A formula that is neither a tautology nor a contradiction is said to be <a href="/wiki/Contingency_(philosophy)" title="Contingency (philosophy)">logically contingent</a>. Such a formula can be made either true or false based on the values assigned to its propositional variables. </p><p>The <a href="/wiki/Double_turnstile" title="Double turnstile">double turnstile</a> notation <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \vDash S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>⊨</mo> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \vDash S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9510f7d1d521313f9fc7f632c62fd6ec528553d8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.159ex; height:2.843ex;" alt="{\displaystyle \vDash S}"></span> is used to indicate that <i>S</i> is a tautology. Tautology is sometimes symbolized by "V<i>pq</i>", and contradiction by "O<i>pq</i>". The <a href="/wiki/Tee_(symbol)" title="Tee (symbol)">tee</a> symbol <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \top }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">⊤</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \top }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cf12e436fef2365e76fcb1034a51179d8328bb33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \top }"></span> is sometimes used to denote an arbitrary tautology, with the dual symbol <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">⊥</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \bot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f282c7bc331cc3bfcf1c57f1452cc23c022f58de" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \bot }"></span> (<a href="/wiki/Falsum" class="mw-redirect" title="Falsum">falsum</a>) representing an arbitrary contradiction; in any symbolism, a tautology may be substituted for the truth value "<a href="/wiki/Logical_truth" title="Logical truth">true</a>", as symbolized, for instance, by "1".<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> </p><p>Tautologies are a key concept in <a href="/wiki/Propositional_logic" class="mw-redirect" title="Propositional logic">propositional logic</a>, where a tautology is defined as a propositional formula that is true under any possible <a href="/wiki/Boolean_valuation" class="mw-redirect" title="Boolean valuation">Boolean valuation</a> of its <a href="/wiki/Propositional_variable" title="Propositional variable">propositional variables</a>.<sup id="cite_ref-:0_2-0" class="reference"><a href="#cite_note-:0-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> A key property of tautologies in propositional logic is that an <a href="/wiki/Effective_method" title="Effective method">effective method</a> exists for testing whether a given formula is always satisfied (equiv., whether its negation is unsatisfiable). </p><p>The definition of tautology can be extended to sentences in <a href="/wiki/Predicate_logic" class="mw-redirect" title="Predicate logic">predicate logic</a>, which may contain <a href="/wiki/Quantification_(logic)" class="mw-redirect" title="Quantification (logic)">quantifiers</a>—a feature absent from sentences of propositional logic. Indeed, in propositional logic, there is no distinction between a tautology and a <a href="/wiki/Validity_(logic)" title="Validity (logic)">logically valid</a> formula. In the context of predicate logic, many authors define a tautology to be a sentence that can be obtained by taking a tautology of propositional logic, and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable). The set of such formulas is a <a href="/wiki/Proper_subset" class="mw-redirect" title="Proper subset">proper subset</a> of the set of logically valid sentences of predicate logic (i.e., sentences that are true in every <a href="/wiki/Structure_(mathematical_logic)" title="Structure (mathematical logic)">model</a>). </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="History">History</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=1" title="Edit section: History"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The word tautology was used by the ancient Greeks to describe a statement that was asserted to be true merely by virtue of saying the same thing twice, a <a href="/wiki/Pejorative" title="Pejorative">pejorative</a> meaning that is still used for <a href="/wiki/Tautology_(rhetoric)" class="mw-redirect" title="Tautology (rhetoric)">rhetorical tautologies</a>. Between 1800 and 1940, the word gained new meaning in logic, and is currently used in <a href="/wiki/Mathematical_logic" title="Mathematical logic">mathematical logic</a> to denote a certain type of propositional formula, without the pejorative connotations it originally possessed. </p><p>In 1800, <a href="/wiki/Immanuel_Kant" title="Immanuel Kant">Immanuel Kant</a> wrote in his book <i>Logic</i>: </p> <style data-mw-deduplicate="TemplateStyles:r1244412712">.mw-parser-output .templatequote{overflow:hidden;margin:1em 0;padding:0 32px}.mw-parser-output .templatequotecite{line-height:1.5em;text-align:left;margin-top:0}@media(min-width:500px){.mw-parser-output .templatequotecite{padding-left:1.6em}}</style><blockquote class="templatequote"><p>The identity of concepts in analytical judgments can be either <i>explicit</i> (<i>explicita</i>) or <i>non-explicit</i> (<i>implicita</i>). In the former case analytic propositions are <i>tautological.</i></p></blockquote> <p>Here, <i>analytic proposition</i> refers to an <a href="/wiki/Logical_truth#Logical_truths_and_analytic_truths" title="Logical truth">analytic truth</a>, a statement in natural language that is true solely because of the terms involved. </p><p>In 1884, <a href="/wiki/Gottlob_Frege" title="Gottlob Frege">Gottlob Frege</a> proposed in his <i>Grundlagen</i> that a truth is analytic exactly if it can be derived using logic. However, he maintained a distinction between analytic truths (i.e., truths based only on the meanings of their terms) and tautologies (i.e., statements devoid of content). </p><p>In his <i><a href="/wiki/Tractatus_Logico-Philosophicus" title="Tractatus Logico-Philosophicus">Tractatus Logico-Philosophicus</a></i> in 1921, Ludwig Wittgenstein proposed that statements that can be deduced by logical deduction are tautological (empty of meaning), as well as being analytic truths. <a href="/wiki/Henri_Poincar%C3%A9" title="Henri Poincaré">Henri Poincaré</a> had made similar remarks in <i><a href="/wiki/Science_and_Hypothesis" title="Science and Hypothesis">Science and Hypothesis</a></i> in 1905. Although <a href="/wiki/Bertrand_Russell" title="Bertrand Russell">Bertrand Russell</a> at first argued against these remarks by Wittgenstein and Poincaré, claiming that mathematical truths were not only non-tautologous but were <a href="/wiki/Synthetic_truth" class="mw-redirect" title="Synthetic truth">synthetic</a>, he later spoke in favor of them in 1918: </p> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1244412712"><blockquote class="templatequote"><p>Everything that is a proposition of logic has got to be in some sense or the other like a tautology. It has got to be something that has some peculiar quality, which I do not know how to define, that belongs to logical propositions but not to others.</p></blockquote> <p>Here, <i>logical proposition</i> refers to a proposition that is provable using the laws of logic. </p><p>Many logicians in the early 20th century used the term 'tautology' for any formula that is universally valid, whether a formula of <a href="/wiki/Propositional_logic" class="mw-redirect" title="Propositional logic">propositional logic</a> or of <a href="/wiki/First-order_logic" title="First-order logic">predicate logic</a>. In this broad sense, a tautology is a formula that is true under all <a href="/wiki/Interpretation_(logic)" title="Interpretation (logic)">interpretations</a>, or that is logically equivalent to the negation of a contradiction. <a href="/wiki/Alfred_Tarski" title="Alfred Tarski">Tarski</a> and <a href="/wiki/Kurt_G%C3%B6del" title="Kurt Gödel">Gödel</a> followed this usage and it appears in textbooks such as that of Lewis and Langford.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> This broad use of the term is less common today, though some textbooks continue to use it. <sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> <sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> </p><p>Modern textbooks more commonly restrict the use of 'tautology' to valid sentences of propositional logic, or valid sentences of predicate logic that can be reduced to propositional tautologies by substitution. <sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> <sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading2"><h2 id="Background">Background</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=2" title="Edit section: Background"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236090951"><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="/wiki/Propositional_logic" class="mw-redirect" title="Propositional logic">Propositional logic</a></div> <p>Propositional logic begins with <b>propositional variables</b>, atomic units that represent concrete propositions. A <b>formula</b> consists of propositional variables connected by logical connectives, built up in such a way that the truth of the overall formula can be deduced from the truth or falsity of each variable. A <b>valuation</b> is a function that assigns each propositional variable to either T (for truth) or F (for falsity). So by using the propositional variables <i>A</i> and <i>B</i>, the binary connectives <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lor }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∨</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lor }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ab47f6b1f589aedcf14638df1d63049d233d851a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \lor }"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∧</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \land }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d6823e5a222eb3ca49672818ac3d13ec607052c4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \land }"></span> representing <a href="/wiki/Logical_disjunction" title="Logical disjunction">disjunction</a> and <a href="/wiki/Logical_conjunction" title="Logical conjunction">conjunction</a> respectively, and the unary connective <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/099107443792f5fec9bebe39b919a690db7198c1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \lnot }"></span> representing <a href="/wiki/Negation" title="Negation">negation</a>, the following formula can be obtained:<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\land B)\lor (\lnot A)\lor (\lnot B)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\land B)\lor (\lnot A)\lor (\lnot B)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4f2d45f06cee4d4881219449c0b0a73fefab5654" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.291ex; height:2.843ex;" alt="{\displaystyle (A\land B)\lor (\lnot A)\lor (\lnot B)}"></span>. </p><p>A valuation here must assign to each of <i>A</i> and <i>B</i> either T or F. But no matter how this assignment is made, the overall formula will come out true. For if the first disjunct <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\land B)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\land B)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ebdcd2d1d13bc1f915aa141415965509a4e2b4f1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.899ex; height:2.843ex;" alt="{\displaystyle (A\land B)}"></span> is not satisfied by a particular valuation, then <i>A</i> or <i>B</i> must be assigned F, which will make one of the following disjunct to be assigned T. In natural language, either both A and B are true or at least one of them is false. </p> <div class="mw-heading mw-heading2"><h2 id="Definition_and_examples">Definition and examples</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=3" title="Edit section: Definition and examples"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1251242444">.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}</style><table class="box-Too_abstract plainlinks metadata ambox ambox-style" role="presentation"><tbody><tr><td class="mbox-image"><div class="mbox-image-div"><span typeof="mw:File"><a href="/wiki/File:Emblem-question-yellow.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/en/thumb/a/aa/Emblem-question-yellow.svg/40px-Emblem-question-yellow.svg.png" decoding="async" width="40" height="40" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/a/aa/Emblem-question-yellow.svg/60px-Emblem-question-yellow.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/a/aa/Emblem-question-yellow.svg/80px-Emblem-question-yellow.svg.png 2x" data-file-width="48" data-file-height="48" /></a></span></div></td><td class="mbox-text"><div class="mbox-text-span">This article may be written in a style that is <b>too abstract</b> to be readily understandable by <a href="/wiki/Wikipedia:MTAA" class="mw-redirect" title="Wikipedia:MTAA">general audiences</a>.<span class="hide-when-compact"> Please <a href="/wiki/Wikipedia:EDIT" class="mw-redirect" title="Wikipedia:EDIT">improve</a> it by defining technical terminology, and by adding examples.</span> <span class="date-container"><i>(<span class="date">May 2020</span>)</i></span></div></td></tr></tbody></table> <p>A formula of propositional logic is a <i>tautology</i> if the formula itself is always true, regardless of which valuation is used for the <a href="/wiki/Propositional_variable" title="Propositional variable">propositional variables</a>. There are infinitely many tautologies. </p><p>In many of the following examples <i>A</i> represents the statement "object <i>X</i> is bound", <i>B</i> represents "object <i>X</i> is a book", and C represents "object <i>X</i> is on the shelf". Without a specific referent object <i>X</i>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\to B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo stretchy="false">→</mo> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\to B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d5b8dd84619daff17b52a08b77d15db2b9ad6c2a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.121ex; height:2.176ex;" alt="{\displaystyle A\to B}"></span> corresponds to the proposition "all bound things are books". </p> <ul><li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor \lnot A)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\lor \lnot A)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ab553b5d4656bafd558a2dc86a152fd94965f5f0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.428ex; height:2.843ex;" alt="{\displaystyle (A\lor \lnot A)}"></span> ("<i>A</i> or not <i>A</i>"), the <a href="/wiki/Law_of_excluded_middle" title="Law of excluded middle">law of excluded middle</a>. This formula has only one propositional variable, <i>A</i>. Any valuation for this formula must, by definition, assign <i>A</i> one of the truth values <i>true</i> or <i>false</i>, and assign <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/099107443792f5fec9bebe39b919a690db7198c1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \lnot }"></span><i>A</i> the other truth value. For instance, "The cat is black or the cat is not black".</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\to B)\Leftrightarrow (\lnot B\to \lnot A)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\to B)\Leftrightarrow (\lnot B\to \lnot A)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/098f044d01ad9910ab70cd46e545a8903e50c454" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.576ex; height:2.843ex;" alt="{\displaystyle (A\to B)\Leftrightarrow (\lnot B\to \lnot A)}"></span> ("if <i>A</i> implies <i>B</i>, then not-<i>B</i> implies not-<i>A</i>", and vice versa), which expresses the law of <a href="/wiki/Contraposition" title="Contraposition">contraposition</a>. For instance, "If it's bound, it is a book; if it's not a book, it's not bound" and vice versa.</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((\lnot A\to B)\land (\lnot A\to \lnot B))\to A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">→</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((\lnot A\to B)\land (\lnot A\to \lnot B))\to A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0f4a6d0f98e002706de264a485f925aedf33ede9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:32.261ex; height:2.843ex;" alt="{\displaystyle ((\lnot A\to B)\land (\lnot A\to \lnot B))\to A}"></span> ("if not-<i>A</i> implies both <i>B</i> and its negation not-<i>B</i>, then not-<i>A</i> must be false, then <i>A</i> must be true"), which is the principle known as <i><a href="/wiki/Reductio_ad_absurdum" title="Reductio ad absurdum">reductio ad absurdum</a></i>. For instance, "If it's not bound, we know it's a book, if it's not bound, we know it's also not a book, so it is bound".</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot (A\land B)\Leftrightarrow (\lnot A\lor \lnot B)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot (A\land B)\Leftrightarrow (\lnot A\lor \lnot B)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c524422701e12217f3b51cb7a4b5ebfe54ed12b7" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.063ex; height:2.843ex;" alt="{\displaystyle \lnot (A\land B)\Leftrightarrow (\lnot A\lor \lnot B)}"></span> ("if not both <i>A</i> and <i>B</i>, then not-<i>A</i> or not-<i>B</i>", and vice versa), which is known as <a href="/wiki/De_Morgan%27s_law" class="mw-redirect" title="De Morgan's law">De Morgan's law</a>. "If it is not both a book and bound, then we are sure that it's not a book or that it's not bound" and vice versa.</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((A\to B)\land (B\to C))\to (A\to C)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((A\to B)\land (B\to C))\to (A\to C)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/72953ec90cee0d9be9b936f5622727a28913a239" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:34.823ex; height:2.843ex;" alt="{\displaystyle ((A\to B)\land (B\to C))\to (A\to C)}"></span> ("if <i>A</i> implies <i>B</i> and <i>B</i> implies <i>C</i>, then <i>A</i> implies <i>C</i>"), which is the principle known as <a href="/wiki/Hypothetical_syllogism#Propositional_logic" title="Hypothetical syllogism">hypothetical syllogism</a>. "If it's bound, then it's a book and if it's a book, then it's on that shelf, so if it's bound, it's on that shelf".</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((A\lor B)\land (A\to C)\land (B\to C))\to C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</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 stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((A\lor B)\land (A\to C)\land (B\to C))\to C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d7043a8c9880f868c508c655566fd9fb9c62eb59" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:38.14ex; height:2.843ex;" alt="{\displaystyle ((A\lor B)\land (A\to C)\land (B\to C))\to C}"></span> ("if at least one of <i>A</i> or <i>B</i> is true, and each implies <i>C</i>, then <i>C</i> must be true as well"), which is the principle known as <a href="/wiki/Proof_by_cases" class="mw-redirect" title="Proof by cases">proof by cases</a>. "Bound things and books are on that shelf. If it's either a book or it's blue, it's on that shelf".</li></ul> <p>A minimal tautology is a tautology that is not the instance of a shorter tautology. </p> <ul><li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\lor B)\to (A\lor B)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∨</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∨</mo> <mi>B</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\lor B)\to (A\lor B)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b989bff15287f20e29310efe2e96fbfa3286933c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.412ex; height:2.843ex;" alt="{\displaystyle (A\lor B)\to (A\lor B)}"></span> is a tautology, but not a minimal one, because it is an instantiation of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C\to C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>C</mi> <mo stretchy="false">→</mo> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle C\to C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/66a7207fef685a567785359fee46605774e1766f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.147ex; height:2.176ex;" alt="{\displaystyle C\to C}"></span>.</li></ul> <div class="mw-heading mw-heading2"><h2 id="Verifying_tautologies">Verifying tautologies</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=4" title="Edit section: Verifying tautologies"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The problem of determining whether a formula is a tautology is fundamental in propositional logic. If there are <i>n</i> variables occurring in a formula then there are 2<sup><i>n</i></sup> distinct valuations for the formula. Therefore, the task of determining whether or not the formula is a tautology is a finite and mechanical one: one needs only to evaluate the <a href="/wiki/Truth_value" title="Truth value">truth value</a> of the formula under each of its possible valuations. One algorithmic method for verifying that every valuation makes the formula to be true is to make a <a href="/wiki/Truth_table" title="Truth table">truth table</a> that includes every possible valuation.<sup id="cite_ref-:0_2-1" class="reference"><a href="#cite_note-:0-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> </p><p>For example, consider the formula </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C)).}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo>.</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C)).}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cce8248fb6011325b512bf3355e488b106dd5136" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.47ex; height:2.843ex;" alt="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C)).}"></span></dd></dl> <p>There are 8 possible valuations for the propositional variables <i>A</i>, <i>B</i>, <i>C</i>, represented by the first three columns of the following table. The remaining columns show the truth of subformulas of the formula above, culminating in a column showing the truth value of the original formula under each valuation. </p> <table class="wikitable" style="text-align: center;"> <tbody><tr> <th><span class="nowrap">⁠<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}"></span>⁠</span></th> <th><span class="nowrap">⁠<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/47136aad860d145f75f3eed3022df827cee94d7a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}"></span>⁠</span></th> <th><span class="nowrap">⁠<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc55753007cd3c18576f7933f6f089196732029" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.766ex; height:2.176ex;" alt="{\displaystyle C}"></span>⁠</span></th> <th><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\land B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>∧</mo> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\land B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/74954195333a8593163b93a9688695b8dc74da55" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.09ex; height:2.176ex;" alt="{\displaystyle A\land B}"></span></th> <th><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\land B)\to C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\land B)\to C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/58fecede545555ce1607458f802a4f8ccb9accf7" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.279ex; height:2.843ex;" alt="{\displaystyle (A\land B)\to C}"></span></th> <th><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B\to C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle B\to C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a9febe2010e6933c5e384a066ef7d5f634b97a7e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.144ex; height:2.176ex;" alt="{\displaystyle B\to C}"></span></th> <th><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\to (B\to C)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\to (B\to C)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b2b33f36f729c9aa2cfdadb0b7d6b58580818228" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.311ex; height:2.843ex;" alt="{\displaystyle A\to (B\to C)}"></span></th> <th><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b161ccc7e428dd923128dae00e2c4268a9382ba0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:34.823ex; height:2.843ex;" alt="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}"></span> </th></tr> <tr> <td>T</td> <td>T</td> <td>T</td> <td>T</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr> <tr> <td>T</td> <td>T</td> <td>F</td> <td>T</td> <td>F</td> <td>F</td> <td>F</td> <td>T </td></tr> <tr> <td>T</td> <td>F</td> <td>T</td> <td>F</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr> <tr> <td>T</td> <td>F</td> <td>F</td> <td>F</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr> <tr> <td>F</td> <td>T</td> <td>T</td> <td>F</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr> <tr> <td>F</td> <td>T</td> <td>F</td> <td>F</td> <td>T</td> <td>F</td> <td>T</td> <td>T </td></tr> <tr> <td>F</td> <td>F</td> <td>T</td> <td>F</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr> <tr> <td>F</td> <td>F</td> <td>F</td> <td>F</td> <td>T</td> <td>T</td> <td>T</td> <td>T </td></tr></tbody></table> <p>Because each row of the final column shows <i>T</i>, the sentence in question is verified to be a tautology. </p><p>It is also possible to define a <a href="/wiki/Deductive_system" class="mw-redirect" title="Deductive system">deductive system</a> (i.e., proof system) for propositional logic, as a simpler variant of the deductive systems employed for first-order logic (see Kleene 1967, Sec 1.9 for one such system). A proof of a tautology in an appropriate deduction system may be much shorter than a complete truth table (a formula with <i>n</i> propositional variables requires a truth table with 2<sup><i>n</i></sup> lines, which quickly becomes infeasible as <i>n</i> increases). Proof systems are also required for the study of <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic</a> propositional logic, in which the method of truth tables cannot be employed because the law of the excluded middle is not assumed. </p> <div class="mw-heading mw-heading2"><h2 id="Tautological_implication">Tautological implication</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=5" title="Edit section: Tautological implication"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236090951"><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="/wiki/Tautological_consequence" title="Tautological consequence">Tautological consequence</a></div> <p>A formula <i>R</i> is said to <b>tautologically imply</b> a formula <i>S</i> if every valuation that causes <i>R</i> to be true also causes <i>S</i> to be true. This situation is denoted <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R\models S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> <mo>⊨</mo> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R\models S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6d49ddd79c8ada52cf08db64070fc134cfbd2b1a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.568ex; height:2.843ex;" alt="{\displaystyle R\models S}"></span>. It is equivalent to the formula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R\to S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> <mo stretchy="false">→</mo> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R\to S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/499bc5e6b1153b43ba86d31780bc215f01aa0bf1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.877ex; height:2.176ex;" alt="{\displaystyle R\to S}"></span> being a tautology (Kleene 1967 p. 27). </p><p>For example, let <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> be <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\land (B\lor \lnot B)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\land (B\lor \lnot B)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/60255d5b706f8baaee19318cfce4af5e376b0e3e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.796ex; height:2.843ex;" alt="{\displaystyle A\land (B\lor \lnot B)}"></span>. Then <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> is not a tautology, because any valuation that makes <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}"></span></i> false will make <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> false. But any valuation that makes <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}"></span></i> true will make <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> true, because <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B\lor \lnot B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>B</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle B\lor \lnot B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/99886f848ae93c75408b416dff4580494edd2523" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.661ex; height:2.176ex;" alt="{\displaystyle B\lor \lnot B}"></span> is a tautology. Let <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span></i> be the formula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\land C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>∧</mo> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\land C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/70bb9844880566f77e0ea00f8a17ed569d8d1726" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.092ex; height:2.176ex;" alt="{\displaystyle A\land C}"></span>. Then <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R\models S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> <mo>⊨</mo> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R\models S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6d49ddd79c8ada52cf08db64070fc134cfbd2b1a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.568ex; height:2.843ex;" alt="{\displaystyle R\models S}"></span>, because any valuation satisfying <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span></i> will make <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}"></span></i> true—and thus makes <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> true. </p><p>It follows from the definition that if a formula <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span></i> is a contradiction, then <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span></i> tautologically implies every formula, because there is no truth valuation that causes <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span></i> to be true, and so the definition of tautological implication is trivially satisfied. Similarly, if <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> is a tautology, then <i><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4611d85173cd3b508e67077d4a1252c9c05abca2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}"></span></i> is tautologically implied by every formula. </p> <div class="mw-heading mw-heading2"><h2 id="Substitution">Substitution</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=6" title="Edit section: Substitution"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236090951"><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="/wiki/Substitution_instance" class="mw-redirect" title="Substitution instance">Substitution instance</a></div> <p>There is a general procedure, the <b>substitution rule</b>, that allows additional tautologies to be constructed from a given tautology (Kleene 1967 sec. 3). Suppose that <span class="texhtml mvar" style="font-style:italic;">S</span> is a tautology and for each propositional variable <span class="texhtml mvar" style="font-style:italic;">A</span> in <span class="texhtml mvar" style="font-style:italic;">S</span> a fixed sentence <span class="texhtml mvar" style="font-style:italic;">S<sub>A</sub></span> is chosen. Then the sentence obtained by replacing each variable <span class="texhtml mvar" style="font-style:italic;">A</span> in <span class="texhtml mvar" style="font-style:italic;">S</span> with the corresponding sentence <span class="texhtml mvar" style="font-style:italic;">S<sub>A</sub></span> is also a tautology. </p><p>For example, let <span class="texhtml mvar" style="font-style:italic;">S</span> be the tautology: </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (A\land B)\lor \lnot A\lor \lnot B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (A\land B)\lor \lnot A\lor \lnot B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0de2fd72960eadc32257afb75315594108ff8cab" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.672ex; height:2.843ex;" alt="{\displaystyle (A\land B)\lor \lnot A\lor \lnot B}"></span>.</dd></dl> <p>Let <span class="texhtml mvar" style="font-style:italic;">S<sub>A</sub></span> be <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C\lor D}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>C</mi> <mo>∨</mo> <mi>D</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle C\lor D}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c85b67fc743ea47c72219cc96329ea364997c82b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.273ex; height:2.176ex;" alt="{\displaystyle C\lor D}"></span> and let <span class="texhtml mvar" style="font-style:italic;">S<sub>B</sub></span> be <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C\to E}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>C</mi> <mo stretchy="false">→</mo> <mi>E</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle C\to E}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/27f24bf52b3555e18537a3f41044ed0f74af8b75" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.156ex; height:2.176ex;" alt="{\displaystyle C\to E}"></span>. </p><p>It follows from the substitution rule that the sentence: </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((C\lor D)\land (C\to E))\lor \lnot (C\lor D)\lor \lnot (C\to E)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>C</mi> <mo>∨</mo> <mi>D</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>C</mi> <mo stretchy="false">→</mo> <mi>E</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>C</mi> <mo>∨</mo> <mi>D</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>C</mi> <mo stretchy="false">→</mo> <mi>E</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((C\lor D)\land (C\to E))\lor \lnot (C\lor D)\lor \lnot (C\to E)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4eebb1522e6ab842a8cae370e61d2857532ab2e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:46.753ex; height:2.843ex;" alt="{\displaystyle ((C\lor D)\land (C\to E))\lor \lnot (C\lor D)\lor \lnot (C\to E)}"></span></dd></dl> <p>is also a tautology. </p> <div class="mw-heading mw-heading2"><h2 id="Semantic_completeness_and_soundness">Semantic completeness and soundness</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=7" title="Edit section: Semantic completeness and soundness"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>An <a href="/wiki/Axiomatic_system" title="Axiomatic system">axiomatic system</a> is <a href="/wiki/Completeness_(logic)" title="Completeness (logic)">complete</a> if every tautology is a theorem (derivable from axioms). An axiomatic system is <a href="/wiki/Soundness" title="Soundness">sound</a> if every theorem is a tautology. </p> <div class="mw-heading mw-heading2"><h2 id="Efficient_verification_and_the_Boolean_satisfiability_problem">Efficient verification and the Boolean satisfiability problem</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=8" title="Edit section: Efficient verification and the Boolean satisfiability problem"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The problem of constructing practical algorithms to determine whether sentences with large numbers of propositional variables are tautologies is an area of contemporary research in the area of <a href="/wiki/Automated_theorem_proving" title="Automated theorem proving">automated theorem proving</a>. </p><p>The method of <a href="/wiki/Truth_tables" class="mw-redirect" title="Truth tables">truth tables</a> illustrated above is provably correct – the truth table for a tautology will end in a column with only <i>T</i>, while the truth table for a sentence that is not a tautology will contain a row whose final column is <i>F</i>, and the valuation corresponding to that row is a valuation that does not satisfy the sentence being tested. This method for verifying tautologies is an <a href="/wiki/Effective_procedure" class="mw-redirect" title="Effective procedure">effective procedure</a>, which means that given unlimited computational resources it can always be used to mechanistically determine whether a sentence is a tautology. This means, in particular, the set of tautologies over a fixed finite or countable alphabet is a <a href="/wiki/Decidable_set" class="mw-redirect" title="Decidable set">decidable set</a>. </p><p>As an <a href="/wiki/Efficient_procedure" class="mw-redirect" title="Efficient procedure">efficient procedure</a>, however, truth tables are constrained by the fact that the number of valuations that must be checked increases as 2<sup><i>k</i></sup>, where <i>k</i> is the number of variables in the formula. This exponential growth in the computation length renders the truth table method useless for formulas with thousands of propositional variables, as contemporary computing hardware cannot execute the algorithm in a feasible time period. </p><p>The problem of determining whether there is any valuation that makes a formula true is the <a href="/wiki/Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a>; the problem of checking tautologies is equivalent to this problem, because verifying that a sentence <i>S</i> is a tautology is equivalent to verifying that there is no valuation satisfying <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot S}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>S</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot S}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/25d8e529dce6b478e956c5a52a56b35bd403929a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.05ex; height:2.176ex;" alt="{\displaystyle \lnot S}"></span>. The Boolean satisfiability problem is <a href="/wiki/NP-complete" class="mw-redirect" title="NP-complete">NP-complete</a>, and consequently, tautology is <a href="/wiki/Co-NP-complete" title="Co-NP-complete">co-NP-complete</a>. It is widely believed that (equivalently for all NP-complete problems) no <a href="/wiki/Polynomial-time_algorithm" class="mw-redirect" title="Polynomial-time algorithm">polynomial-time algorithm</a> can solve the satisfiability problem, although some algorithms perform well on special classes of formulas, or terminate quickly on many instances.<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading2"><h2 id="Tautologies_versus_validities_in_first-order_logic">Tautologies versus validities in first-order logic</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=9" title="Edit section: Tautologies versus validities in first-order logic"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The fundamental definition of a tautology is in the context of propositional logic. The definition can be extended, however, to sentences in <a href="/wiki/First-order_logic" title="First-order logic">first-order logic</a>.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> These sentences may contain quantifiers, unlike sentences of propositional logic. In the context of first-order logic, a distinction is maintained between <i>logical validities</i>, sentences that are true in every model, and <i>tautologies</i> (or, <i>tautological validities</i>), which are a proper subset of the first-order logical validities. In the context of propositional logic, these two terms coincide. </p><p>A tautology in first-order logic is a sentence that can be obtained by taking a tautology of propositional logic and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable). For example, because <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\lor \lnot A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\lor \lnot A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/42bc39c90e40298464f5f82377cb9e7ed52e938f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.619ex; height:2.176ex;" alt="{\displaystyle A\lor \lnot A}"></span> is a tautology of propositional logic, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\forall x(x=x))\lor (\lnot \forall x(x=x))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>=</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>=</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\forall x(x=x))\lor (\lnot \forall x(x=x))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/dbd2ba6fe297ec4eca0ea94051d19189b7e25b83" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.13ex; height:2.843ex;" alt="{\displaystyle (\forall x(x=x))\lor (\lnot \forall x(x=x))}"></span> is a tautology in first order logic. Similarly, in a first-order language with a unary relation symbols <i>R</i>,<i>S</i>,<i>T</i>, the following sentence is a tautology: </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (((\exists xRx)\land \lnot (\exists xSx))\to \forall xTx)\Leftrightarrow ((\exists xRx)\to ((\lnot \exists xSx)\to \forall xTx)).}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>R</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo>∧</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>S</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>T</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>R</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>S</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>T</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo>.</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (((\exists xRx)\land \lnot (\exists xSx))\to \forall xTx)\Leftrightarrow ((\exists xRx)\to ((\lnot \exists xSx)\to \forall xTx)).}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4430d0257beea1747560863b478044ded886d411" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:68.771ex; height:2.843ex;" alt="{\displaystyle (((\exists xRx)\land \lnot (\exists xSx))\to \forall xTx)\Leftrightarrow ((\exists xRx)\to ((\lnot \exists xSx)\to \forall xTx)).}"></span></dd></dl> <p>It is obtained by replacing <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7daff47fa58cdfd29dc333def748ff5fa4c923e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}"></span> with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists xRx}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>R</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists xRx}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1a4d4a873b7094fbd05698877ee33d16eff96532" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.716ex; height:2.176ex;" alt="{\displaystyle \exists xRx}"></span>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/47136aad860d145f75f3eed3022df827cee94d7a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}"></span> with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot \exists xSx}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi>S</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot \exists xSx}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8f0badf19c8ba7ecd1d930556e4cc1cfa67374dc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.001ex; height:2.176ex;" alt="{\displaystyle \lnot \exists xSx}"></span>, and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>C</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle C}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc55753007cd3c18576f7933f6f089196732029" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.766ex; height:2.176ex;" alt="{\displaystyle C}"></span> with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall xTx}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>T</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall xTx}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e87d515ef56ffb2ba34b78014c7b8a450fffe1ca" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.588ex; height:2.176ex;" alt="{\displaystyle \forall xTx}"></span> in the propositional tautology: <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo>∧</mo> <mi>B</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">⇔</mo> <mo stretchy="false">(</mo> <mi>A</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>B</mi> <mo stretchy="false">→</mo> <mi>C</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b161ccc7e428dd923128dae00e2c4268a9382ba0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:34.823ex; height:2.843ex;" alt="{\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}"></span>. </p><p>Not all logical validities are tautologies in first-order logic. For example, the sentence: </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\forall xRx)\to \lnot \exists x\lnot Rx}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>R</mi> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">¬</mi> <mi>R</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\forall xRx)\to \lnot \exists x\lnot Rx}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/96a7147c32a23111310147e6e255af950c5d8ed5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.956ex; height:2.843ex;" alt="{\displaystyle (\forall xRx)\to \lnot \exists x\lnot Rx}"></span></dd></dl> <p>is true in any first-order interpretation, but it corresponds to the propositional sentence <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\to B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo stretchy="false">→</mo> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\to B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d5b8dd84619daff17b52a08b77d15db2b9ad6c2a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.121ex; height:2.176ex;" alt="{\displaystyle A\to B}"></span> which is not a tautology of propositional logic. </p> <div class="mw-heading mw-heading2"><h2 id="Tautologies_in_Non-Classical_Logics">Tautologies in Non-Classical Logics</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=10" title="Edit section: Tautologies in Non-Classical Logics"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Whether a given formula is a tautology depends on the formal system of logic that is in use. For example, the following formula is a tautology of classical logic but not of <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a>: </p> <dl><dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg \neg A\to A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo stretchy="false">→</mo> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg A\to A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/84aaf1a07ba682fb0d3a84a80bc528871cd5bd78" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.201ex; height:2.176ex;" alt="{\displaystyle \neg \neg A\to A}"></span></dd></dl> <div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=11" title="Edit section: See also"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Normal_forms">Normal forms</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=12" title="Edit section: Normal forms"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a href="/wiki/Algebraic_normal_form" title="Algebraic normal form">Algebraic normal form</a></li> <li><a href="/wiki/Conjunctive_normal_form" title="Conjunctive normal form">Conjunctive normal form</a></li> <li><a href="/wiki/Disjunctive_normal_form" title="Disjunctive normal form">Disjunctive normal form</a></li> <li><a href="/wiki/Logic_optimization" title="Logic optimization">Logic optimization</a></li></ul> <div class="mw-heading mw-heading3"><h3 id="Related_logical_topics">Related logical topics</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=13" title="Edit section: Related logical topics"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1216972533">.mw-parser-output .col-begin{border-collapse:collapse;padding:0;color:inherit;width:100%;border:0;margin:0}.mw-parser-output .col-begin-small{font-size:90%}.mw-parser-output .col-break{vertical-align:top;text-align:left}.mw-parser-output .col-break-2{width:50%}.mw-parser-output .col-break-3{width:33.3%}.mw-parser-output .col-break-4{width:25%}.mw-parser-output .col-break-5{width:20%}@media(max-width:720px){.mw-parser-output .col-begin,.mw-parser-output .col-begin>tbody,.mw-parser-output .col-begin>tbody>tr,.mw-parser-output .col-begin>tbody>tr>td{display:block!important;width:100%!important}.mw-parser-output .col-break{padding-left:0!important}}</style><div> <table class="col-begin" role="presentation"> <tbody><tr> <td class="col-break"> <ul><li><a href="/wiki/Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li> <li><a href="/wiki/Boolean_domain" title="Boolean domain">Boolean domain</a></li> <li><a href="/wiki/Boolean_function" title="Boolean function">Boolean function</a></li> <li><a href="/wiki/Contradiction" title="Contradiction">Contradiction</a></li> <li><a href="/wiki/False_(logic)" title="False (logic)">False (logic)</a></li> <li><a href="/wiki/Syllogism" title="Syllogism">Syllogism</a></li> <li><a href="/wiki/List_of_logic_symbols" title="List of logic symbols">List of logic symbols</a></li></ul> </td> <td class="col-break"> <ul><li><a href="/wiki/Logic_synthesis" title="Logic synthesis">Logic synthesis</a></li> <li><a href="/wiki/Logical_consequence" title="Logical consequence">Logical consequence</a></li> <li><a href="/wiki/Logical_graph" class="mw-redirect" title="Logical graph">Logical graph</a></li> <li><a href="/wiki/Logical_truth" title="Logical truth">Logical truth</a></li> <li><a href="/wiki/Vacuous_truth" title="Vacuous truth">Vacuous truth</a></li></ul> <p>  </p> </td></tr></tbody></table></div> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=14" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFWeisstein" class="citation web cs1">Weisstein, Eric W. <a rel="nofollow" class="external text" href="https://mathworld.wolfram.com/Tautology.html">"Tautology"</a>. <i>mathworld.wolfram.com</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2020-08-14</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=mathworld.wolfram.com&rft.atitle=Tautology&rft.aulast=Weisstein&rft.aufirst=Eric+W.&rft_id=https%3A%2F%2Fmathworld.wolfram.com%2FTautology.html&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span></span> </li> <li id="cite_note-:0-2"><span class="mw-cite-backlink">^ <a href="#cite_ref-:0_2-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-:0_2-1"><sup><i><b>b</b></i></sup></a></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.britannica.com/topic/tautology">"tautology | Definition & Facts"</a>. <i>Encyclopedia Britannica</i><span class="reference-accessdate">. Retrieved <span class="nowrap">2020-08-14</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=Encyclopedia+Britannica&rft.atitle=tautology+%7C+Definition+%26+Facts&rft_id=https%3A%2F%2Fwww.britannica.com%2Ftopic%2Ftautology&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFLewisLangford1959" class="citation book cs1">Lewis, C I; Langford, C H (1959). <i>Symbolic Logic</i> (2nd ed.). Dover.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Symbolic+Logic&rft.edition=2nd&rft.pub=Dover&rft.date=1959&rft.aulast=Lewis&rft.aufirst=C+I&rft.au=Langford%2C+C+H&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span> </span> </li> <li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFHedman2004" class="citation book cs1">Hedman, Shawn (2004). <i>A First Course in Logic</i>. Oxford University Press. p. 63.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=A+First+Course+in+Logic&rft.pages=63&rft.pub=Oxford+University+Press&rft.date=2004&rft.aulast=Hedman&rft.aufirst=Shawn&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span> </span> </li> <li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFRautenberg2010" class="citation book cs1">Rautenberg, Wolfgang (2010). <i>A Concise Introduction to Mathematical Logic</i>. Springer. p. 64.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=A+Concise+Introduction+to+Mathematical+Logic&rft.pages=64&rft.pub=Springer&rft.date=2010&rft.aulast=Rautenberg&rft.aufirst=Wolfgang&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span> </span> </li> <li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFEnderton2001" class="citation book cs1">Enderton, Herbert (2001). <i>Mathematical Introduction to Logic</i>. Academic Press. p. 88.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Mathematical+Introduction+to+Logic&rft.pages=88&rft.pub=Academic+Press&rft.date=2001&rft.aulast=Enderton&rft.aufirst=Herbert&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span> </span> </li> <li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFHinman2010" class="citation book cs1">Hinman, Peter (2010). <i>Fundamentals of Mathematical Logic</i>. Springer. p. 98.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Fundamentals+of+Mathematical+Logic&rft.pages=98&rft.pub=Springer&rft.date=2010&rft.aulast=Hinman&rft.aufirst=Peter&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span> </span> </li> <li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text">See <a href="/wiki/SAT_solver" title="SAT solver">SAT solver</a> for references.</span> </li> <li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation journal cs1"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1111/j.1559-3584.2002.tb00103.x">"New Members"</a>. <i>Naval Engineers Journal</i>. <b>114</b> (1): 17–18. January 2002. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1111%2Fj.1559-3584.2002.tb00103.x">10.1111/j.1559-3584.2002.tb00103.x</a>. <a href="/wiki/ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0028-1425">0028-1425</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Naval+Engineers+Journal&rft.atitle=New+Members&rft.volume=114&rft.issue=1&rft.pages=17-18&rft.date=2002-01&rft_id=info%3Adoi%2F10.1111%2Fj.1559-3584.2002.tb00103.x&rft.issn=0028-1425&rft_id=http%3A%2F%2Fdx.doi.org%2F10.1111%2Fj.1559-3584.2002.tb00103.x&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span></span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=15" title="Edit section: Further reading"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a href="/wiki/J%C3%B3zef_Maria_Boche%C5%84ski" title="Józef Maria Bocheński">Bocheński, J. M.</a> (1959) <i>Précis of Mathematical Logic</i>, translated from the French and German editions by Otto Bird, <a href="/wiki/Dordrecht" title="Dordrecht">Dordrecht</a>, <a href="/wiki/South_Holland" title="South Holland">South Holland</a>: <a href="/wiki/D._Reidel" title="D. Reidel">D. Reidel</a>.</li> <li><a href="/wiki/Herbert_Enderton" title="Herbert Enderton">Enderton, H. B.</a> (2002) <i>A Mathematical Introduction to Logic</i>, <a href="/wiki/Harcourt_(publisher)" title="Harcourt (publisher)">Harcourt</a>/<a href="/wiki/Academic_Press" title="Academic Press">Academic Press</a>, <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-12-238452-0" title="Special:BookSources/0-12-238452-0">0-12-238452-0</a>.</li> <li><a href="/wiki/Stephen_Kleene" class="mw-redirect" title="Stephen Kleene">Kleene, S. C.</a> (1967) <i>Mathematical Logic</i>, reprinted 2002, <a href="/wiki/Dover_Publications" title="Dover Publications">Dover Publications</a>, <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-486-42533-9" title="Special:BookSources/0-486-42533-9">0-486-42533-9</a>.</li> <li><a href="/wiki/Hans_Reichenbach" title="Hans Reichenbach">Reichenbach, H.</a> (1947). <i>Elements of Symbolic Logic</i>, reprinted 1980, Dover, <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-486-24004-5" title="Special:BookSources/0-486-24004-5">0-486-24004-5</a></li> <li><a href="/wiki/Ludwig_Wittgenstein" title="Ludwig Wittgenstein">Wittgenstein, L.</a> (1921). "Logisch-philosophiche Abhandlung", <i>Annalen der Naturphilosophie</i> (Leipzig), v. 14, pp. 185–262, reprinted in English translation as <i>Tractatus logico-philosophicus</i>, <a href="/wiki/New_York_City" title="New York City">New York City</a> and <a href="/wiki/London" title="London">London</a>, 1922.</li></ul> <div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Tautology_(logic)&action=edit&section=16" title="Edit section: External links"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation cs2"><a rel="nofollow" class="external text" href="https://www.encyclopediaofmath.org/index.php?title=Tautology">"Tautology"</a>, <i><a href="/wiki/Encyclopedia_of_Mathematics" title="Encyclopedia of Mathematics">Encyclopedia of Mathematics</a></i>, <a href="/wiki/European_Mathematical_Society" title="European Mathematical Society">EMS Press</a>, 2001 [1994]</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=Tautology&rft.btitle=Encyclopedia+of+Mathematics&rft.pub=EMS+Press&rft.date=2001&rft_id=https%3A%2F%2Fwww.encyclopediaofmath.org%2Findex.php%3Ftitle%3DTautology&rfr_id=info%3Asid%2Fen.wikipedia.org%3ATautology+%28logic%29" class="Z3988"></span></li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Mathematical_logic" style="padding:3px"><table class="nowraplinks mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Mathematical_logic" title="Template:Mathematical logic"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Mathematical_logic" title="Template talk:Mathematical logic"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Mathematical_logic" title="Special:EditPage/Template:Mathematical logic"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Mathematical_logic" style="font-size:114%;margin:0 4em"><a href="/wiki/Mathematical_logic" title="Mathematical logic">Mathematical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Axiom" title="Axiom">Axiom</a> <ul><li><a href="/wiki/List_of_axioms" title="List of axioms">list</a></li></ul></li> <li><a href="/wiki/Cardinality" title="Cardinality">Cardinality</a></li> <li><a href="/wiki/First-order_logic" title="First-order logic">First-order logic</a></li> <li><a href="/wiki/Formal_proof" title="Formal proof">Formal proof</a></li> <li><a href="/wiki/Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a></li> <li><a href="/wiki/Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a></li> <li><a href="/wiki/Information_theory" title="Information theory">Information theory</a></li> <li><a href="/wiki/Lemma_(mathematics)" title="Lemma (mathematics)">Lemma</a></li> <li><a href="/wiki/Logical_consequence" title="Logical consequence">Logical consequence</a></li> <li><a href="/wiki/Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a></li> <li><a href="/wiki/Theorem" title="Theorem">Theorem</a></li> <li><a href="/wiki/Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a></li> <li><a href="/wiki/Type_theory" title="Type theory">Type theory</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theorems (<a href="/wiki/Category:Theorems_in_the_foundations_of_mathematics" title="Category:Theorems in the foundations of mathematics">list</a>)<br /> and <a href="/wiki/Paradoxes_of_set_theory" title="Paradoxes of set theory">paradoxes</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/G%C3%B6del%27s_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness</a> and <a href="/wiki/G%C3%B6del%27s_incompleteness_theorems" title="Gödel's incompleteness theorems">incompleteness theorems</a></li> <li><a href="/wiki/Tarski%27s_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability</a></li> <li><a href="/wiki/Banach%E2%80%93Tarski_paradox" title="Banach–Tarski paradox">Banach–Tarski paradox</a></li> <li>Cantor's <a href="/wiki/Cantor%27s_theorem" title="Cantor's theorem">theorem,</a> <a href="/wiki/Cantor%27s_paradox" title="Cantor's paradox">paradox</a> and <a href="/wiki/Cantor%27s_diagonal_argument" title="Cantor's diagonal argument">diagonal argument</a></li> <li><a href="/wiki/Compactness_theorem" title="Compactness theorem">Compactness</a></li> <li><a href="/wiki/Halting_problem" title="Halting problem">Halting problem</a></li> <li><a href="/wiki/Lindstr%C3%B6m%27s_theorem" title="Lindström's theorem">Lindström's</a></li> <li><a href="/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem</a></li> <li><a href="/wiki/Russell%27s_paradox" title="Russell's paradox">Russell's paradox</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Logic" title="Logic">Logics</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th id="Traditional" scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Term_logic" title="Term logic">Traditional</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Classical_logic" title="Classical logic">Classical logic</a></li> <li><a href="/wiki/Logical_truth" title="Logical truth">Logical truth</a></li> <li><a class="mw-selflink selflink">Tautology</a></li> <li><a href="/wiki/Proposition" title="Proposition">Proposition</a></li> <li><a href="/wiki/Inference" title="Inference">Inference</a></li> <li><a href="/wiki/Logical_equivalence" title="Logical equivalence">Logical equivalence</a></li> <li><a href="/wiki/Consistency" title="Consistency">Consistency</a> <ul><li><a href="/wiki/Equiconsistency" title="Equiconsistency">Equiconsistency</a></li></ul></li> <li><a href="/wiki/Argument" title="Argument">Argument</a></li> <li><a href="/wiki/Soundness" title="Soundness">Soundness</a></li> <li><a href="/wiki/Validity_(logic)" title="Validity (logic)">Validity</a></li> <li><a href="/wiki/Syllogism" title="Syllogism">Syllogism</a></li> <li><a href="/wiki/Square_of_opposition" title="Square of opposition">Square of opposition</a></li> <li><a href="/wiki/Venn_diagram" title="Venn diagram">Venn diagram</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Propositional_calculus" title="Propositional calculus">Propositional</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li> <li><a href="/wiki/Boolean_function" title="Boolean function">Boolean functions</a></li> <li><a href="/wiki/Logical_connective" title="Logical connective">Logical connectives</a></li> <li><a href="/wiki/Propositional_calculus" title="Propositional calculus">Propositional calculus</a></li> <li><a href="/wiki/Propositional_formula" title="Propositional formula">Propositional formula</a></li> <li><a href="/wiki/Truth_table" title="Truth table">Truth tables</a></li> <li><a href="/wiki/Many-valued_logic" title="Many-valued logic">Many-valued logic</a> <ul><li><a href="/wiki/Three-valued_logic" title="Three-valued logic">3</a></li> <li><a href="/wiki/Finite-valued_logic" title="Finite-valued logic">finite</a></li> <li><a href="/wiki/Infinite-valued_logic" title="Infinite-valued logic">∞</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/First-order_logic" title="First-order logic">First-order</a> <ul><li><a href="/wiki/List_of_first-order_theories" title="List of first-order theories"><span style="font-size:85%;">list</span></a></li></ul></li> <li><a href="/wiki/Second-order_logic" title="Second-order logic">Second-order</a> <ul><li><a href="/wiki/Monadic_second-order_logic" title="Monadic second-order logic">Monadic</a></li></ul></li> <li><a href="/wiki/Higher-order_logic" title="Higher-order logic">Higher-order</a></li> <li><a href="/wiki/Fixed-point_logic" title="Fixed-point logic">Fixed-point</a></li> <li><a href="/wiki/Free_logic" title="Free logic">Free</a></li> <li><a href="/wiki/Quantifier_(logic)" title="Quantifier (logic)">Quantifiers</a></li> <li><a href="/wiki/Predicate_(mathematical_logic)" title="Predicate (mathematical logic)">Predicate</a></li> <li><a href="/wiki/Monadic_predicate_calculus" title="Monadic predicate calculus">Monadic predicate calculus</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Set_theory" title="Set theory">Set theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Set</a> <ul><li><a href="/wiki/Hereditary_set" title="Hereditary set">hereditary</a></li></ul></li> <li><a href="/wiki/Class_(set_theory)" title="Class (set theory)">Class</a></li> <li>(<a href="/wiki/Urelement" title="Urelement">Ur-</a>)<a href="/wiki/Element_(mathematics)" title="Element (mathematics)">Element</a></li> <li><a href="/wiki/Ordinal_number" title="Ordinal number">Ordinal number</a></li> <li><a href="/wiki/Extensionality" title="Extensionality">Extensionality</a></li> <li><a href="/wiki/Forcing_(mathematics)" title="Forcing (mathematics)">Forcing</a></li> <li><a href="/wiki/Relation_(mathematics)" title="Relation (mathematics)">Relation</a> <ul><li><a href="/wiki/Equivalence_relation" title="Equivalence relation">equivalence</a></li> <li><a href="/wiki/Partition_of_a_set" title="Partition of a set">partition</a></li></ul></li> <li>Set operations: <ul><li><a href="/wiki/Intersection_(set_theory)" title="Intersection (set theory)">intersection</a></li> <li><a href="/wiki/Union_(set_theory)" title="Union (set theory)">union</a></li> <li><a href="/wiki/Complement_(set_theory)" title="Complement (set theory)">complement</a></li> <li><a href="/wiki/Cartesian_product" title="Cartesian product">Cartesian product</a></li> <li><a href="/wiki/Power_set" title="Power set">power set</a></li> <li><a href="/wiki/List_of_set_identities_and_relations" title="List of set identities and relations">identities</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Types of <a href="/wiki/Set_(mathematics)" title="Set (mathematics)">sets</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Countable_set" title="Countable set">Countable</a></li> <li><a href="/wiki/Uncountable_set" title="Uncountable set">Uncountable</a></li> <li><a href="/wiki/Empty_set" title="Empty set">Empty</a></li> <li><a href="/wiki/Inhabited_set" title="Inhabited set">Inhabited</a></li> <li><a href="/wiki/Singleton_(mathematics)" title="Singleton (mathematics)">Singleton</a></li> <li><a href="/wiki/Finite_set" title="Finite set">Finite</a></li> <li><a href="/wiki/Infinite_set" title="Infinite set">Infinite</a></li> <li><a href="/wiki/Transitive_set" title="Transitive set">Transitive</a></li> <li><a href="/wiki/Ultrafilter_(set_theory)" class="mw-redirect" title="Ultrafilter (set theory)">Ultrafilter</a></li> <li><a href="/wiki/Recursive_set" class="mw-redirect" title="Recursive set">Recursive</a></li> <li><a href="/wiki/Fuzzy_set" title="Fuzzy set">Fuzzy</a></li> <li><a href="/wiki/Universal_set" title="Universal set">Universal</a></li> <li><a href="/wiki/Universe_(mathematics)" title="Universe (mathematics)">Universe</a> <ul><li><a href="/wiki/Constructible_universe" title="Constructible universe">constructible</a></li> <li><a href="/wiki/Grothendieck_universe" title="Grothendieck universe">Grothendieck</a></li> <li><a href="/wiki/Von_Neumann_universe" title="Von Neumann universe">Von Neumann</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Map_(mathematics)" title="Map (mathematics)">Maps</a> and <a href="/wiki/Cardinality" title="Cardinality">cardinality</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Function_(mathematics)" title="Function (mathematics)">Function</a>/<a href="/wiki/Map_(mathematics)" title="Map (mathematics)">Map</a> <ul><li><a href="/wiki/Domain_of_a_function" title="Domain of a function">domain</a></li> <li><a href="/wiki/Codomain" title="Codomain">codomain</a></li> <li><a href="/wiki/Image_(mathematics)" title="Image (mathematics)">image</a></li></ul></li> <li><a href="/wiki/Injective_function" title="Injective function">In</a>/<a href="/wiki/Surjective_function" title="Surjective function">Sur</a>/<a href="/wiki/Bijection" title="Bijection">Bi</a>-jection</li> <li><a href="/wiki/Schr%C3%B6der%E2%80%93Bernstein_theorem" title="Schröder–Bernstein theorem">Schröder–Bernstein theorem</a></li> <li><a href="/wiki/Isomorphism" title="Isomorphism">Isomorphism</a></li> <li><a href="/wiki/G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a></li> <li><a href="/wiki/Enumeration" title="Enumeration">Enumeration</a></li> <li><a href="/wiki/Large_cardinal" title="Large cardinal">Large cardinal</a> <ul><li><a href="/wiki/Inaccessible_cardinal" title="Inaccessible cardinal">inaccessible</a></li></ul></li> <li><a href="/wiki/Aleph_number" title="Aleph number">Aleph number</a></li> <li><a href="/wiki/Operation_(mathematics)" title="Operation (mathematics)">Operation</a> <ul><li><a href="/wiki/Binary_operation" title="Binary operation">binary</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Set theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel</a> <ul><li><a href="/wiki/Axiom_of_choice" title="Axiom of choice">axiom of choice</a></li> <li><a href="/wiki/Continuum_hypothesis" title="Continuum hypothesis">continuum hypothesis</a></li></ul></li> <li><a href="/wiki/General_set_theory" title="General set theory">General</a></li> <li><a href="/wiki/Kripke%E2%80%93Platek_set_theory" title="Kripke–Platek set theory">Kripke–Platek</a></li> <li><a href="/wiki/Morse%E2%80%93Kelley_set_theory" title="Morse–Kelley set theory">Morse–Kelley</a></li> <li><a href="/wiki/Naive_set_theory" title="Naive set theory">Naive</a></li> <li><a href="/wiki/New_Foundations" title="New Foundations">New Foundations</a></li> <li><a href="/wiki/Tarski%E2%80%93Grothendieck_set_theory" title="Tarski–Grothendieck set theory">Tarski–Grothendieck</a></li> <li><a href="/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory" title="Von Neumann–Bernays–Gödel set theory">Von Neumann–Bernays–Gödel</a></li> <li><a href="/wiki/Ackermann_set_theory" title="Ackermann set theory">Ackermann</a></li> <li><a href="/wiki/Constructive_set_theory" title="Constructive set theory">Constructive</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Formal_system" title="Formal system">Formal systems</a> (<a href="/wiki/List_of_formal_systems" title="List of formal systems"><span style="font-size:85%;">list</span></a>),<br /><a href="/wiki/Formal_language" title="Formal language">language</a> and <a href="/wiki/Syntax_(logic)" title="Syntax (logic)">syntax</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li> <li><a href="/wiki/Arity" title="Arity">Arity</a></li> <li><a href="/wiki/Automata_theory" title="Automata theory">Automata</a></li> <li><a href="/wiki/Axiom_schema" title="Axiom schema">Axiom schema</a></li> <li><a href="/wiki/Expression_(mathematics)" title="Expression (mathematics)">Expression</a> <ul><li><a href="/wiki/Ground_expression" title="Ground expression">ground</a></li></ul></li> <li><a href="/wiki/Extension_by_new_constant_and_function_names" title="Extension by new constant and function names">Extension</a> <ul><li><a href="/wiki/Extension_by_definitions" title="Extension by definitions">by definition</a></li> <li><a href="/wiki/Conservative_extension" title="Conservative extension">conservative</a></li></ul></li> <li><a href="/wiki/Finitary_relation" title="Finitary relation">Relation</a></li> <li><a href="/wiki/Formation_rule" title="Formation rule">Formation rule</a></li> <li><a href="/wiki/Formal_grammar" title="Formal grammar">Grammar</a></li> <li><a href="/wiki/Well-formed_formula" title="Well-formed formula">Formula</a> <ul><li><a href="/wiki/Atomic_formula" title="Atomic formula">atomic</a></li> <li><a href="/wiki/Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">closed</a></li> <li><a href="/wiki/Ground_formula" class="mw-redirect" title="Ground formula">ground</a></li> <li><a href="/wiki/Open_formula" title="Open formula">open</a></li></ul></li> <li><a href="/wiki/Free_variables_and_bound_variables" title="Free variables and bound variables">Free/bound variable</a></li> <li><a href="/wiki/Formal_language" title="Formal language">Language</a></li> <li><a href="/wiki/Metalanguage" title="Metalanguage">Metalanguage</a></li> <li><a href="/wiki/Logical_connective" title="Logical connective">Logical connective</a> <ul><li><a href="/wiki/Negation" title="Negation">¬</a></li> <li><a href="/wiki/Logical_disjunction" title="Logical disjunction">∨</a></li> <li><a href="/wiki/Logical_conjunction" title="Logical conjunction">∧</a></li> <li><a href="/wiki/Material_conditional" title="Material conditional">→</a></li> <li><a href="/wiki/Logical_biconditional" title="Logical biconditional">↔</a></li> <li><a href="/wiki/Logical_equality" title="Logical equality">=</a></li></ul></li> <li><a href="/wiki/Predicate_(mathematical_logic)" title="Predicate (mathematical logic)">Predicate</a> <ul><li><a href="/wiki/Functional_predicate" title="Functional predicate">functional</a></li> <li><a href="/wiki/Predicate_variable" title="Predicate variable">variable</a></li> <li><a href="/wiki/Propositional_variable" title="Propositional variable">propositional variable</a></li></ul></li> <li><a href="/wiki/Formal_proof" title="Formal proof">Proof</a></li> <li><a href="/wiki/Quantifier_(logic)" title="Quantifier (logic)">Quantifier</a> <ul><li><a href="/wiki/Existential_quantification" title="Existential quantification">∃</a></li> <li><a href="/wiki/Uniqueness_quantification" title="Uniqueness quantification">!</a></li> <li><a href="/wiki/Universal_quantification" title="Universal quantification">∀</a></li> <li><a href="/wiki/Quantifier_rank" title="Quantifier rank">rank</a></li></ul></li> <li><a href="/wiki/Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">Sentence</a> <ul><li><a href="/wiki/Atomic_sentence" title="Atomic sentence">atomic</a></li> <li><a href="/wiki/Spectrum_of_a_sentence" title="Spectrum of a sentence">spectrum</a></li></ul></li> <li><a href="/wiki/Signature_(logic)" title="Signature (logic)">Signature</a></li> <li><a href="/wiki/String_(formal_languages)" class="mw-redirect" title="String (formal languages)">String</a></li> <li><a href="/wiki/Substitution_(logic)" title="Substitution (logic)">Substitution</a></li> <li><a href="/wiki/Symbol_(formal)" title="Symbol (formal)">Symbol</a> <ul><li><a href="/wiki/Uninterpreted_function" title="Uninterpreted function">function</a></li> <li><a href="/wiki/Logical_constant" title="Logical constant">logical/constant</a></li> <li><a href="/wiki/Non-logical_symbol" title="Non-logical symbol">non-logical</a></li> <li><a href="/wiki/Variable_(mathematics)" title="Variable (mathematics)">variable</a></li></ul></li> <li><a href="/wiki/Term_(logic)" title="Term (logic)">Term</a></li> <li><a href="/wiki/Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a> <ul><li><a href="/wiki/List_of_mathematical_theories" title="List of mathematical theories"><span style="font-size:85%;">list</span></a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><span class="nowrap">Example <a href="/wiki/Axiomatic_system" title="Axiomatic system">axiomatic<br />systems</a> <span style="font-size:85%;">(<a href="/wiki/List_of_first-order_theories" title="List of first-order theories">list</a>)</span></span></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li>of <a href="/wiki/True_arithmetic" title="True arithmetic">arithmetic</a>: <ul><li><a href="/wiki/Peano_axioms" title="Peano axioms">Peano</a></li> <li><a href="/wiki/Second-order_arithmetic" title="Second-order arithmetic">second-order</a></li> <li><a href="/wiki/Elementary_function_arithmetic" title="Elementary function arithmetic">elementary function</a></li> <li><a href="/wiki/Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">primitive recursive</a></li> <li><a href="/wiki/Robinson_arithmetic" title="Robinson arithmetic">Robinson</a></li> <li><a href="/wiki/Skolem_arithmetic" title="Skolem arithmetic">Skolem</a></li></ul></li> <li>of the <a href="/wiki/Construction_of_the_real_numbers" title="Construction of the real numbers">real numbers</a> <ul><li><a href="/wiki/Tarski%27s_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">Tarski's axiomatization</a></li></ul></li> <li>of <a href="/wiki/Axiomatization_of_Boolean_algebras" class="mw-redirect" title="Axiomatization of Boolean algebras">Boolean algebras</a> <ul><li><a href="/wiki/Boolean_algebras_canonically_defined" title="Boolean algebras canonically defined">canonical</a></li> <li><a href="/wiki/Minimal_axioms_for_Boolean_algebra" title="Minimal axioms for Boolean algebra">minimal axioms</a></li></ul></li> <li>of <a href="/wiki/Foundations_of_geometry" title="Foundations of geometry">geometry</a>: <ul><li><a href="/wiki/Euclidean_geometry" title="Euclidean geometry">Euclidean</a>: <ul><li><a href="/wiki/Euclid%27s_Elements" title="Euclid's Elements"><i>Elements</i></a></li> <li><a href="/wiki/Hilbert%27s_axioms" title="Hilbert's axioms">Hilbert's</a></li> <li><a href="/wiki/Tarski%27s_axioms" title="Tarski's axioms">Tarski's</a></li></ul></li> <li><a href="/wiki/Non-Euclidean_geometry" title="Non-Euclidean geometry">non-Euclidean</a></li></ul></li></ul> <ul><li><i><a href="/wiki/Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></i></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Proof_theory" title="Proof theory">Proof theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Formal_proof" title="Formal proof">Formal proof</a></li> <li><a href="/wiki/Natural_deduction" title="Natural deduction">Natural deduction</a></li> <li><a href="/wiki/Logical_consequence" title="Logical consequence">Logical consequence</a></li> <li><a href="/wiki/Rule_of_inference" title="Rule of inference">Rule of inference</a></li> <li><a href="/wiki/Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li> <li><a href="/wiki/Theorem" title="Theorem">Theorem</a></li> <li><a href="/wiki/Formal_system" title="Formal system">Systems</a> <ul><li><a href="/wiki/Axiomatic_system" title="Axiomatic system">axiomatic</a></li> <li><a href="/wiki/Deductive_system" class="mw-redirect" title="Deductive system">deductive</a></li> <li><a href="/wiki/Hilbert_system" title="Hilbert system">Hilbert</a> <ul><li><a href="/wiki/List_of_Hilbert_systems" class="mw-redirect" title="List of Hilbert systems">list</a></li></ul></li></ul></li> <li><a href="/wiki/Complete_theory" title="Complete theory">Complete theory</a></li> <li><a href="/wiki/Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a> (<a href="/wiki/List_of_statements_independent_of_ZFC" title="List of statements independent of ZFC">from ZFC</a>)</li> <li><a href="/wiki/Proof_of_impossibility" title="Proof of impossibility">Proof of impossibility</a></li> <li><a href="/wiki/Ordinal_analysis" title="Ordinal analysis">Ordinal analysis</a></li> <li><a href="/wiki/Reverse_mathematics" title="Reverse mathematics">Reverse mathematics</a></li> <li><a href="/wiki/Self-verifying_theories" title="Self-verifying theories">Self-verifying theories</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Model_theory" title="Model theory">Model theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a> <ul><li><a href="/wiki/Interpretation_function" class="mw-redirect" title="Interpretation function">function</a></li> <li><a href="/wiki/Interpretation_(model_theory)" title="Interpretation (model theory)">of models</a></li></ul></li> <li><a href="/wiki/Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a> <ul><li><a href="/wiki/Elementary_equivalence" title="Elementary equivalence">equivalence</a></li> <li><a href="/wiki/Finite_model_theory" title="Finite model theory">finite</a></li> <li><a href="/wiki/Saturated_model" title="Saturated model">saturated</a></li> <li><a href="/wiki/Spectrum_of_a_theory" title="Spectrum of a theory">spectrum</a></li> <li><a href="/wiki/Substructure_(mathematics)" title="Substructure (mathematics)">submodel</a></li></ul></li> <li><a href="/wiki/Non-standard_model" title="Non-standard model">Non-standard model</a> <ul><li><a href="/wiki/Non-standard_model_of_arithmetic" title="Non-standard model of arithmetic">of arithmetic</a></li></ul></li> <li><a href="/wiki/Diagram_(mathematical_logic)" title="Diagram (mathematical logic)">Diagram</a> <ul><li><a href="/wiki/Elementary_diagram" title="Elementary diagram">elementary</a></li></ul></li> <li><a href="/wiki/Categorical_theory" title="Categorical theory">Categorical theory</a></li> <li><a href="/wiki/Model_complete_theory" title="Model complete theory">Model complete theory</a></li> <li><a href="/wiki/Satisfiability" title="Satisfiability">Satisfiability</a></li> <li><a href="/wiki/Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li> <li><a href="/wiki/Strength_(mathematical_logic)" title="Strength (mathematical logic)">Strength</a></li> <li><a href="/wiki/Theories_of_truth" class="mw-redirect" title="Theories of truth">Theories of truth</a> <ul><li><a href="/wiki/Semantic_theory_of_truth" title="Semantic theory of truth">semantic</a></li> <li><a href="/wiki/Tarski%27s_theory_of_truth" class="mw-redirect" title="Tarski's theory of truth">Tarski's</a></li> <li><a href="/wiki/Kripke%27s_theory_of_truth" class="mw-redirect" title="Kripke's theory of truth">Kripke's</a></li></ul></li> <li><a href="/wiki/T-schema" title="T-schema">T-schema</a></li> <li><a href="/wiki/Transfer_principle" title="Transfer principle">Transfer principle</a></li> <li><a href="/wiki/Truth_predicate" title="Truth predicate">Truth predicate</a></li> <li><a href="/wiki/Truth_value" title="Truth value">Truth value</a></li> <li><a href="/wiki/Type_(model_theory)" title="Type (model theory)">Type</a></li> <li><a href="/wiki/Ultraproduct" title="Ultraproduct">Ultraproduct</a></li> <li><a href="/wiki/Validity_(logic)" title="Validity (logic)">Validity</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Computability_theory" title="Computability theory">Computability theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Church_encoding" title="Church encoding">Church encoding</a></li> <li><a href="/wiki/Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li> <li><a href="/wiki/Computably_enumerable_set" title="Computably enumerable set">Computably enumerable</a></li> <li><a href="/wiki/Computable_function" title="Computable function">Computable function</a></li> <li><a href="/wiki/Computable_set" title="Computable set">Computable set</a></li> <li><a href="/wiki/Decision_problem" title="Decision problem">Decision problem</a> <ul><li><a href="/wiki/Decidability_(logic)" title="Decidability (logic)">decidable</a></li> <li><a href="/wiki/Undecidable_problem" title="Undecidable problem">undecidable</a></li> <li><a href="/wiki/P_(complexity)" title="P (complexity)">P</a></li> <li><a href="/wiki/NP_(complexity)" title="NP (complexity)">NP</a></li> <li><a href="/wiki/P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a></li></ul></li> <li><a href="/wiki/Kolmogorov_complexity" title="Kolmogorov complexity">Kolmogorov complexity</a></li> <li><a href="/wiki/Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li> <li><a href="/wiki/Primitive_recursive_function" title="Primitive recursive function">Primitive recursive function</a></li> <li><a href="/wiki/Recursion" title="Recursion">Recursion</a></li> <li><a href="/wiki/Recursive_set" class="mw-redirect" title="Recursive set">Recursive set</a></li> <li><a href="/wiki/Turing_machine" title="Turing machine">Turing machine</a></li> <li><a href="/wiki/Type_theory" title="Type theory">Type theory</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Abstract_logic" title="Abstract logic">Abstract logic</a></li> <li><a href="/wiki/Algebraic_logic" title="Algebraic logic">Algebraic logic</a></li> <li><a href="/wiki/Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li> <li><a href="/wiki/Category_theory" title="Category theory">Category theory</a></li> <li><a href="/wiki/Concrete_category" title="Concrete category">Concrete</a>/<a href="/wiki/Category_(mathematics)" title="Category (mathematics)">Abstract category</a></li> <li><a href="/wiki/Category_of_sets" title="Category of sets">Category of sets</a></li> <li><a href="/wiki/History_of_logic" title="History of logic">History of logic</a></li> <li><a href="/wiki/History_of_mathematical_logic" class="mw-redirect" title="History of mathematical logic">History of mathematical logic</a> <ul><li><a href="/wiki/Timeline_of_mathematical_logic" title="Timeline of mathematical logic">timeline</a></li></ul></li> <li><a href="/wiki/Logicism" title="Logicism">Logicism</a></li> <li><a href="/wiki/Mathematical_object" title="Mathematical object">Mathematical object</a></li> <li><a href="/wiki/Philosophy_of_mathematics" title="Philosophy of mathematics">Philosophy of mathematics</a></li> <li><a href="/wiki/Supertask" title="Supertask">Supertask</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><b><span class="nowrap"><span class="noviewer" typeof="mw:File"><a href="/wiki/File:Nuvola_apps_edu_mathematics_blue-p.svg" class="mw-file-description"><img alt="icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/16px-Nuvola_apps_edu_mathematics_blue-p.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/24px-Nuvola_apps_edu_mathematics_blue-p.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/32px-Nuvola_apps_edu_mathematics_blue-p.svg.png 2x" data-file-width="128" data-file-height="128" /></a></span> </span><a href="/wiki/Portal:Mathematics" title="Portal:Mathematics">Mathematics portal</a></b></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Logic" style="padding:3px"><table class="nowraplinks hlist mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Logic" title="Template:Logic"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Logic" title="Template talk:Logic"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Logic" title="Special:EditPage/Template:Logic"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Logic" style="font-size:114%;margin:0 4em"><a href="/wiki/Logic" title="Logic">Logic</a></div></th></tr><tr><td class="navbox-abovebelow" colspan="2"><div> <ul><li><a href="/wiki/Outline_of_logic" title="Outline of logic">Outline</a></li> <li><a href="/wiki/History_of_logic" title="History of logic">History</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Major fields</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Logic_in_computer_science" title="Logic in computer science">Computer science</a></li> <li><a href="/wiki/Formal_semantics_(natural_language)" title="Formal semantics (natural language)">Formal semantics (natural language)</a></li> <li><a href="/wiki/Inference" title="Inference">Inference</a></li> <li><a href="/wiki/Philosophy_of_logic" title="Philosophy of logic">Philosophy of logic</a></li> <li><a href="/wiki/Formal_proof" title="Formal proof">Proof</a></li> <li><a href="/wiki/Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li> <li><a href="/wiki/Syntax_(logic)" title="Syntax (logic)">Syntax</a></li></ul> </div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Logics</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Classical_logic" title="Classical logic">Classical</a></li> <li><a href="/wiki/Informal_logic" title="Informal logic">Informal</a> <ul><li><a href="/wiki/Critical_thinking" title="Critical thinking">Critical thinking</a></li> <li><a href="/wiki/Reason" title="Reason">Reason</a></li></ul></li> <li><a href="/wiki/Mathematical_logic" title="Mathematical logic">Mathematical</a></li> <li><a href="/wiki/Non-classical_logic" title="Non-classical logic">Non-classical</a></li> <li><a href="/wiki/Philosophical_logic" title="Philosophical logic">Philosophical</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Argumentation_theory" title="Argumentation theory">Argumentation</a></li> <li><a href="/wiki/Metalogic" title="Metalogic">Metalogic</a></li> <li><a href="/wiki/Metamathematics" title="Metamathematics">Metamathematics</a></li> <li><a href="/wiki/Set_theory" title="Set theory">Set</a></li></ul> </div></td></tr></tbody></table><div> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Foundations</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Abductive_reasoning" title="Abductive reasoning">Abduction</a></li> <li><a href="/wiki/Analytic%E2%80%93synthetic_distinction" title="Analytic–synthetic distinction">Analytic and synthetic propositions</a></li> <li><a href="/wiki/Antecedent_(logic)" title="Antecedent (logic)">Antecedent</a></li> <li><a href="/wiki/Consequent" title="Consequent">Consequent</a></li> <li><a href="/wiki/Contradiction" title="Contradiction">Contradiction</a> <ul><li><a href="/wiki/Paradox" title="Paradox">Paradox</a></li> <li><a href="/wiki/Antinomy" title="Antinomy">Antinomy</a></li></ul></li> <li><a href="/wiki/Deductive_reasoning" title="Deductive reasoning">Deduction</a></li> <li><a href="/wiki/Deductive_closure" title="Deductive closure">Deductive closure</a></li> <li><a href="/wiki/Definition" title="Definition">Definition</a></li> <li><a href="/wiki/Description" title="Description">Description</a></li> <li><a href="/wiki/Logical_consequence" title="Logical consequence">Entailment</a> <ul><li><a href="/wiki/Entailment_(linguistics)" title="Entailment (linguistics)">Linguistic</a></li></ul></li> <li><a href="/wiki/Logical_form" title="Logical form">Form</a></li> <li><a href="/wiki/Inductive_reasoning" title="Inductive reasoning">Induction</a></li> <li><a href="/wiki/Logical_truth" title="Logical truth">Logical truth</a></li> <li><a href="/wiki/Name" title="Name">Name</a></li> <li><a href="/wiki/Necessity_and_sufficiency" title="Necessity and sufficiency">Necessity and sufficiency</a></li> <li><a href="/wiki/Premise" title="Premise">Premise</a></li> <li><a href="/wiki/Probability" title="Probability">Probability</a></li> <li><a href="/wiki/Proposition" title="Proposition">Proposition</a></li> <li><a href="/wiki/Reference" title="Reference">Reference</a></li> <li><a href="/wiki/Statement_(logic)" title="Statement (logic)">Statement</a></li> <li><a href="/wiki/Substitution_(logic)" title="Substitution (logic)">Substitution</a></li> <li><a href="/wiki/Truth" title="Truth">Truth</a></li> <li><a href="/wiki/Validity_(logic)" title="Validity (logic)">Validity</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Lists</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/Index_of_logic_articles" title="Index of logic articles">topics</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/List_of_mathematical_logic_topics" title="List of mathematical logic topics">Mathematical logic</a></li> <li><a href="/wiki/List_of_Boolean_algebra_topics" title="List of Boolean algebra topics">Boolean algebra</a></li> <li><a href="/wiki/List_of_set_theory_topics" title="List of set theory topics">Set theory</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">other</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/List_of_logicians" title="List of logicians">Logicians</a></li> <li><a href="/wiki/List_of_rules_of_inference" title="List of rules of inference">Rules of inference</a></li> <li><a href="/wiki/List_of_paradoxes" title="List of paradoxes">Paradoxes</a></li> <li><a href="/wiki/List_of_fallacies" title="List of fallacies">Fallacies</a></li> <li><a href="/wiki/List_of_logic_symbols" title="List of logic symbols">Logic symbols</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div> <ul><li><span class="nowrap"><span class="noviewer" typeof="mw:File"><span><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/18px-Socrates.png" decoding="async" width="18" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/27px-Socrates.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/36px-Socrates.png 2x" data-file-width="326" data-file-height="500" /></span></span> </span><a href="/wiki/Portal:Philosophy" title="Portal:Philosophy">Philosophy portal</a></li> <li><a href="/wiki/Category:Logic" title="Category:Logic">Category</a></li> <li><a href="/wiki/Wikipedia:WikiProject_Logic" title="Wikipedia:WikiProject Logic">WikiProject</a> (<a href="/wiki/Wikipedia_talk:WikiProject_Logic" title="Wikipedia talk:WikiProject Logic">talk</a>)</li> <li><a class="external text" href="https://en.wikipedia.org/w/index.php?title=Special:Recentchangeslinked&target=Template:Logic&hidebots=0">changes</a></li></ul> </div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Common_logical_connectives" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="3"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Logical_connectives" title="Template:Logical connectives"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Logical_connectives" title="Template talk:Logical connectives"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Logical_connectives" title="Special:EditPage/Template:Logical connectives"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Common_logical_connectives" style="font-size:114%;margin:0 4em">Common <a href="/wiki/Logical_connective" title="Logical connective">logical connectives</a></div></th></tr><tr><td colspan="2" class="navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a class="mw-selflink selflink">Tautology</a>/<a href="/wiki/Logical_truth" title="Logical truth">True</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \top }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">⊤</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \top }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cf12e436fef2365e76fcb1034a51179d8328bb33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \top }"></span></li></ul> </div></td><td class="noviewer navbox-image" rowspan="5" style="width:1px;padding:0 0 0 2px"><div><span typeof="mw:File"><a href="/wiki/File:Logical_connectives_Hasse_diagram.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Logical_connectives_Hasse_diagram.svg/80px-Logical_connectives_Hasse_diagram.svg.png" decoding="async" width="80" height="113" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Logical_connectives_Hasse_diagram.svg/120px-Logical_connectives_Hasse_diagram.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Logical_connectives_Hasse_diagram.svg/160px-Logical_connectives_Hasse_diagram.svg.png 2x" data-file-width="744" data-file-height="1052" /></a></span></div></td></tr><tr><td colspan="2" class="navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Sheffer_stroke" title="Sheffer stroke">Alternative denial</a> (<a href="/wiki/NAND_gate" title="NAND gate">NAND gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \uparrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">↑</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \uparrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ddb20b28c74cdaa09e1f101d426441da1996072f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.162ex; height:2.509ex;" alt="{\displaystyle \uparrow }"></span></li> <li><a href="/wiki/Converse_(logic)" title="Converse (logic)">Converse implication</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leftarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">←</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leftarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3c0fb4bce772117bbaf55b7ca1539ceff9ae218c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \leftarrow }"></span></li> <li><a href="/wiki/Material_conditional" title="Material conditional">Implication</a> (<a href="/wiki/IMPLY_gate" title="IMPLY gate">IMPLY gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rightarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">→</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \rightarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/53e574cc3aa5b4bf5f3f5906caf121a378eef08b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \rightarrow }"></span></li> <li><a href="/wiki/Logical_disjunction" title="Logical disjunction">Disjunction</a> (<a href="/wiki/OR_gate" title="OR gate">OR gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lor }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∨</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lor }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ab47f6b1f589aedcf14638df1d63049d233d851a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \lor }"></span></li></ul> </div></td></tr><tr><td colspan="2" class="navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Negation" title="Negation">Negation</a> (<a href="/wiki/Inverter_(logic_gate)" title="Inverter (logic gate)">NOT gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fa78fd02085d39aa58c9e47a6d4033ce41e02fad" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \neg }"></span></li> <li><a href="/wiki/Exclusive_or" title="Exclusive or">Exclusive or</a> (<a href="/wiki/XOR_gate" title="XOR gate">XOR gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \not \leftrightarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>↮</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \not \leftrightarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/363ed81fd02da85c658dde9f17737c13b7263e49" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.137ex; margin-bottom: -0.308ex; width:2.324ex; height:1.509ex;" alt="{\displaystyle \not \leftrightarrow }"></span></li> <li><a href="/wiki/Logical_biconditional" title="Logical biconditional">Biconditional</a> (<a href="/wiki/XNOR_gate" title="XNOR gate">XNOR gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leftrightarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">↔</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leftrightarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/046b918c43e05caf6624fe9b676c69ec9cd6b892" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \leftrightarrow }"></span></li> <li><a href="/wiki/Statement_(logic)" title="Statement (logic)">Statement</a> (<a href="/wiki/Digital_buffer" title="Digital buffer">Digital buffer</a>)</li></ul> </div></td></tr><tr><td colspan="2" class="navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Logical_NOR" title="Logical NOR">Joint denial</a> (<a href="/wiki/NOR_gate" title="NOR gate">NOR gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \downarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">↓</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \downarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4618f22b0f780805eb94bb407578d9bc9487947a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.162ex; height:2.509ex;" alt="{\displaystyle \downarrow }"></span></li> <li><a href="/wiki/Material_nonimplication" title="Material nonimplication">Nonimplication</a> (<a href="/wiki/NIMPLY_gate" title="NIMPLY gate">NIMPLY gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \nrightarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>↛</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \nrightarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4c458d67617e028ed10948d2dbcfef80e9e060a2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.137ex; margin-bottom: -0.308ex; width:2.324ex; height:1.509ex;" alt="{\displaystyle \nrightarrow }"></span></li> <li><a href="/wiki/Converse_nonimplication" title="Converse nonimplication">Converse nonimplication</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \nleftarrow }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>↚</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \nleftarrow }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7694c9fc8eebe8a57c8156dd3c2caf022a619439" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.137ex; margin-bottom: -0.308ex; width:2.324ex; height:1.509ex;" alt="{\displaystyle \nleftarrow }"></span></li> <li><a href="/wiki/Logical_conjunction" title="Logical conjunction">Conjunction</a> (<a href="/wiki/AND_gate" title="AND gate">AND gate</a>) <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∧</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \land }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d6823e5a222eb3ca49672818ac3d13ec607052c4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \land }"></span></li></ul> </div></td></tr><tr><td colspan="2" class="navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Contradiction" title="Contradiction">Contradiction</a>/<a href="/wiki/False_(logic)" title="False (logic)">False</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">⊥</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \bot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f282c7bc331cc3bfcf1c57f1452cc23c022f58de" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \bot }"></span></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="3"><div><span class="nowrap"><span class="noviewer" typeof="mw:File"><span><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/18px-Socrates.png" decoding="async" width="18" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/27px-Socrates.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/36px-Socrates.png 2x" data-file-width="326" data-file-height="500" /></span></span> </span><a href="/wiki/Portal:Philosophy" title="Portal:Philosophy">Philosophy portal</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="‌Logical_truth_⊤" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="3"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Logical_truth" title="Template:Logical truth"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Logical_truth" title="Template talk:Logical truth"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Logical_truth" title="Special:EditPage/Template:Logical truth"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="‌Logical_truth_⊤" style="font-size:114%;margin:0 4em">‌<a href="/wiki/Logical_truth" title="Logical truth">Logical truth</a> ⊤</div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Functional:</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Truth_value" title="Truth value">truth value</a></li> <li><a href="/wiki/Truth_function" title="Truth function">truth function</a></li> <li>⊨ <a class="mw-selflink selflink">tautology</a></li></ul> </div></td><td class="noviewer navbox-image" rowspan="3" style="width:1px;padding:0 0 0 2px"><div><span typeof="mw:File"><a href="/wiki/File:Venn1001.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/4/47/Venn1001.svg/90px-Venn1001.svg.png" decoding="async" width="90" height="66" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/4/47/Venn1001.svg/135px-Venn1001.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/4/47/Venn1001.svg/180px-Venn1001.svg.png 2x" data-file-width="410" data-file-height="299" /></a></span></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Formal:</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Theory_(mathematical_logic)" title="Theory (mathematical logic)">theory</a></li> <li><a href="/wiki/Formal_proof" title="Formal proof">formal proof</a></li> <li><a href="/wiki/Theorem" title="Theorem">theorem</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Negation </th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><b>⊥</b> <a href="/wiki/False_(logic)" title="False (logic)">false</a></li> <li><a href="/wiki/Contradiction" title="Contradiction">contradiction</a></li> <li><a href="/wiki/Consistency" title="Consistency">inconsistency</a></li></ul> </div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Common_logical_symbols" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Common_logical_symbols" title="Template:Common logical symbols"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Common_logical_symbols" title="Template talk:Common logical symbols"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Common_logical_symbols" title="Special:EditPage/Template:Common logical symbols"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Common_logical_symbols" style="font-size:114%;margin:0 4em">Common <a href="/wiki/List_of_logic_symbols" title="List of logic symbols">logical symbols</a></div></th></tr><tr><td colspan="2" class="navbox-list navbox-odd" style="width:100%;padding:0;background:transparent;color:inherit;"><div style="padding:0px"><table class="navbox-columns-table" style="border-spacing: 0px; text-align:left;width:100%;"><tbody><tr style="vertical-align:top"><td class="navbox-list" style="padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Wedge_(symbol)" title="Wedge (symbol)">∧</a>  <span style="font-size:55%;"><i>or</i></span>  <a href="/wiki/Ampersand" title="Ampersand">&</a> </div> <a href="/wiki/Logical_conjunction" title="Logical conjunction">and</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Vel_(symbol)" class="mw-redirect" title="Vel (symbol)">∨</a> </div> <a href="/wiki/Logical_disjunction" title="Logical disjunction">or</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Negation" title="Negation">¬</a>  <span style="font-size:55%;"><i>or</i></span>  <a href="/wiki/Tilde" title="Tilde">~</a> </div> <a href="/wiki/Negation" title="Negation">not</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Arrow_(symbol)" title="Arrow (symbol)">→</a> </div> <a href="/wiki/Material_conditional" title="Material conditional">implies</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Horseshoe_(symbol)" title="Horseshoe (symbol)">⊃</a> </div> <a href="/wiki/Material_conditional" title="Material conditional">implies</a>,<br /><a href="/wiki/Subset" title="Subset">superset</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Arrow_(symbol)" title="Arrow (symbol)">↔</a>  <span style="font-size:55%;"><i>or</i></span>  <a href="/wiki/Triple_bar" title="Triple bar">≡</a> </div> <a href="/wiki/If_and_only_if" title="If and only if">iff</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Sheffer_stroke" title="Sheffer stroke">|</a> </div> <a href="/wiki/Sheffer_stroke" title="Sheffer stroke">nand</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Turned_A" title="Turned A">∀</a> </div> <div style="display: inline-block; line-height: 1.2em; padding: .1em 0; line-height:1.15em"><a href="/wiki/Universal_quantification" title="Universal quantification">universal<br />quantification</a></div> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Existential_quantification" title="Existential quantification">∃</a> </div> <div style="display: inline-block; line-height: 1.2em; padding: .1em 0; line-height:1.15em"><a href="/wiki/Existential_quantification" title="Existential quantification">existential<br />quantification</a></div> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Tee_(symbol)" title="Tee (symbol)">⊤</a> </div> <a href="/wiki/True_(logic)" class="mw-redirect" title="True (logic)">true</a>,<br /><a class="mw-selflink selflink">tautology</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Up_tack" title="Up tack">⊥</a> </div> <a href="/wiki/False_(logic)" title="False (logic)">false</a>,<br /><a href="/wiki/Contradiction" title="Contradiction">contradiction</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Turnstile_(symbol)" title="Turnstile (symbol)">⊢</a> </div> <a href="/wiki/Turnstile_(symbol)" title="Turnstile (symbol)">entails,<br />proves</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Double_turnstile" title="Double turnstile">⊨</a> </div> <a href="/wiki/Double_turnstile" title="Double turnstile">entails,<br />therefore</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Therefore_sign" title="Therefore sign">∴</a> </div> <a href="/wiki/Logical_consequence" title="Logical consequence">therefore</a> </div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;padding-top:0.85em;text-align:center;white-space:nowrap;padding-bottom:0.85em;width:10em;"><div> <div style="font-size:150%;margin-bottom:0.55em;"> <a href="/wiki/Therefore_sign#Similar_signs" title="Therefore sign">∵</a> </div> <a href="/wiki/Therefore_sign#Similar_signs" title="Therefore sign">because</a> </div></td></tr></tbody></table></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="nowrap"><span class="noviewer" typeof="mw:File"><span><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/18px-Socrates.png" decoding="async" width="18" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/27px-Socrates.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Socrates.png/36px-Socrates.png 2x" data-file-width="326" data-file-height="500" /></span></span> </span><a href="/wiki/Portal:Philosophy" title="Portal:Philosophy">Philosophy portal</a><br /><span class="nowrap"><span class="noviewer" typeof="mw:File"><a href="/wiki/File:Nuvola_apps_edu_mathematics_blue-p.svg" class="mw-file-description"><img alt="icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/28px-Nuvola_apps_edu_mathematics_blue-p.svg.png" decoding="async" width="28" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/42px-Nuvola_apps_edu_mathematics_blue-p.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/56px-Nuvola_apps_edu_mathematics_blue-p.svg.png 2x" data-file-width="128" data-file-height="128" /></a></span> </span><a href="/wiki/Portal:Mathematics" title="Portal:Mathematics">Mathematics portal</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"><style data-mw-deduplicate="TemplateStyles:r1038841319">.mw-parser-output .tooltip-dotted{border-bottom:1px dotted;cursor:help}</style></div><div role="navigation" class="navbox authority-control" aria-label="Navbox" style="padding:3px"><table class="nowraplinks hlist navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Help:Authority_control" title="Help:Authority control">Authority control databases</a>: National <span class="mw-valign-text-top noprint" typeof="mw:File/Frameless"><a href="https://www.wikidata.org/wiki/Q209555#identifiers" title="Edit this at Wikidata"><img alt="Edit this at Wikidata" src="//upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/10px-OOjs_UI_icon_edit-ltr-progressive.svg.png" decoding="async" width="10" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/15px-OOjs_UI_icon_edit-ltr-progressive.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/20px-OOjs_UI_icon_edit-ltr-progressive.svg.png 2x" data-file-width="20" data-file-height="20" /></a></span></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4184539-0">Germany</a></span></li><li><span class="uid"><span class="rt-commentedText tooltip tooltip-dotted" title="tautologie"><a rel="nofollow" class="external text" href="https://aleph.nkp.cz/F/?func=find-c&local_base=aut&ccl_term=ica=ph135768&CON_LNG=ENG">Czech Republic</a></span></span></li></ul></div></td></tr></tbody></table></div>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Tautology_(logic)&oldid=1254124403">https://en.wikipedia.org/w/index.php?title=Tautology_(logic)&oldid=1254124403</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/wiki/Category:Logical_expressions" title="Category:Logical expressions">Logical expressions</a></li><li><a href="/wiki/Category:Logical_truth" title="Category:Logical truth">Logical truth</a></li><li><a href="/wiki/Category:Mathematical_logic" title="Category:Mathematical logic">Mathematical logic</a></li><li><a href="/wiki/Category:Propositional_calculus" title="Category:Propositional calculus">Propositional calculus</a></li><li><a href="/wiki/Category:Propositions" title="Category:Propositions">Propositions</a></li><li><a href="/wiki/Category:Semantics" title="Category:Semantics">Semantics</a></li><li><a href="/wiki/Category:Sentences_by_type" title="Category:Sentences by type">Sentences by type</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Articles_with_short_description" title="Category:Articles with short description">Articles with short description</a></li><li><a href="/wiki/Category:Short_description_is_different_from_Wikidata" title="Category:Short description is different from Wikidata">Short description is different from Wikidata</a></li><li><a href="/wiki/Category:Articles_containing_Ancient_Greek_(to_1453)-language_text" title="Category:Articles containing Ancient Greek (to 1453)-language text">Articles containing Ancient Greek (to 1453)-language text</a></li><li><a href="/wiki/Category:Pages_that_use_a_deprecated_format_of_the_math_tags" title="Category:Pages that use a deprecated format of the math tags">Pages that use a deprecated format of the math tags</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 29 October 2024, at 14:48<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Tautology_(logic)&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-f69cdc8f6-89558","wgBackendResponseTime":1446,"wgPageParseReport":{"limitreport":{"cputime":"0.889","walltime":"1.246","ppvisitednodes":{"value":3001,"limit":1000000},"postexpandincludesize":{"value":140659,"limit":2097152},"templateargumentsize":{"value":2855,"limit":2097152},"expansiondepth":{"value":14,"limit":100},"expensivefunctioncount":{"value":7,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":89062,"limit":5000000},"entityaccesscount":{"value":1,"limit":400},"timingprofile":["100.00% 856.988 1 -total"," 22.07% 189.100 1 Template:Reflist"," 20.26% 173.605 9 Template:Navbox"," 16.24% 139.166 1 Template:Langx"," 14.07% 120.566 1 Template:Mathematical_logic"," 13.38% 114.701 2 Template:Cite_web"," 11.04% 94.571 1 Template:Short_description"," 6.77% 58.031 1 Template:Authority_control"," 6.23% 53.406 2 Template:Pagetype"," 4.04% 34.602 5 Template:Portal-inline"]},"scribunto":{"limitreport-timeusage":{"value":"0.502","limit":"10.000"},"limitreport-memusage":{"value":14200201,"limit":52428800},"limitreport-logs":"table#1 {\n [\"size\"] = \"tiny\",\n}\ntable#1 {\n}\ntable#1 {\n}\ntable#1 {\n}\ntable#1 {\n}\n"},"cachereport":{"origin":"mw-web.codfw.main-f69cdc8f6-89558","timestamp":"20241122143113","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Tautology (logic)","url":"https:\/\/en.wikipedia.org\/wiki\/Tautology_(logic)","sameAs":"http:\/\/www.wikidata.org\/entity\/Q209555","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q209555","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2006-03-24T02:29:16Z","dateModified":"2024-10-29T14:48:06Z","headline":"logical formula which is true in every possible interpretation"}</script> </body> </html>