CINXE.COM

<!DOCTYPE html> <html class="client-nojs skin-theme-clientpref-day mf-expand-sections-clientpref-0 mf-font-size-clientpref-small mw-mf-amc-clientpref-0" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Double negation - Wikipedia</title> <script>(function(){var className="client-js skin-theme-clientpref-day mf-expand-sections-clientpref-0 mf-font-size-clientpref-small mw-mf-amc-clientpref-0";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":"1151063d-b9d7-4430-beaa-27750d148725","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Double_negation","wgTitle":"Double negation","wgCurRevisionId":1232342427,"wgRevisionId":1232342427,"wgArticleId":379833, "wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Double_negation","wgRelevantArticleId":379833,"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"},"wgMFMode":"stable","wgMFAmc":false,"wgMFAmcOutreachActive":false,"wgMFAmcOutreachUserEligible":false,"wgMFLazyLoadImages":true,"wgMFEditNoticesFeatureConflict":false,"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgMFIsSupportedEditRequest":true,"wgMFScriptPath":"", "wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":8000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":true,"wgEditSubmitButtonLabelPublish":true,"wgSectionTranslationMissingLanguages":[{"lang":"ace","autonym":"Acèh","dir":"ltr"},{"lang":"ady","autonym":"адыгабзэ","dir":"ltr"},{"lang":"alt","autonym":"алтай тил","dir":"ltr"},{"lang":"am","autonym":"አማርኛ","dir":"ltr"},{"lang":"ami","autonym":"Pangcah","dir":"ltr"},{"lang":"an","autonym":"aragonés","dir":"ltr"},{"lang":"ang","autonym":"Ænglisc","dir":"ltr"},{"lang":"ann","autonym":"Obolo","dir":"ltr"},{"lang":"anp","autonym":"अंगिका","dir":"ltr"},{"lang":"ar","autonym":"العربية","dir":"rtl"},{"lang":"ary","autonym":"الدارجة","dir":"rtl"},{"lang":"arz","autonym":"مصرى","dir":"rtl"},{"lang":"as","autonym":"অসমীয়া","dir":"ltr"},{"lang":"ast","autonym":"asturianu","dir":"ltr"},{"lang":"av","autonym":"авар","dir":"ltr"},{"lang":"avk","autonym": "Kotava","dir":"ltr"},{"lang":"awa","autonym":"अवधी","dir":"ltr"},{"lang":"ay","autonym":"Aymar aru","dir":"ltr"},{"lang":"az","autonym":"azərbaycanca","dir":"ltr"},{"lang":"azb","autonym":"تۆرکجه","dir":"rtl"},{"lang":"ba","autonym":"башҡортса","dir":"ltr"},{"lang":"ban","autonym":"Basa Bali","dir":"ltr"},{"lang":"bar","autonym":"Boarisch","dir":"ltr"},{"lang":"bbc","autonym":"Batak Toba","dir":"ltr"},{"lang":"bcl","autonym":"Bikol Central","dir":"ltr"},{"lang":"bdr","autonym":"Bajau Sama","dir":"ltr"},{"lang":"be","autonym":"беларуская","dir":"ltr"},{"lang":"bew","autonym":"Betawi","dir":"ltr"},{"lang":"bg","autonym":"български","dir":"ltr"},{"lang":"bho","autonym":"भोजपुरी","dir":"ltr"},{"lang":"bi","autonym":"Bislama","dir":"ltr"},{"lang":"bjn","autonym":"Banjar","dir":"ltr"},{"lang":"blk","autonym":"ပအိုဝ်ႏဘာႏသာႏ","dir":"ltr"},{"lang":"bm","autonym":"bamanankan","dir":"ltr"},{"lang":"bn","autonym": "বাংলা","dir":"ltr"},{"lang":"bo","autonym":"བོད་ཡིག","dir":"ltr"},{"lang":"bpy","autonym":"বিষ্ণুপ্রিয়া মণিপুরী","dir":"ltr"},{"lang":"br","autonym":"brezhoneg","dir":"ltr"},{"lang":"bs","autonym":"bosanski","dir":"ltr"},{"lang":"btm","autonym":"Batak Mandailing","dir":"ltr"},{"lang":"bug","autonym":"Basa Ugi","dir":"ltr"},{"lang":"ca","autonym":"català","dir":"ltr"},{"lang":"cdo","autonym":"閩東語 / Mìng-dĕ̤ng-ngṳ̄","dir":"ltr"},{"lang":"ce","autonym":"нохчийн","dir":"ltr"},{"lang":"ceb","autonym":"Cebuano","dir":"ltr"},{"lang":"ch","autonym":"Chamoru","dir":"ltr"},{"lang":"chr","autonym":"ᏣᎳᎩ","dir":"ltr"},{"lang":"ckb","autonym":"کوردی","dir":"rtl"},{"lang":"co","autonym":"corsu","dir":"ltr"},{"lang":"cr","autonym":"Nēhiyawēwin / ᓀᐦᐃᔭᐍᐏᐣ","dir":"ltr"},{"lang":"crh","autonym":"qırımtatarca","dir":"ltr"},{"lang":"cs","autonym":"čeština","dir":"ltr"},{"lang":"cu","autonym": "словѣньскъ / ⰔⰎⰑⰂⰡⰐⰠⰔⰍⰟ","dir":"ltr"},{"lang":"cy","autonym":"Cymraeg","dir":"ltr"},{"lang":"da","autonym":"dansk","dir":"ltr"},{"lang":"dag","autonym":"dagbanli","dir":"ltr"},{"lang":"de","autonym":"Deutsch","dir":"ltr"},{"lang":"dga","autonym":"Dagaare","dir":"ltr"},{"lang":"din","autonym":"Thuɔŋjäŋ","dir":"ltr"},{"lang":"diq","autonym":"Zazaki","dir":"ltr"},{"lang":"dsb","autonym":"dolnoserbski","dir":"ltr"},{"lang":"dtp","autonym":"Kadazandusun","dir":"ltr"},{"lang":"dv","autonym":"ދިވެހިބަސް","dir":"rtl"},{"lang":"dz","autonym":"ཇོང་ཁ","dir":"ltr"},{"lang":"ee","autonym":"eʋegbe","dir":"ltr"},{"lang":"el","autonym":"Ελληνικά","dir":"ltr"},{"lang":"eml","autonym":"emiliàn e rumagnòl","dir":"ltr"},{"lang":"eo","autonym":"Esperanto","dir":"ltr"},{"lang":"et","autonym":"eesti","dir":"ltr"},{"lang":"eu","autonym":"euskara","dir":"ltr"},{"lang":"fat","autonym":"mfantse","dir":"ltr"},{"lang":"ff","autonym":"Fulfulde","dir" :"ltr"},{"lang":"fi","autonym":"suomi","dir":"ltr"},{"lang":"fj","autonym":"Na Vosa Vakaviti","dir":"ltr"},{"lang":"fo","autonym":"føroyskt","dir":"ltr"},{"lang":"fon","autonym":"fɔ̀ngbè","dir":"ltr"},{"lang":"fr","autonym":"français","dir":"ltr"},{"lang":"frp","autonym":"arpetan","dir":"ltr"},{"lang":"frr","autonym":"Nordfriisk","dir":"ltr"},{"lang":"fur","autonym":"furlan","dir":"ltr"},{"lang":"fy","autonym":"Frysk","dir":"ltr"},{"lang":"gag","autonym":"Gagauz","dir":"ltr"},{"lang":"gan","autonym":"贛語","dir":"ltr"},{"lang":"gcr","autonym":"kriyòl gwiyannen","dir":"ltr"},{"lang":"gl","autonym":"galego","dir":"ltr"},{"lang":"glk","autonym":"گیلکی","dir":"rtl"},{"lang":"gn","autonym":"Avañe'ẽ","dir":"ltr"},{"lang":"gom","autonym":"गोंयची कोंकणी / Gõychi Konknni","dir":"ltr"},{"lang":"gor","autonym":"Bahasa Hulontalo","dir":"ltr"},{"lang":"gpe","autonym":"Ghanaian Pidgin","dir":"ltr"},{"lang":"gu","autonym":"ગુજરાતી","dir":"ltr"},{ "lang":"guc","autonym":"wayuunaiki","dir":"ltr"},{"lang":"gur","autonym":"farefare","dir":"ltr"},{"lang":"guw","autonym":"gungbe","dir":"ltr"},{"lang":"gv","autonym":"Gaelg","dir":"ltr"},{"lang":"ha","autonym":"Hausa","dir":"ltr"},{"lang":"hak","autonym":"客家語 / Hak-kâ-ngî","dir":"ltr"},{"lang":"haw","autonym":"Hawaiʻi","dir":"ltr"},{"lang":"he","autonym":"עברית","dir":"rtl"},{"lang":"hi","autonym":"हिन्दी","dir":"ltr"},{"lang":"hif","autonym":"Fiji Hindi","dir":"ltr"},{"lang":"hr","autonym":"hrvatski","dir":"ltr"},{"lang":"hsb","autonym":"hornjoserbsce","dir":"ltr"},{"lang":"ht","autonym":"Kreyòl ayisyen","dir":"ltr"},{"lang":"hu","autonym":"magyar","dir":"ltr"},{"lang":"hyw","autonym":"Արեւմտահայերէն","dir":"ltr"},{"lang":"ia","autonym":"interlingua","dir":"ltr"},{"lang":"iba","autonym":"Jaku Iban","dir":"ltr"},{"lang":"ie","autonym":"Interlingue","dir":"ltr"},{"lang":"ig","autonym":"Igbo","dir":"ltr"},{"lang":"igl","autonym":"Igala","dir": "ltr"},{"lang":"ilo","autonym":"Ilokano","dir":"ltr"},{"lang":"io","autonym":"Ido","dir":"ltr"},{"lang":"is","autonym":"íslenska","dir":"ltr"},{"lang":"iu","autonym":"ᐃᓄᒃᑎᑐᑦ / inuktitut","dir":"ltr"},{"lang":"ja","autonym":"日本語","dir":"ltr"},{"lang":"jam","autonym":"Patois","dir":"ltr"},{"lang":"jv","autonym":"Jawa","dir":"ltr"},{"lang":"ka","autonym":"ქართული","dir":"ltr"},{"lang":"kaa","autonym":"Qaraqalpaqsha","dir":"ltr"},{"lang":"kab","autonym":"Taqbaylit","dir":"ltr"},{"lang":"kbd","autonym":"адыгэбзэ","dir":"ltr"},{"lang":"kbp","autonym":"Kabɩyɛ","dir":"ltr"},{"lang":"kcg","autonym":"Tyap","dir":"ltr"},{"lang":"kg","autonym":"Kongo","dir":"ltr"},{"lang":"kge","autonym":"Kumoring","dir":"ltr"},{"lang":"ki","autonym":"Gĩkũyũ","dir":"ltr"},{"lang":"kk","autonym":"қазақша","dir":"ltr"},{"lang":"kl","autonym":"kalaallisut","dir":"ltr"},{"lang":"km","autonym":"ភាសាខ្មែរ","dir":"ltr"},{"lang":"kn","autonym": "ಕನ್ನಡ","dir":"ltr"},{"lang":"koi","autonym":"перем коми","dir":"ltr"},{"lang":"krc","autonym":"къарачай-малкъар","dir":"ltr"},{"lang":"ks","autonym":"कॉशुर / کٲشُر","dir":"rtl"},{"lang":"ku","autonym":"kurdî","dir":"ltr"},{"lang":"kus","autonym":"Kʋsaal","dir":"ltr"},{"lang":"kv","autonym":"коми","dir":"ltr"},{"lang":"kw","autonym":"kernowek","dir":"ltr"},{"lang":"ky","autonym":"кыргызча","dir":"ltr"},{"lang":"lad","autonym":"Ladino","dir":"ltr"},{"lang":"lb","autonym":"Lëtzebuergesch","dir":"ltr"},{"lang":"lez","autonym":"лезги","dir":"ltr"},{"lang":"lg","autonym":"Luganda","dir":"ltr"},{"lang":"li","autonym":"Limburgs","dir":"ltr"},{"lang":"lij","autonym":"Ligure","dir":"ltr"},{"lang":"lld","autonym":"Ladin","dir":"ltr"},{"lang":"lmo","autonym":"lombard","dir":"ltr"},{"lang":"ln","autonym":"lingála","dir":"ltr"},{"lang":"lo","autonym":"ລາວ","dir":"ltr"},{"lang":"lt","autonym":"lietuvių","dir":"ltr"},{"lang" :"ltg","autonym":"latgaļu","dir":"ltr"},{"lang":"lv","autonym":"latviešu","dir":"ltr"},{"lang":"mad","autonym":"Madhurâ","dir":"ltr"},{"lang":"mai","autonym":"मैथिली","dir":"ltr"},{"lang":"map-bms","autonym":"Basa Banyumasan","dir":"ltr"},{"lang":"mdf","autonym":"мокшень","dir":"ltr"},{"lang":"mg","autonym":"Malagasy","dir":"ltr"},{"lang":"mhr","autonym":"олык марий","dir":"ltr"},{"lang":"mi","autonym":"Māori","dir":"ltr"},{"lang":"min","autonym":"Minangkabau","dir":"ltr"},{"lang":"mk","autonym":"македонски","dir":"ltr"},{"lang":"ml","autonym":"മലയാളം","dir":"ltr"},{"lang":"mn","autonym":"монгол","dir":"ltr"},{"lang":"mni","autonym":"ꯃꯤꯇꯩ ꯂꯣꯟ","dir":"ltr"},{"lang":"mnw","autonym":"ဘာသာမန်","dir":"ltr"},{"lang":"mos","autonym":"moore","dir":"ltr"},{"lang":"mr","autonym":"मराठी","dir":"ltr"},{"lang":"mrj","autonym":"кырык мары","dir":"ltr"},{"lang":"ms","autonym":"Bahasa Melayu", "dir":"ltr"},{"lang":"mt","autonym":"Malti","dir":"ltr"},{"lang":"mwl","autonym":"Mirandés","dir":"ltr"},{"lang":"my","autonym":"မြန်မာဘာသာ","dir":"ltr"},{"lang":"myv","autonym":"эрзянь","dir":"ltr"},{"lang":"mzn","autonym":"مازِرونی","dir":"rtl"},{"lang":"nah","autonym":"Nāhuatl","dir":"ltr"},{"lang":"nan","autonym":"閩南語 / Bân-lâm-gú","dir":"ltr"},{"lang":"nap","autonym":"Napulitano","dir":"ltr"},{"lang":"nb","autonym":"norsk bokmål","dir":"ltr"},{"lang":"nds","autonym":"Plattdüütsch","dir":"ltr"},{"lang":"nds-nl","autonym":"Nedersaksies","dir":"ltr"},{"lang":"ne","autonym":"नेपाली","dir":"ltr"},{"lang":"new","autonym":"नेपाल भाषा","dir":"ltr"},{"lang":"nia","autonym":"Li Niha","dir":"ltr"},{"lang":"nl","autonym":"Nederlands","dir":"ltr"},{"lang":"nn","autonym":"norsk nynorsk","dir":"ltr"},{"lang":"nqo","autonym":"ߒߞߏ","dir":"rtl"},{"lang":"nr","autonym":"isiNdebele seSewula","dir":"ltr"},{"lang":"nso", "autonym":"Sesotho sa Leboa","dir":"ltr"},{"lang":"ny","autonym":"Chi-Chewa","dir":"ltr"},{"lang":"oc","autonym":"occitan","dir":"ltr"},{"lang":"om","autonym":"Oromoo","dir":"ltr"},{"lang":"or","autonym":"ଓଡ଼ିଆ","dir":"ltr"},{"lang":"os","autonym":"ирон","dir":"ltr"},{"lang":"pa","autonym":"ਪੰਜਾਬੀ","dir":"ltr"},{"lang":"pag","autonym":"Pangasinan","dir":"ltr"},{"lang":"pam","autonym":"Kapampangan","dir":"ltr"},{"lang":"pap","autonym":"Papiamentu","dir":"ltr"},{"lang":"pcd","autonym":"Picard","dir":"ltr"},{"lang":"pcm","autonym":"Naijá","dir":"ltr"},{"lang":"pdc","autonym":"Deitsch","dir":"ltr"},{"lang":"pms","autonym":"Piemontèis","dir":"ltr"},{"lang":"pnb","autonym":"پنجابی","dir":"rtl"},{"lang":"ps","autonym":"پښتو","dir":"rtl"},{"lang":"pwn","autonym":"pinayuanan","dir":"ltr"},{"lang":"qu","autonym":"Runa Simi","dir":"ltr"},{"lang":"rm","autonym":"rumantsch","dir":"ltr"},{"lang":"rn","autonym":"ikirundi","dir":"ltr"},{"lang":"ro","autonym": "română","dir":"ltr"},{"lang":"rsk","autonym":"руски","dir":"ltr"},{"lang":"rue","autonym":"русиньскый","dir":"ltr"},{"lang":"rup","autonym":"armãneashti","dir":"ltr"},{"lang":"rw","autonym":"Ikinyarwanda","dir":"ltr"},{"lang":"sa","autonym":"संस्कृतम्","dir":"ltr"},{"lang":"sah","autonym":"саха тыла","dir":"ltr"},{"lang":"sat","autonym":"ᱥᱟᱱᱛᱟᱲᱤ","dir":"ltr"},{"lang":"sc","autonym":"sardu","dir":"ltr"},{"lang":"scn","autonym":"sicilianu","dir":"ltr"},{"lang":"sco","autonym":"Scots","dir":"ltr"},{"lang":"sd","autonym":"سنڌي","dir":"rtl"},{"lang":"se","autonym":"davvisámegiella","dir":"ltr"},{"lang":"sg","autonym":"Sängö","dir":"ltr"},{"lang":"sgs","autonym":"žemaitėška","dir":"ltr"},{"lang":"sh","autonym":"srpskohrvatski / српскохрватски","dir":"ltr"},{"lang":"shi","autonym":"Taclḥit","dir":"ltr"},{"lang":"shn","autonym":"ၽႃႇသႃႇတႆး ","dir":"ltr"},{"lang":"si","autonym": "සිංහල","dir":"ltr"},{"lang":"sk","autonym":"slovenčina","dir":"ltr"},{"lang":"skr","autonym":"سرائیکی","dir":"rtl"},{"lang":"sl","autonym":"slovenščina","dir":"ltr"},{"lang":"sm","autonym":"Gagana Samoa","dir":"ltr"},{"lang":"smn","autonym":"anarâškielâ","dir":"ltr"},{"lang":"sn","autonym":"chiShona","dir":"ltr"},{"lang":"so","autonym":"Soomaaliga","dir":"ltr"},{"lang":"sq","autonym":"shqip","dir":"ltr"},{"lang":"sr","autonym":"српски / srpski","dir":"ltr"},{"lang":"srn","autonym":"Sranantongo","dir":"ltr"},{"lang":"ss","autonym":"SiSwati","dir":"ltr"},{"lang":"st","autonym":"Sesotho","dir":"ltr"},{"lang":"stq","autonym":"Seeltersk","dir":"ltr"},{"lang":"su","autonym":"Sunda","dir":"ltr"},{"lang":"sv","autonym":"svenska","dir":"ltr"},{"lang":"sw","autonym":"Kiswahili","dir":"ltr"},{"lang":"szl","autonym":"ślůnski","dir":"ltr"},{"lang":"ta","autonym":"தமிழ்","dir":"ltr"},{"lang":"tay","autonym":"Tayal","dir":"ltr"},{"lang":"tcy","autonym": "ತುಳು","dir":"ltr"},{"lang":"tdd","autonym":"ᥖᥭᥰ ᥖᥬᥲ ᥑᥨᥒᥰ","dir":"ltr"},{"lang":"te","autonym":"తెలుగు","dir":"ltr"},{"lang":"tet","autonym":"tetun","dir":"ltr"},{"lang":"th","autonym":"ไทย","dir":"ltr"},{"lang":"ti","autonym":"ትግርኛ","dir":"ltr"},{"lang":"tk","autonym":"Türkmençe","dir":"ltr"},{"lang":"tl","autonym":"Tagalog","dir":"ltr"},{"lang":"tly","autonym":"tolışi","dir":"ltr"},{"lang":"tn","autonym":"Setswana","dir":"ltr"},{"lang":"to","autonym":"lea faka-Tonga","dir":"ltr"},{"lang":"tpi","autonym":"Tok Pisin","dir":"ltr"},{"lang":"tr","autonym":"Türkçe","dir":"ltr"},{"lang":"trv","autonym":"Seediq","dir":"ltr"},{"lang":"ts","autonym":"Xitsonga","dir":"ltr"},{"lang":"tt","autonym":"татарча / tatarça","dir":"ltr"},{"lang":"tum","autonym":"chiTumbuka","dir":"ltr"},{"lang":"tw","autonym":"Twi","dir":"ltr"},{"lang":"ty","autonym":"reo tahiti","dir":"ltr"},{"lang":"tyv","autonym":"тыва дыл","dir":"ltr"},{ "lang":"udm","autonym":"удмурт","dir":"ltr"},{"lang":"ur","autonym":"اردو","dir":"rtl"},{"lang":"uz","autonym":"oʻzbekcha / ўзбекча","dir":"ltr"},{"lang":"ve","autonym":"Tshivenda","dir":"ltr"},{"lang":"vec","autonym":"vèneto","dir":"ltr"},{"lang":"vep","autonym":"vepsän kel’","dir":"ltr"},{"lang":"vi","autonym":"Tiếng Việt","dir":"ltr"},{"lang":"vls","autonym":"West-Vlams","dir":"ltr"},{"lang":"vo","autonym":"Volapük","dir":"ltr"},{"lang":"vro","autonym":"võro","dir":"ltr"},{"lang":"wa","autonym":"walon","dir":"ltr"},{"lang":"war","autonym":"Winaray","dir":"ltr"},{"lang":"wo","autonym":"Wolof","dir":"ltr"},{"lang":"wuu","autonym":"吴语","dir":"ltr"},{"lang":"xal","autonym":"хальмг","dir":"ltr"},{"lang":"xh","autonym":"isiXhosa","dir":"ltr"},{"lang":"xmf","autonym":"მარგალური","dir":"ltr"},{"lang":"yi","autonym":"ייִדיש","dir":"rtl"},{"lang":"yo","autonym":"Yorùbá","dir":"ltr"},{"lang":"yue","autonym":"粵語","dir":"ltr"},{ "lang":"za","autonym":"Vahcuengh","dir":"ltr"},{"lang":"zgh","autonym":"ⵜⴰⵎⴰⵣⵉⵖⵜ ⵜⴰⵏⴰⵡⴰⵢⵜ","dir":"ltr"},{"lang":"zh","autonym":"中文","dir":"ltr"},{"lang":"zu","autonym":"isiZulu","dir":"ltr"}],"wgSectionTranslationTargetLanguages":["ace","ady","alt","am","ami","an","ang","ann","anp","ar","ary","arz","as","ast","av","avk","awa","ay","az","azb","ba","ban","bar","bbc","bcl","bdr","be","bew","bg","bho","bi","bjn","blk","bm","bn","bo","bpy","br","bs","btm","bug","ca","cdo","ce","ceb","ch","chr","ckb","co","cr","crh","cs","cu","cy","da","dag","de","dga","din","diq","dsb","dtp","dv","dz","ee","el","eml","eo","es","et","eu","fa","fat","ff","fi","fj","fo","fon","fr","frp","frr","fur","fy","gag","gan","gcr","gl","glk","gn","gom","gor","gpe","gu","guc","gur","guw","gv","ha","hak","haw","he","hi","hif","hr","hsb","ht","hu","hy","hyw","ia","iba","ie","ig","igl","ilo","io","is","it","iu","ja","jam","jv","ka","kaa","kab","kbd","kbp","kcg","kg","kge","ki","kk","kl", "km","kn","ko","koi","krc","ks","ku","kus","kv","kw","ky","lad","lb","lez","lg","li","lij","lld","lmo","ln","lo","lt","ltg","lv","mad","mai","map-bms","mdf","mg","mhr","mi","min","mk","ml","mn","mni","mnw","mos","mr","mrj","ms","mt","mwl","my","myv","mzn","nah","nan","nap","nb","nds","nds-nl","ne","new","nia","nl","nn","nqo","nr","nso","ny","oc","om","or","os","pa","pag","pam","pap","pcd","pcm","pdc","pl","pms","pnb","ps","pt","pwn","qu","rm","rn","ro","rsk","rue","rup","rw","sa","sah","sat","sc","scn","sco","sd","se","sg","sgs","sh","shi","shn","si","sk","skr","sl","sm","smn","sn","so","sq","sr","srn","ss","st","stq","su","sv","sw","szl","ta","tay","tcy","tdd","te","tet","tg","th","ti","tk","tl","tly","tn","to","tpi","tr","trv","ts","tt","tum","tw","ty","tyv","udm","ur","uz","ve","vec","vep","vi","vls","vo","vro","wa","war","wo","wuu","xal","xh","xmf","yi","yo","yue","za","zgh","zh","zu"],"isLanguageSearcherCXEntrypointEnabled":true,"mintEntrypointLanguages":["ace","ast","azb","bcl", "bjn","bh","crh","ff","fon","ig","is","ki","ks","lmo","min","sat","ss","tn","vec"],"wgWikibaseItemId":"Q5300067","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false,"wgMinervaPermissions":{"watchable":true,"watch":false},"wgMinervaFeatures":{"beta":false,"donate":true,"mobileOptionsLink":true,"categories":false,"pageIssues":true,"talkAtTop":true,"historyInPageActions":false,"overflowSubmenu":false,"tabsOnSpecials":true,"personalMenu":false,"mainMenuExpanded":false,"echo":true,"nightMode":true},"wgMinervaDownloadNamespaces":[0]};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.minerva.styles":"ready","skins.minerva.content.styles.images":"ready","mediawiki.hlist":"ready","skins.minerva.codex.styles":"ready","skins.minerva.icons":"ready","skins.minerva.amc.styles":"ready","ext.wikimediamessages.styles":"ready","mobile.init.styles":"ready","ext.relatedArticles.styles":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","site","mediawiki.page.ready","skins.minerva.scripts","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","ext.popups","mobile.init","ext.echo.centralauth","ext.relatedArticles.readMore.bootstrap","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.cx.eventlogging.campaigns","ext.cx.entrypoints.mffrequentlanguages","ext.cx.entrypoints.languagesearcher.init","mw.externalguidance.init","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.relatedArticles.styles%7Cext.wikimediaBadges%7Cext.wikimediamessages.styles%7Cmediawiki.hlist%7Cmobile.init.styles%7Cskins.minerva.amc.styles%7Cskins.minerva.codex.styles%7Cskins.minerva.content.styles.images%7Cskins.minerva.icons%2Cstyles%7Cwikibase.client.init&only=styles&skin=minerva"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=minerva"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=minerva"> <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="theme-color" content="#eaecf0"> <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes, minimum-scale=0.25, maximum-scale=5.0"> <meta property="og:title" content="Double negation - Wikipedia"> <meta property="og:type" content="website"> <link rel="manifest" href="/w/api.php?action=webapp-manifest"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Double_negation&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/Double_negation"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Double_negation rootpage-Double_negation stable issues-group-B skin-minerva action-view skin--responsive mw-mf-amc-disabled mw-mf"><div id="mw-mf-viewport"> <div id="mw-mf-page-center"> <a class="mw-mf-page-center__mask" href="#"></a> <header class="header-container header-chrome"> <div class="minerva-header"> <nav class="navigation-drawer toggle-list view-border-box"> <input type="checkbox" id="main-menu-input" class="toggle-list__checkbox" role="button" aria-haspopup="true" aria-expanded="false" aria-labelledby="mw-mf-main-menu-button"> <label role="button" for="main-menu-input" id="mw-mf-main-menu-button" aria-hidden="true" data-event-name="ui.mainmenu" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet toggle-list__toggle"> <span class="minerva-icon minerva-icon--menu"></span> <span></span> </label> <div id="mw-mf-page-left" class="menu view-border-box"> <ul id="p-navigation" class="toggle-list__list"> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--home" href="/wiki/Main_Page" data-mw="interface"> <span class="minerva-icon minerva-icon--home"></span> <span class="toggle-list-item__label">Home</span> </a> </li> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--random" href="/wiki/Special:Random" data-mw="interface"> <span class="minerva-icon minerva-icon--die"></span> <span class="toggle-list-item__label">Random</span> </a> </li> <li class="toggle-list-item skin-minerva-list-item-jsonly"> <a class="toggle-list-item__anchor menu__item--nearby" href="/wiki/Special:Nearby" data-event-name="menu.nearby" data-mw="interface"> <span class="minerva-icon minerva-icon--mapPin"></span> <span class="toggle-list-item__label">Nearby</span> </a> </li> </ul> <ul id="p-personal" class="toggle-list__list"> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--login" href="/w/index.php?title=Special:UserLogin&returnto=Double+negation" data-event-name="menu.login" data-mw="interface"> <span class="minerva-icon minerva-icon--logIn"></span> <span class="toggle-list-item__label">Log in</span> </a> </li> </ul> <ul id="pt-preferences" class="toggle-list__list"> <li class="toggle-list-item skin-minerva-list-item-jsonly"> <a class="toggle-list-item__anchor menu__item--settings" href="/w/index.php?title=Special:MobileOptions&returnto=Double+negation" data-event-name="menu.settings" data-mw="interface"> <span class="minerva-icon minerva-icon--settings"></span> <span class="toggle-list-item__label">Settings</span> </a> </li> </ul> <ul id="p-donation" class="toggle-list__list"> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--donate" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en&utm_key=minerva" data-event-name="menu.donate" data-mw="interface"> <span class="minerva-icon minerva-icon--heart"></span> <span class="toggle-list-item__label">Donate</span> </a> </li> </ul> <ul class="hlist"> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--about" href="/wiki/Wikipedia:About" data-mw="interface"> <span class="toggle-list-item__label">About Wikipedia</span> </a> </li> <li class="toggle-list-item "> <a class="toggle-list-item__anchor menu__item--disclaimers" href="/wiki/Wikipedia:General_disclaimer" data-mw="interface"> <span class="toggle-list-item__label">Disclaimers</span> </a> </li> </ul> </div> <label class="main-menu-mask" for="main-menu-input"></label> </nav> <div class="branding-box"> <a href="/wiki/Main_Page"> <span><img src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" alt="Wikipedia" width="120" height="18" style="width: 7.5em; height: 1.125em;"/> </span> </a> </div> <form action="/w/index.php" method="get" class="minerva-search-form"> <div class="search-box"> <input type="hidden" name="title" value="Special:Search"/> <input class="search skin-minerva-search-trigger" id="searchInput" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f"> <span class="search-box-icon-overlay"><span class="minerva-icon minerva-icon--search"></span> </span> </div> <button id="searchIcon" class="cdx-button cdx-button--size-large cdx-button--icon-only cdx-button--weight-quiet skin-minerva-search-trigger"> <span class="minerva-icon minerva-icon--search"></span> <span>Search</span> </button> </form> <nav class="minerva-user-navigation" aria-label="User navigation"> </nav> </div> </header> <main id="content" class="mw-body"> <div class="banner-container"> <div id="siteNotice"></div> </div> <div class="pre-content heading-holder"> <div class="page-heading"> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Double negation</span></h1> <div class="tagline"></div> </div> <ul id="p-associated-pages" class="minerva__tab-container"> <li class="minerva__tab selected"> <a class="minerva__tab-text" href="/wiki/Double_negation" rel="" data-event-name="tabs.subject">Article</a> </li> <li class="minerva__tab "> <a class="minerva__tab-text" href="/wiki/Talk:Double_negation" rel="discussion" data-event-name="tabs.talk">Talk</a> </li> </ul> <nav class="page-actions-menu"> <ul id="p-views" class="page-actions-menu__list"> <li id="language-selector" class="page-actions-menu__list-item"> <a role="button" href="#p-lang" data-mw="interface" data-event-name="menu.languages" title="Language" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet language-selector"> <span class="minerva-icon minerva-icon--language"></span> <span>Language</span> </a> </li> <li id="page-actions-watch" class="page-actions-menu__list-item"> <a role="button" id="ca-watch" href="/w/index.php?title=Special:UserLogin&returnto=Double+negation" data-event-name="menu.watch" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet menu__item--page-actions-watch"> <span class="minerva-icon minerva-icon--star"></span> <span>Watch</span> </a> </li> <li id="page-actions-edit" class="page-actions-menu__list-item"> <a role="button" id="ca-edit" href="/w/index.php?title=Double_negation&action=edit" data-event-name="menu.edit" data-mw="interface" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet edit-page menu__item--page-actions-edit"> <span class="minerva-icon minerva-icon--edit"></span> <span>Edit</span> </a> </li> </ul> </nav>  <div id="mw-content-subtitle"></div> </div> <div id="bodyContent" class="content"> <div id="mw-content-text" class="mw-body-content"><script>function mfTempOpenSection(id){var block=document.getElementById("mf-section-"+id);block.className+=" open-block";block.previousSibling.className+=" open-block";}</script><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><section class="mf-section-0" id="mf-section-0"> <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 the logical concept. For the linguistic concept, see <a href="/wiki/Double_negative" title="Double negative">double negative</a>.</div> <style data-mw-deduplicate="TemplateStyles:r1257001546">.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme) div:not(.notheme){background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table tr{display:table-row!important}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}</style><p>In <a href="/wiki/Propositional_calculus" title="Propositional calculus">propositional logic</a>, the <b>double negation</b> of a statement states that "it is not the case that the statement is not true". In <a href="/wiki/Classical_logic" title="Classical logic">classical logic</a>, every statement is <a href="/wiki/Logical_equivalence" title="Logical equivalence">logically equivalent</a> to its double negation, but this is not true in <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a>; this can be expressed by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign <span class="nounderlines" style="border: 1px solid var(--border-color-muted,#ddd); color: var(--color-base); background-color: var( --background-color-neutral-subtle, #fdfdfd); padding: 1px 1px;"><b>~</b></span> expresses <a href="/wiki/Negation" title="Negation">negation</a>. </p><table class="infobox vcard"><caption class="infobox-title fn" style="padding-bottom:0.2em;">Double negation</caption><tbody><tr><th scope="row" class="infobox-label">Type</th><td class="infobox-data"><a href="/wiki/Theorem" title="Theorem">Theorem</a></td></tr><tr><th scope="row" class="infobox-label">Field</th><td class="infobox-data"><style data-mw-deduplicate="TemplateStyles:r1126788409">.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}</style><div class="plainlist"> <ul><li><a href="/wiki/Propositional_calculus" title="Propositional calculus">Propositional calculus</a></li> <li><a href="/wiki/Classical_logic" title="Classical logic">Classical logic</a></li></ul> </div></td></tr><tr><th scope="row" class="infobox-label">Statement</th><td class="infobox-data">If a statement is true, then it is not the case that the statement is not true, and vice versa."</td></tr><tr><th scope="row" class="infobox-label">Symbolic statement</th><td class="infobox-data"><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\equiv \sim (\sim A)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>≡∼</mo> <mo stretchy="false">(</mo> <mo>∼</mo> <mi>A</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\equiv \sim (\sim A)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/28e32df56cc3e2ae93468149a762ce096a12e61f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.655ex; height:2.843ex;" alt="{\displaystyle A\equiv \sim (\sim A)}"></span></td></tr></tbody></table> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1126788409"><style data-mw-deduplicate="TemplateStyles:r1246091330">.mw-parser-output .sidebar{width:22em;float:right;clear:right;margin:0.5em 0 1em 1em;background:var(--background-color-neutral-subtle,#f8f9fa);border:1px solid var(--border-color-base,#a2a9b1);padding:0.2em;text-align:center;line-height:1.4em;font-size:88%;border-collapse:collapse;display:table}body.skin-minerva .mw-parser-output .sidebar{display:table!important;float:right!important;margin:0.5em 0 1em 1em!important}.mw-parser-output .sidebar-subgroup{width:100%;margin:0;border-spacing:0}.mw-parser-output .sidebar-left{float:left;clear:left;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-none{float:none;clear:both;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-outer-title{padding:0 0.4em 0.2em;font-size:125%;line-height:1.2em;font-weight:bold}.mw-parser-output .sidebar-top-image{padding:0.4em}.mw-parser-output .sidebar-top-caption,.mw-parser-output .sidebar-pretitle-with-top-image,.mw-parser-output .sidebar-caption{padding:0.2em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-pretitle{padding:0.4em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-title,.mw-parser-output .sidebar-title-with-pretitle{padding:0.2em 0.8em;font-size:145%;line-height:1.2em}.mw-parser-output .sidebar-title-with-pretitle{padding:0.1em 0.4em}.mw-parser-output .sidebar-image{padding:0.2em 0.4em 0.4em}.mw-parser-output .sidebar-heading{padding:0.1em 0.4em}.mw-parser-output .sidebar-content{padding:0 0.5em 0.4em}.mw-parser-output .sidebar-content-with-subgroup{padding:0.1em 0.4em 0.2em}.mw-parser-output .sidebar-above,.mw-parser-output .sidebar-below{padding:0.3em 0.8em;font-weight:bold}.mw-parser-output .sidebar-collapse .sidebar-above,.mw-parser-output .sidebar-collapse .sidebar-below{border-top:1px solid #aaa;border-bottom:1px solid #aaa}.mw-parser-output .sidebar-navbar{text-align:right;font-size:115%;padding:0 0.4em 0.4em}.mw-parser-output .sidebar-list-title{padding:0 0.4em;text-align:left;font-weight:bold;line-height:1.6em;font-size:105%}.mw-parser-output .sidebar-list-title-c{padding:0 0.4em;text-align:center;margin:0 3.3em}@media(max-width:640px){body.mediawiki .mw-parser-output .sidebar{width:100%!important;clear:both;float:none!important;margin-left:0!important;margin-right:0!important}}body.skin--responsive .mw-parser-output .sidebar a>img{max-width:none!important}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media print{body.ns-0 .mw-parser-output .sidebar{display:none!important}}</style><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> <p>Like the <a href="/wiki/Law_of_the_excluded_middle" class="mw-redirect" title="Law of the excluded middle">law of the excluded middle</a>, this principle is considered to be a <a href="/wiki/Law_of_thought" title="Law of thought">law of thought</a> in classical logic,<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> but it is disallowed by <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a>.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> The principle was stated as a theorem of <a href="/wiki/Propositional_calculus" title="Propositional calculus">propositional logic</a> by <a href="/wiki/Bertrand_Russell" title="Bertrand Russell">Russell</a> and <a href="/wiki/Alfred_North_Whitehead" title="Alfred North Whitehead">Whitehead</a> in <i><a href="/wiki/Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></i> as: </p> <dl><dd><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 \mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mo mathvariant="bold">∗</mo> <mn mathvariant="bold">4</mn> <mo>⋅</mo> <mn mathvariant="bold">13</mn> </mrow> <mo>.</mo> <mtext> </mtext> <mtext> </mtext> <mo>⊢</mo> <mo>.</mo> <mtext> </mtext> <mi>p</mi> <mtext> </mtext> <mo>≡</mo> <mtext> </mtext> <mo class="MJX-variant">∼</mo> <mo stretchy="false">(</mo> <mo class="MJX-variant">∼</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/66c60b2d21d01711aad35a16607c343d11328034" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.861ex; height:2.843ex;" alt="{\displaystyle \mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)}"></span><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></dd> <dd>"This is the principle of double negation, <i>i.e.</i> a proposition is equivalent of the falsehood of its negation."</dd></dl></dd></dl> <div id="toc" class="toc" role="navigation" aria-labelledby="mw-toc-heading"><input type="checkbox" role="button" id="toctogglecheckbox" class="toctogglecheckbox" style="display:none"><div class="toctitle" lang="en" dir="ltr"><h2 id="mw-toc-heading">Contents</h2><span class="toctogglespan"><label class="toctogglelabel" for="toctogglecheckbox"></label></span></div> <ul> <li class="toclevel-1 tocsection-1"><a href="#Elimination_and_introduction"><span class="tocnumber">1</span> <span class="toctext">Elimination and introduction</span></a> <ul> <li class="toclevel-2 tocsection-2"><a href="#Formal_notation"><span class="tocnumber">1.1</span> <span class="toctext">Formal notation</span></a></li> </ul> </li> <li class="toclevel-1 tocsection-3"><a href="#Proofs"><span class="tocnumber">2</span> <span class="toctext">Proofs</span></a> <ul> <li class="toclevel-2 tocsection-4"><a href="#In_classical_propositional_calculus_system"><span class="tocnumber">2.1</span> <span class="toctext">In classical propositional calculus system</span></a></li> </ul> </li> <li class="toclevel-1 tocsection-5"><a href="#See_also"><span class="tocnumber">3</span> <span class="toctext">See also</span></a></li> <li class="toclevel-1 tocsection-6"><a href="#References"><span class="tocnumber">4</span> <span class="toctext">References</span></a></li> <li class="toclevel-1 tocsection-7"><a href="#Bibliography"><span class="tocnumber">5</span> <span class="toctext">Bibliography</span></a></li> </ul> </div> </section><div class="mw-heading mw-heading2 section-heading" onclick="mfTempOpenSection(1)"><span class="indicator mf-icon mf-icon-expand mf-icon--small"></span><h2 id="Elimination_and_introduction"><span id="Double_negative_elimination"></span> Elimination and introduction</h2><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=1" title="Edit section: Elimination and introduction" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div><section class="mf-section-1 collapsible-block" id="mf-section-1"> <p><b>Double negation elimination</b> and <b>double negation introduction</b> are two <a href="/wiki/Validity_(logic)" title="Validity (logic)">valid</a> <a href="/wiki/Rules_of_replacement" class="mw-redirect" title="Rules of replacement">rules of replacement</a>. They are the <a href="/wiki/Inference" title="Inference">inferences</a> that, if <i>not not-A</i> is true, then <i>A</i> is true, and its <a href="/wiki/Converse_(logic)" title="Converse (logic)">converse</a>, that, if <i>A</i> is true, then <i>not not-A</i> is true, respectively. The rule allows one to introduce or eliminate a <a href="/wiki/Negation" title="Negation">negation</a> from a <a href="/wiki/Formal_proof" title="Formal proof">formal proof</a>. The rule is based on the equivalence of, for example, <i>It is false that it is not raining.</i> and <i>It is raining.</i> </p><p>The <i>double negation introduction</i> rule is: </p> <dl><dd><i>P <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><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" 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 }"></noscript><span class="lazy-image-placeholder" style="width: 2.324ex;height: 1.843ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" data-alt="{\displaystyle \Rightarrow }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></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 \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><noscript><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 }"></noscript><span class="lazy-image-placeholder" style="width: 1.55ex;height: 1.176ex;vertical-align: 0.204ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fa78fd02085d39aa58c9e47a6d4033ce41e02fad" data-alt="{\displaystyle \neg }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></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 \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><noscript><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 }"></noscript><span class="lazy-image-placeholder" style="width: 1.55ex;height: 1.176ex;vertical-align: 0.204ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fa78fd02085d39aa58c9e47a6d4033ce41e02fad" data-alt="{\displaystyle \neg }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>P</i></dd></dl> <p>and the <i>double negation elimination</i> rule is: </p> <dl><dd><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 \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><noscript><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 }"></noscript><span class="lazy-image-placeholder" style="width: 1.55ex;height: 1.176ex;vertical-align: 0.204ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fa78fd02085d39aa58c9e47a6d4033ce41e02fad" data-alt="{\displaystyle \neg }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></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 \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><noscript><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 }"></noscript><span class="lazy-image-placeholder" style="width: 1.55ex;height: 1.176ex;vertical-align: 0.204ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fa78fd02085d39aa58c9e47a6d4033ce41e02fad" data-alt="{\displaystyle \neg }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>P <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><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" 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 }"></noscript><span class="lazy-image-placeholder" style="width: 2.324ex;height: 1.843ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" data-alt="{\displaystyle \Rightarrow }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> P</i></dd></dl> <p>Where "<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><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" 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 }"></noscript><span class="lazy-image-placeholder" style="width: 2.324ex;height: 1.843ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/469b737d167b9b28a74e27c7f5e35b5ea9256100" data-alt="{\displaystyle \Rightarrow }" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>" is a <a href="/wiki/Metalogic" title="Metalogic">metalogical</a> <a href="/wiki/Symbol_(formal)" title="Symbol (formal)">symbol</a> representing "can be replaced in a proof with." </p><p>In logics that have both rules, negation is an <a href="/wiki/Involution_(mathematics)" title="Involution (mathematics)">involution</a>. </p> <div class="mw-heading mw-heading3"><h3 id="Formal_notation">Formal notation</h3><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=2" title="Edit section: Formal notation" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div> <p>The <i>double negation introduction</i> rule may be written in <a href="/wiki/Sequent" title="Sequent">sequent</a> notation: </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 P\vdash \neg \neg P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>P</mi> <mo>⊢</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle P\vdash \neg \neg P}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7ffa1c8b78753c797f3a6b31ca896054ae8ada39" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:9.302ex; height:2.176ex;" alt="{\displaystyle P\vdash \neg \neg P}"></noscript><span class="lazy-image-placeholder" style="width: 9.302ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7ffa1c8b78753c797f3a6b31ca896054ae8ada39" data-alt="{\displaystyle P\vdash \neg \neg P}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>The <i>double negation elimination</i> rule may be written as: </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 P\vdash P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> <mo>⊢</mo> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg P\vdash P}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2b03e6b1b249f88e59663057ac3c30f0776681de" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:9.302ex; height:2.176ex;" alt="{\displaystyle \neg \neg P\vdash P}"></noscript><span class="lazy-image-placeholder" style="width: 9.302ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2b03e6b1b249f88e59663057ac3c30f0776681de" data-alt="{\displaystyle \neg \neg P\vdash P}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>In <a href="/wiki/Inference_rule" class="mw-redirect" title="Inference rule">rule form</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 {\frac {P}{\neg \neg P}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mfrac> <mi>P</mi> <mrow> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> </mrow> </mfrac> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\frac {P}{\neg \neg P}}}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1118f5b15e2b6a1748d43f45f10835cdca6f8faf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.838ex; width:5.682ex; height:5.176ex;" alt="{\displaystyle {\frac {P}{\neg \neg P}}}"></noscript><span class="lazy-image-placeholder" style="width: 5.682ex;height: 5.176ex;vertical-align: -1.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1118f5b15e2b6a1748d43f45f10835cdca6f8faf" data-alt="{\displaystyle {\frac {P}{\neg \neg P}}}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>and </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 {\frac {\neg \neg P}{P}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mfrac> <mrow> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> </mrow> <mi>P</mi> </mfrac> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\frac {\neg \neg P}{P}}}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d53c0ebf22b7f898986f977050edd5278194aa27" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.838ex; width:5.682ex; height:5.176ex;" alt="{\displaystyle {\frac {\neg \neg P}{P}}}"></noscript><span class="lazy-image-placeholder" style="width: 5.682ex;height: 5.176ex;vertical-align: -1.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d53c0ebf22b7f898986f977050edd5278194aa27" data-alt="{\displaystyle {\frac {\neg \neg P}{P}}}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>or as a <a href="/wiki/Tautology_(logic)" title="Tautology (logic)">tautology</a> (plain propositional calculus 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 P\to \neg \neg P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>P</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle P\to \neg \neg P}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/40e39162b78925788231e8debe44919114fc445e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.206ex; height:2.176ex;" alt="{\displaystyle P\to \neg \neg P}"></noscript><span class="lazy-image-placeholder" style="width: 10.206ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/40e39162b78925788231e8debe44919114fc445e" data-alt="{\displaystyle P\to \neg \neg P}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>and </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 P\to P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> <mo stretchy="false">→</mo> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg P\to P}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d80b5d10118d07d51d53e832629d7a386057fc5c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.206ex; height:2.176ex;" alt="{\displaystyle \neg \neg P\to P}"></noscript><span class="lazy-image-placeholder" style="width: 10.206ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d80b5d10118d07d51d53e832629d7a386057fc5c" data-alt="{\displaystyle \neg \neg P\to P}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>These can be combined into a single biconditional 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 \neg \neg P\leftrightarrow P}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>P</mi> <mo stretchy="false">↔</mo> <mi>P</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg P\leftrightarrow P}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/91406484cc7451c9c9c739aa0b51893048035b0e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.206ex; height:2.176ex;" alt="{\displaystyle \neg \neg P\leftrightarrow P}"></noscript><span class="lazy-image-placeholder" style="width: 10.206ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/91406484cc7451c9c9c739aa0b51893048035b0e" data-alt="{\displaystyle \neg \neg P\leftrightarrow P}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>.</dd></dl> <p>Since biconditionality is an <a href="/wiki/Equivalence_relation" title="Equivalence relation">equivalence relation</a>, any instance of ¬¬<i>A</i> in a <a href="/wiki/Well-formed_formula" title="Well-formed formula">well-formed formula</a> can be replaced by <i>A</i>, leaving unchanged the <a href="/wiki/Truth-value" class="mw-redirect" title="Truth-value">truth-value</a> of the well-formed formula. </p><p>Double negative elimination is a theorem of <a href="/wiki/Classical_logic" title="Classical logic">classical logic</a>, but not of weaker logics such as <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a> and <a href="/wiki/Minimal_logic" title="Minimal logic">minimal logic</a>. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is <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 \neg A\vdash \neg A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>A</mi> <mo>⊢</mo> <mi mathvariant="normal">¬</mi> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg \neg A\vdash \neg A}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0d7777066102156644dece549eadd293e793a644" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:12.398ex; height:2.176ex;" alt="{\displaystyle \neg \neg \neg A\vdash \neg A}"></noscript><span class="lazy-image-placeholder" style="width: 12.398ex;height: 2.176ex;vertical-align: -0.338ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0d7777066102156644dece549eadd293e793a644" data-alt="{\displaystyle \neg \neg \neg A\vdash \neg A}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>. </p><p>Because of their constructive character, a statement such as <i>It's not the case that it's not raining</i> is weaker than <i>It's raining.</i> The latter requires a proof of rain, whereas the former merely requires a proof that rain would not be contradictory. This distinction also arises in natural language in the form of <a href="/wiki/Litotes" title="Litotes">litotes</a>. </p> </section><div class="mw-heading mw-heading2 section-heading" onclick="mfTempOpenSection(2)"><span class="indicator mf-icon mf-icon-expand mf-icon--small"></span><h2 id="Proofs">Proofs</h2><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=3" title="Edit section: Proofs" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div><section class="mf-section-2 collapsible-block" id="mf-section-2"> <div class="mw-heading mw-heading3"><h3 id="In_classical_propositional_calculus_system">In classical propositional calculus system</h3><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=4" title="Edit section: In classical propositional calculus system" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div> <p>In <a href="/wiki/Hilbert_system" title="Hilbert system">Hilbert-style deductive systems</a> for propositional logic, double negation is not always taken as an axiom (see <a href="/wiki/List_of_Hilbert_systems" class="mw-redirect" title="List of Hilbert systems">list of Hilbert systems</a>), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by <a href="/wiki/Jan_%C5%81ukasiewicz" title="Jan Łukasiewicz">Jan Łukasiewicz</a>: </p> <dl><dd>A1. <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 \phi \to \left(\psi \to \phi \right)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mrow> <mo>(</mo> <mrow> <mi>ψ</mi> <mo stretchy="false">→</mo> <mi>ϕ</mi> </mrow> <mo>)</mo> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \phi \to \left(\psi \to \phi \right)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/24333bbf801ca1613550143fc97a2d34c954139f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.321ex; height:2.843ex;" alt="{\displaystyle \phi \to \left(\psi \to \phi \right)}"></noscript><span class="lazy-image-placeholder" style="width: 13.321ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/24333bbf801ca1613550143fc97a2d34c954139f" data-alt="{\displaystyle \phi \to \left(\psi \to \phi \right)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd> <dd>A2. <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 \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow> <mo>(</mo> <mrow> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mrow> <mo>(</mo> <mrow> <mi>ψ</mi> <mo stretchy="false">→</mo> <mi>ξ</mi> </mrow> <mo>)</mo> </mrow> </mrow> <mo>)</mo> </mrow> <mo stretchy="false">→</mo> <mrow> <mo>(</mo> <mrow> <mrow> <mo>(</mo> <mrow> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mi>ψ</mi> </mrow> <mo>)</mo> </mrow> <mo stretchy="false">→</mo> <mrow> <mo>(</mo> <mrow> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mi>ξ</mi> </mrow> <mo>)</mo> </mrow> </mrow> <mo>)</mo> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0c9dd8563e60109bc5cb573b3b0903827ea05bf0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:39.974ex; height:2.843ex;" alt="{\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}"></noscript><span class="lazy-image-placeholder" style="width: 39.974ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0c9dd8563e60109bc5cb573b3b0903827ea05bf0" data-alt="{\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd> <dd>A3. <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 \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow> <mo>(</mo> <mrow> <mi mathvariant="normal">¬</mi> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>ψ</mi> </mrow> <mo>)</mo> </mrow> <mo stretchy="false">→</mo> <mrow> <mo>(</mo> <mrow> <mi>ψ</mi> <mo stretchy="false">→</mo> <mi>ϕ</mi> </mrow> <mo>)</mo> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a74da76a538fd97ba30e37fe304ef7da1d7dbd91" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.359ex; height:2.843ex;" alt="{\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}"></noscript><span class="lazy-image-placeholder" style="width: 23.359ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a74da76a538fd97ba30e37fe304ef7da1d7dbd91" data-alt="{\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>We use the lemma <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 p\to p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> <mo stretchy="false">→</mo> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p\to p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/edf3d9dfaa106174c31fe6f412ad65c67ea3afbe" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:6.042ex; height:2.176ex;" alt="{\displaystyle p\to p}"></noscript><span class="lazy-image-placeholder" style="width: 6.042ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/edf3d9dfaa106174c31fe6f412ad65c67ea3afbe" data-alt="{\displaystyle p\to p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> proved <a href="/wiki/Propositional_calculus#Proof_example_in_P2" title="Propositional calculus">here</a>, which we refer to as (L1), and use the following additional lemma, proved <a href="/wiki/Hilbert_system#Some_useful_theorems_and_their_proofs" title="Hilbert system">here</a>: </p> <dl><dd>(L2) <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 p\to ((p\to q)\to q)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>p</mi> <mo stretchy="false">→</mo> <mi>q</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>q</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p\to ((p\to q)\to q)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/83f3d98c9ede603036d39b606989fcfc72e08f73" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:19.028ex; height:2.843ex;" alt="{\displaystyle p\to ((p\to q)\to q)}"></noscript><span class="lazy-image-placeholder" style="width: 19.028ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/83f3d98c9ede603036d39b606989fcfc72e08f73" data-alt="{\displaystyle p\to ((p\to q)\to q)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span></dd></dl> <p>We first prove <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 p\to p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg p\to p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/79364f11891d1d8022f81a3f8d3e83c0f7499892" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.054ex; height:2.176ex;" alt="{\displaystyle \neg \neg p\to p}"></noscript><span class="lazy-image-placeholder" style="width: 9.054ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/79364f11891d1d8022f81a3f8d3e83c0f7499892" data-alt="{\displaystyle \neg \neg p\to p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>. For shortness, we denote <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 q\to (r\to q)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>q</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>r</mi> <mo stretchy="false">→</mo> <mi>q</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle q\to (r\to q)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/feac8d6400ab200772d9fe8eb363f39624c4026d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.225ex; height:2.843ex;" alt="{\displaystyle q\to (r\to q)}"></noscript><span class="lazy-image-placeholder" style="width: 12.225ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/feac8d6400ab200772d9fe8eb363f39624c4026d" data-alt="{\displaystyle q\to (r\to q)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> by φ<sub>0</sub>. We also use repeatedly the method of the <a href="/wiki/Hypothetical_syllogism#As_a_metatheorem" title="Hypothetical syllogism">hypothetical syllogism metatheorem</a> as a shorthand for several proof steps. </p> <dl><dd>(1) <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 \varphi _{0}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \varphi _{0}}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6cf63e8f16cefbe25d3d028fbb464a8c4a53cc7b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:2.574ex; height:2.176ex;" alt="{\displaystyle \varphi _{0}}"></noscript><span class="lazy-image-placeholder" style="width: 2.574ex;height: 2.176ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6cf63e8f16cefbe25d3d028fbb464a8c4a53cc7b" data-alt="{\displaystyle \varphi _{0}}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (A1))</dd> <dd>(2) <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 \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bca48395a3b3d664e89df49b556ca20f09d110f9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:31.25ex; height:2.843ex;" alt="{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}"></noscript><span class="lazy-image-placeholder" style="width: 31.25ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bca48395a3b3d664e89df49b556ca20f09d110f9" data-alt="{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (A3))</dd> <dd>(3) <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 p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e4079e53440aff66a6ad5fb03a2125e4da4f1b99" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.049ex; height:2.843ex;" alt="{\displaystyle (\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}"></noscript><span class="lazy-image-placeholder" style="width: 25.049ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e4079e53440aff66a6ad5fb03a2125e4da4f1b99" data-alt="{\displaystyle (\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (A3))</dd> <dd>(4) <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 \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/80453ccb33c016ff65e2e034363b5e86cf2c1173" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.15ex; height:2.843ex;" alt="{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}"></noscript><span class="lazy-image-placeholder" style="width: 28.15ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/80453ccb33c016ff65e2e034363b5e86cf2c1173" data-alt="{\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (from (2) and (3) by the hypothetical syllogism metatheorem)</dd> <dd>(5) <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 p\to (\neg \neg \varphi _{0}\to \neg \neg p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/126363ed01e2ce1f564be7948052230ea1ae8044" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.253ex; height:2.843ex;" alt="{\displaystyle \neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)}"></noscript><span class="lazy-image-placeholder" style="width: 23.253ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/126363ed01e2ce1f564be7948052230ea1ae8044" data-alt="{\displaystyle \neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (A1))</dd> <dd>(6) <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 p\to (\varphi _{0}\to p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg p\to (\varphi _{0}\to p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b256c977d996c39416d631307093c8c5736cc743" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.051ex; height:2.843ex;" alt="{\displaystyle \neg \neg p\to (\varphi _{0}\to p)}"></noscript><span class="lazy-image-placeholder" style="width: 17.051ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b256c977d996c39416d631307093c8c5736cc743" data-alt="{\displaystyle \neg \neg p\to (\varphi _{0}\to p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (from (4) and (5) by the hypothetical syllogism metatheorem)</dd> <dd>(7) <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 \varphi _{0}\to ((\varphi _{0}\to p)\to p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \varphi _{0}\to ((\varphi _{0}\to p)\to p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/281c419004c4d2c3e2771b3e914bed45494610a4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.948ex; height:2.843ex;" alt="{\displaystyle \varphi _{0}\to ((\varphi _{0}\to p)\to p)}"></noscript><span class="lazy-image-placeholder" style="width: 21.948ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/281c419004c4d2c3e2771b3e914bed45494610a4" data-alt="{\displaystyle \varphi _{0}\to ((\varphi _{0}\to p)\to p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (L2))</dd> <dd>(8) <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 (\varphi _{0}\to p)\to p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <msub> <mi>φ</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\varphi _{0}\to p)\to p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fd9c906eb1df7229dfa7c862df77d654b995c282" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.951ex; height:2.843ex;" alt="{\displaystyle (\varphi _{0}\to p)\to p}"></noscript><span class="lazy-image-placeholder" style="width: 13.951ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fd9c906eb1df7229dfa7c862df77d654b995c282" data-alt="{\displaystyle (\varphi _{0}\to p)\to p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (from (1) and (7) by modus ponens)</dd> <dd>(9) <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 p\to p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg p\to p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/79364f11891d1d8022f81a3f8d3e83c0f7499892" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.054ex; height:2.176ex;" alt="{\displaystyle \neg \neg p\to p}"></noscript><span class="lazy-image-placeholder" style="width: 9.054ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/79364f11891d1d8022f81a3f8d3e83c0f7499892" data-alt="{\displaystyle \neg \neg p\to p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (from (6) and (8) by the hypothetical syllogism metatheorem)</dd></dl> <p>We now prove <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 p\to \neg \neg p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p\to \neg \neg p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb56efba4129a7fd9ef620e17746d3e1c561dac9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:9.143ex; height:2.176ex;" alt="{\displaystyle p\to \neg \neg p}"></noscript><span class="lazy-image-placeholder" style="width: 9.143ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb56efba4129a7fd9ef620e17746d3e1c561dac9" data-alt="{\displaystyle p\to \neg \neg p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span>. </p> <dl><dd>(1) <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 \neg p\to \neg p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg \neg p\to \neg p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/716805a77e4f60fb09c79272ba79ffdf5f90e28e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.154ex; height:2.176ex;" alt="{\displaystyle \neg \neg \neg p\to \neg p}"></noscript><span class="lazy-image-placeholder" style="width: 12.154ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/716805a77e4f60fb09c79272ba79ffdf5f90e28e" data-alt="{\displaystyle \neg \neg \neg p\to \neg p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of the first part of the theorem we have just proven)</dd> <dd>(2) <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 \neg p\to \neg p)\to (p\to \neg \neg p)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1dfea01a0da8b3b91e134675d0173938fb2eac3e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.44ex; height:2.843ex;" alt="{\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}"></noscript><span class="lazy-image-placeholder" style="width: 28.44ex;height: 2.843ex;vertical-align: -0.838ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1dfea01a0da8b3b91e134675d0173938fb2eac3e" data-alt="{\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (instance of (A3))</dd> <dd>(3) <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 p\to \neg \neg p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p\to \neg \neg p}</annotation> </semantics> </math></span><noscript><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb56efba4129a7fd9ef620e17746d3e1c561dac9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:9.143ex; height:2.176ex;" alt="{\displaystyle p\to \neg \neg p}"></noscript><span class="lazy-image-placeholder" style="width: 9.143ex;height: 2.176ex;vertical-align: -0.671ex;" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb56efba4129a7fd9ef620e17746d3e1c561dac9" data-alt="{\displaystyle p\to \neg \neg p}" data-class="mwe-math-fallback-image-inline mw-invert skin-invert"> </span></span> (from (1) and (2) by modus ponens)</dd></dl> <p>And the proof is complete. </p> </section><div class="mw-heading mw-heading2 section-heading" onclick="mfTempOpenSection(3)"><span class="indicator mf-icon mf-icon-expand mf-icon--small"></span><h2 id="See_also">See also</h2><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=5" title="Edit section: See also" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div><section class="mf-section-3 collapsible-block" id="mf-section-3"> <ul><li><a href="/wiki/Double-negation_translation" title="Double-negation translation">Gödel–Gentzen negative translation</a></li></ul> </section><div class="mw-heading mw-heading2 section-heading" onclick="mfTempOpenSection(4)"><span class="indicator mf-icon mf-icon-expand mf-icon--small"></span><h2 id="References">References</h2><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=6" title="Edit section: References" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div><section class="mf-section-4 collapsible-block" id="mf-section-4"> <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">Hamilton is discussing <a href="/wiki/Hegel" class="mw-redirect" title="Hegel">Hegel</a> in the following: "In the more recent systems of philosophy, the universality and necessity of the axiom of Reason has, with other logical laws, been controverted and rejected by speculators on the absolute.[<i>On principle of Double Negation as another law of Thought</i>, see Fries, <i>Logik</i>, §41, p. 190; Calker, <i>Denkiehre odor Logic und Dialecktik</i>, §165, p. 453; Beneke, <i>Lehrbuch der Logic</i>, §64, p. 41.]" (Hamilton 1860:68)</span> </li> <li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">The <sup>o</sup> of Kleene's formula *49<sup>o</sup> indicates "the demonstration is not valid for both systems [classical system and intuitionistic system]", Kleene 1952:101.</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">PM 1952 reprint of 2nd edition 1927 pp. 101–02, 117.</span> </li> </ol></div></div> </section><div class="mw-heading mw-heading2 section-heading" onclick="mfTempOpenSection(5)"><span class="indicator mf-icon mf-icon-expand mf-icon--small"></span><h2 id="Bibliography">Bibliography</h2><span class="mw-editsection"> <a role="button" href="/w/index.php?title=Double_negation&action=edit&section=7" title="Edit section: Bibliography" class="cdx-button cdx-button--size-large cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--icon-only cdx-button--weight-quiet "> <span class="minerva-icon minerva-icon--edit"></span> <span>edit</span> </a> </span> </div><section class="mf-section-5 collapsible-block" id="mf-section-5"> <ul><li><a href="/wiki/Sir_William_Hamilton,_9th_Baronet" title="Sir William Hamilton, 9th Baronet">William Hamilton</a>, 1860, <i>Lectures on Metaphysics and Logic, Vol. II. Logic; Edited by Henry Mansel and John Veitch</i>, Boston, Gould and Lincoln.</li> <li><a href="/wiki/Christoph_Sigwart" class="mw-redirect" title="Christoph Sigwart">Christoph Sigwart</a>, 1895, <i>Logic: The Judgment, Concept, and Inference; Second Edition, Translated by Helen Dendy</i>, Macmillan & Co. New York.</li> <li><a href="/wiki/Stephen_C._Kleene" class="mw-redirect" title="Stephen C. Kleene">Stephen C. Kleene</a>, 1952, <i>Introduction to Metamathematics</i>, 6th reprinting with corrections 1971, North-Holland Publishing Company, Amsterdam NY, <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><a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-7204-2103-9" title="Special:BookSources/0-7204-2103-9">0-7204-2103-9</a>.</li> <li><a href="/wiki/Stephen_C._Kleene" class="mw-redirect" title="Stephen C. Kleene">Stephen C. Kleene</a>, 1967, <i>Mathematical Logic</i>, Dover edition 2002, Dover Publications, Inc, Mineola N.Y. <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/Alfred_North_Whitehead" title="Alfred North Whitehead">Alfred North Whitehead</a> and <a href="/wiki/Bertrand_Russell" title="Bertrand Russell">Bertrand Russell</a>, <i>Principia Mathematica to *56</i>, 2nd edition 1927, reprint 1962, Cambridge at the University Press.</li></ul>    </section></div> <noscript><img src="https://login.m.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1&mobile=1" 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=Double_negation&oldid=1232342427">https://en.wikipedia.org/w/index.php?title=Double_negation&oldid=1232342427</a>"</div></div> </div> <div class="post-content" id="page-secondary-actions"> </div> </main> <footer class="mw-footer minerva-footer" role="contentinfo"> <a class="last-modified-bar" href="/w/index.php?title=Double_negation&action=history"> <div class="post-content last-modified-bar__content"> <span class="minerva-icon minerva-icon-size-medium minerva-icon--modified-history"></span> <span class="last-modified-bar__text modified-enhancement" data-user-name="David Eppstein" data-user-gender="unknown" data-timestamp="1719992129"> <span>Last edited on 3 July 2024, at 07:35</span> </span> <span class="minerva-icon minerva-icon-size-small minerva-icon--expand"></span> </div> </a> <div class="post-content footer-content"> <div id='mw-data-after-content'> <div class="read-more-container"></div> </div> <div id="p-lang"> <h4>Languages</h4> <section> <ul id="p-variants" class="minerva-languages"></ul> <ul class="minerva-languages"><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/Doble_negaci%C3%B3n_(l%C3%B3gica)" title="Doble negación (lógica) – Spanish" lang="es" hreflang="es" data-title="Doble negación (lógica)" 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-fa mw-list-item"><a href="https://fa.wikipedia.org/wiki/%D9%86%D9%82%DB%8C%D8%B6_%D9%85%D8%B6%D8%A7%D8%B9%D9%81" 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-ko badge-Q70893996 mw-list-item" title=""><a href="https://ko.wikipedia.org/wiki/%EC%9D%B4%EC%A4%91_%EB%B6%80%EC%A0%95" 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-hy mw-list-item"><a href="https://hy.wikipedia.org/wiki/%D4%B2%D5%A1%D6%81%D5%A1%D5%BD%D5%B4%D5%A1%D5%B6_%D6%85%D6%80%D5%A5%D5%B6%D6%84" title="Բացասման օրենք – Armenian" lang="hy" hreflang="hy" data-title="Բացասման օրենք" data-language-autonym="Հայերեն" data-language-local-name="Armenian" class="interlanguage-link-target"><span>Հայերեն</span></a></li><li class="interlanguage-link interwiki-it mw-list-item"><a href="https://it.wikipedia.org/wiki/Doppia_negazione" title="Doppia negazione – Italian" lang="it" hreflang="it" data-title="Doppia negazione" data-language-autonym="Italiano" data-language-local-name="Italian" class="interlanguage-link-target"><span>Italiano</span></a></li><li class="interlanguage-link interwiki-pl mw-list-item"><a href="https://pl.wikipedia.org/wiki/Prawo_podw%C3%B3jnego_przeczenia" title="Prawo podwójnego przeczenia – Polish" lang="pl" hreflang="pl" data-title="Prawo podwójnego przeczenia" 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/Dupla_nega%C3%A7%C3%A3o" title="Dupla negação – Portuguese" lang="pt" hreflang="pt" data-title="Dupla negação" 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-tg mw-list-item"><a href="https://tg.wikipedia.org/wiki/%D0%98%D0%BD%D0%BA%D0%BE%D1%80%D0%B8_%D0%B8%D0%BD%D0%BA%D0%BE%D1%80" title="Инкори инкор – Tajik" lang="tg" hreflang="tg" data-title="Инкори инкор" data-language-autonym="Тоҷикӣ" data-language-local-name="Tajik" class="interlanguage-link-target"><span>Тоҷикӣ</span></a></li></ul> </section> </div> <div class="minerva-footer-logo"><img src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" alt="Wikipedia" width="120" height="18" style="width: 7.5em; height: 1.125em;"/> </div> <ul id="footer-info" class="footer-info hlist hlist-separated"> <li id="footer-info-lastmod"> This page was last edited on 3 July 2024, at 07:35<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Content is available under <a class="external" rel="nofollow" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">CC BY-SA 4.0</a> unless otherwise noted.</li> </ul> <ul id="footer-places" class="footer-places hlist hlist-separated"> <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-terms-use"><a href="https://foundation.m.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use">Terms of Use</a></li> <li id="footer-places-desktop-toggle"><a id="mw-mf-display-toggle" href="//en.wikipedia.org/w/index.php?title=Double_negation&mobileaction=toggle_view_desktop" data-event-name="switch_to_desktop">Desktop</a></li> </ul> </div> </footer> </div> </div> <div class="mw-notification-area" data-mw="interface"></div>  <script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-f69cdc8f6-828bf","wgBackendResponseTime":193,"wgPageParseReport":{"limitreport":{"cputime":"0.373","walltime":"0.516","ppvisitednodes":{"value":1199,"limit":1000000},"postexpandincludesize":{"value":17905,"limit":2097152},"templateargumentsize":{"value":1099,"limit":2097152},"expansiondepth":{"value":14,"limit":100},"expensivefunctioncount":{"value":1,"limit":500},"unstrip-depth":{"value":0,"limit":20},"unstrip-size":{"value":16349,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 370.568 1 -total"," 34.88% 129.258 1 Template:Transformation_rules"," 33.84% 125.412 1 Template:Sidebar"," 22.31% 82.665 1 Template:Short_description"," 16.28% 60.325 2 Template:ISBN"," 15.78% 58.472 1 Template:Flatlist"," 14.71% 54.523 2 Template:Pagetype"," 13.27% 49.159 2 Template:Catalog_lookup_link"," 12.44% 46.100 1 Template:Infobox_mathematical_statement"," 11.43% 42.365 1 Template:Infobox"]},"scribunto":{"limitreport-timeusage":{"value":"0.158","limit":"10.000"},"limitreport-memusage":{"value":2010803,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-f69cdc8f6-qvkwc","timestamp":"20241122150427","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Double negation","url":"https:\/\/en.wikipedia.org\/wiki\/Double_negation","sameAs":"http:\/\/www.wikidata.org\/entity\/Q5300067","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q5300067","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":"2003-11-26T09:12:31Z","dateModified":"2024-07-03T07:35:29Z","headline":"theorem"}</script><script>(window.NORLQ=window.NORLQ||[]).push(function(){var ns,i,p,img;ns=document.getElementsByTagName('noscript');for(i=0;i<ns.length;i++){p=ns[i].nextSibling;if(p&&p.className&&p.className.indexOf('lazy-image-placeholder')>-1){img=document.createElement('img');img.setAttribute('src',p.getAttribute('data-src'));img.setAttribute('width',p.getAttribute('data-width'));img.setAttribute('height',p.getAttribute('data-height'));img.setAttribute('alt',p.getAttribute('data-alt'));p.parentNode.replaceChild(img,p);}}});</script> </body> </html>