CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Constructive analysis - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"77e12a29-e262-4ce1-86b2-69ea553cfd9b","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Constructive_analysis","wgTitle":"Constructive analysis","wgCurRevisionId":1238917105,"wgRevisionId":1238917105,"wgArticleId":239851,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Articles with short description","Short description is different from Wikidata","Mathematical analysis","Constructivism (mathematics)","Intuitionism"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Constructive_analysis","wgRelevantArticleId":239851,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia", "wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":30000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q2845197","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false, "wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","ext.math.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader", "ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.math.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Constructive analysis - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Constructive_analysis"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Constructive_analysis&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/Constructive_analysis"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Constructive_analysis rootpage-Constructive_analysis skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Constructive+analysis" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Constructive+analysis" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Constructive+analysis" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Constructive+analysis" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-Introduction" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Introduction"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Introduction</span> </div> </a> <ul id="toc-Introduction-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Logical_preliminaries" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Logical_preliminaries"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>Logical preliminaries</span> </div> </a> <button aria-controls="toc-Logical_preliminaries-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Logical preliminaries subsection</span> </button> <ul id="toc-Logical_preliminaries-sublist" class="vector-toc-list"> <li id="toc-Undecidable_predicates" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Undecidable_predicates"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.1</span> <span>Undecidable predicates</span> </div> </a> <ul id="toc-Undecidable_predicates-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Order_vs._disjunctions" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Order_vs._disjunctions"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2</span> <span>Order vs. disjunctions</span> </div> </a> <ul id="toc-Order_vs._disjunctions-sublist" class="vector-toc-list"> <li id="toc-Trichotomy" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Trichotomy"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2.1</span> <span>Trichotomy</span> </div> </a> <ul id="toc-Trichotomy-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Apartness" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Apartness"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2.2</span> <span>Apartness</span> </div> </a> <ul id="toc-Apartness-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Non-strict_partial_order" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Non-strict_partial_order"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2.3</span> <span>Non-strict partial order</span> </div> </a> <ul id="toc-Non-strict_partial_order-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Variations" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Variations"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2.4</span> <span>Variations</span> </div> </a> <ul id="toc-Variations-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Invertibility" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Invertibility"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.3</span> <span>Invertibility</span> </div> </a> <ul id="toc-Invertibility-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Formalization" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Formalization"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Formalization</span> </div> </a> <button aria-controls="toc-Formalization-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Formalization subsection</span> </button> <ul id="toc-Formalization-sublist" class="vector-toc-list"> <li id="toc-Rational_sequences" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Rational_sequences"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1</span> <span>Rational sequences</span> </div> </a> <ul id="toc-Rational_sequences-sublist" class="vector-toc-list"> <li id="toc-Moduli" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Moduli"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.1</span> <span>Moduli</span> </div> </a> <ul id="toc-Moduli-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Bounds_and_suprema" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Bounds_and_suprema"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.2</span> <span>Bounds and suprema</span> </div> </a> <ul id="toc-Bounds_and_suprema-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Bishop's_formalization" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Bishop's_formalization"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.3</span> <span>Bishop's formalization</span> </div> </a> <ul id="toc-Bishop's_formalization-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Variations_2" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Variations_2"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.4</span> <span>Variations</span> </div> </a> <ul id="toc-Variations_2-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Coding" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Coding"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.5</span> <span>Coding</span> </div> </a> <ul id="toc-Coding-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Set_theory" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Set_theory"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2</span> <span>Set theory</span> </div> </a> <ul id="toc-Set_theory-sublist" class="vector-toc-list"> <li id="toc-Cauchy_reals" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Cauchy_reals"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2.1</span> <span>Cauchy reals</span> </div> </a> <ul id="toc-Cauchy_reals-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Dedekind_reals" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Dedekind_reals"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2.2</span> <span>Dedekind reals</span> </div> </a> <ul id="toc-Dedekind_reals-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Interval_arithmetic" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Interval_arithmetic"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2.3</span> <span>Interval arithmetic</span> </div> </a> <ul id="toc-Interval_arithmetic-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Uncountability" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Uncountability"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2.4</span> <span>Uncountability</span> </div> </a> <ul id="toc-Uncountability-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Category_and_type_theory" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Category_and_type_theory"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.3</span> <span>Category and type theory</span> </div> </a> <ul id="toc-Category_and_type_theory-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Principles" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Principles"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Principles</span> </div> </a> <button aria-controls="toc-Principles-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Principles subsection</span> </button> <ul id="toc-Principles-sublist" class="vector-toc-list"> <li id="toc-Anti-classical_schools" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Anti-classical_schools"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.1</span> <span>Anti-classical schools</span> </div> </a> <ul id="toc-Anti-classical_schools-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Theorems" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Theorems"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>Theorems</span> </div> </a> <button aria-controls="toc-Theorems-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Theorems subsection</span> </button> <ul id="toc-Theorems-sublist" class="vector-toc-list"> <li id="toc-The_intermediate_value_theorem" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#The_intermediate_value_theorem"> <div class="vector-toc-text"> <span class="vector-toc-numb">5.1</span> <span>The intermediate value theorem</span> </div> </a> <ul id="toc-The_intermediate_value_theorem-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-The_least-upper-bound_principle_and_compact_sets" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#The_least-upper-bound_principle_and_compact_sets"> <div class="vector-toc-text"> <span class="vector-toc-numb">5.2</span> <span>The least-upper-bound principle and compact sets</span> </div> </a> <ul id="toc-The_least-upper-bound_principle_and_compact_sets-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-See_also" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#See_also"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>See also</span> </div> </a> <ul id="toc-See_also-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">7</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Further_reading" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Further_reading"> <div class="vector-toc-text"> <span class="vector-toc-numb">8</span> <span>Further reading</span> </div> </a> <ul id="toc-Further_reading-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Constructive analysis</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 2 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-2" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">2 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Analyse_constructive" title="Analyse constructive – French" lang="fr" hreflang="fr" data-title="Analyse constructive" data-language-autonym="Français" data-language-local-name="French" class="interlanguage-link-target"><span>Français</span></a></li><li class="interlanguage-link interwiki-pt mw-list-item"><a href="https://pt.wikipedia.org/wiki/An%C3%A1lise_construtiva" title="Análise construtiva – Portuguese" lang="pt" hreflang="pt" data-title="Análise construtiva" data-language-autonym="Português" data-language-local-name="Portuguese" class="interlanguage-link-target"><span>Português</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q2845197#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Constructive_analysis" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Constructive_analysis" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Constructive_analysis"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Constructive_analysis&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Constructive_analysis&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Constructive_analysis"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Constructive_analysis&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Constructive_analysis&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Constructive_analysis" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Constructive_analysis" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages" title="A list of all special pages [q]" accesskey="q"><span>Special pages</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Constructive_analysis&oldid=1238917105" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Constructive_analysis&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Constructive_analysis&id=1238917105&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FConstructive_analysis"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FConstructive_analysis"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Constructive_analysis&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Constructive_analysis&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q2845197" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><div class="shortdescription nomobile noexcerpt noprint searchaux" style="display:none">Mathematical analysis</div> <p>In <a href="/wiki/Mathematics" title="Mathematics">mathematics</a>, <b>constructive analysis</b> is <a href="/wiki/Mathematical_analysis" title="Mathematical analysis">mathematical analysis</a> done according to some principles of <a href="/wiki/Constructive_mathematics" class="mw-redirect" title="Constructive mathematics">constructive mathematics</a>. </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Introduction">Introduction</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=1" title="Edit section: Introduction"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The name of the subject contrasts with <i>classical analysis</i>, which in this context means analysis done according to the more common principles of classical mathematics. However, there are various schools of thought and many different formalizations of constructive analysis.<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> Whether classical or constructive in some fashion, any such framework of analysis axiomatizes the <a href="/wiki/Real_number_line" class="mw-redirect" title="Real number line">real number line</a> by some means, a collection extending the <a href="/wiki/Rationals" class="mw-redirect" title="Rationals">rationals</a> and with an <a href="/wiki/Apartness_relation" title="Apartness relation">apartness relation</a> definable from an asymmetric order structure. Center stage takes a positivity predicate, here denoted <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/80d24be5f0eb4a9173da6038badc8659546021d0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x>0}"></span>, which governs an equality-to-zero <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 x\cong 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≅</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\cong 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/162b4b1fabdcd260c8fa207f376378dfc155d8dc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x\cong 0}"></span>. The members of the collection are generally just called the <i>real numbers</i>. While this term is thus overloaded in the subject, all the frameworks share a broad common core of results that are also theorems of classical analysis. </p><p>Constructive frameworks for its formulation are extensions of <a href="/wiki/Heyting_arithmetic" title="Heyting arithmetic">Heyting arithmetic</a> by types including <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 {\mathbb {N} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {N} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e6699687943087822616a37468d23367daaef9fa" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.097ex; height:2.676ex;" alt="{\displaystyle {\mathbb {N} }^{\mathbb {N} }}"></span>, constructive <a href="/wiki/Second-order_arithmetic" title="Second-order arithmetic">second-order arithmetic</a>, or strong enough <a href="/wiki/Topos_theory" class="mw-redirect" title="Topos theory">topos</a>-, <a href="/wiki/Dependent_type_theory" class="mw-redirect" title="Dependent type theory">type</a>- or <a href="/wiki/Constructive_set_theory#Analysis" title="Constructive set theory">constructive set theories</a> such as <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 {\mathsf {CZF}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">C</mi> <mi mathvariant="sans-serif">Z</mi> <mi mathvariant="sans-serif">F</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {CZF}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/68735fcc4a56810ef5e5662f4ab1a4ad4dde9e51" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.228ex; height:2.176ex;" alt="{\displaystyle {\mathsf {CZF}}}"></span>, a constructive counter-part of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathsf {ZF}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">Z</mi> <mi mathvariant="sans-serif">F</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {ZF}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/357de7cef8bb838c67863270938732ac24317b8c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.743ex; height:2.176ex;" alt="{\displaystyle {\mathsf {ZF}}}"></span>. Of course, a <a href="/wiki/Tarski%27s_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">direct axiomatization</a> may be studied as well. </p> <div class="mw-heading mw-heading2"><h2 id="Logical_preliminaries">Logical preliminaries</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=2" title="Edit section: Logical preliminaries"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The base logic of constructive analysis is <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a>, which means that the <a href="/wiki/Principle_of_excluded_middle" class="mw-redirect" title="Principle of excluded middle">principle of excluded middle</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathrm {PEM} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {PEM} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/933a14d796125020390d99ccd8a3db5647abe2a8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {PEM} }}"></span> is not automatically assumed for every <a href="/wiki/Proposition" title="Proposition">proposition</a>. If a proposition <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 \exists x.\theta (x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mo>.</mo> <mi>θ</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg \exists x.\theta (x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b2fc8d077266cb6aad3a620397dbfe744f26d723" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.986ex; height:2.843ex;" alt="{\displaystyle \neg \neg \exists x.\theta (x)}"></span> is provable, this exactly means that the non-existence claim <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 \exists x.\theta (x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mo>.</mo> <mi>θ</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \exists x.\theta (x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/146dd05de0aa2edffa342737e8d47bdcc9883404" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.436ex; height:2.843ex;" alt="{\displaystyle \neg \exists x.\theta (x)}"></span> being provable would be absurd, and so the latter cannot also be provable in a consistent theory. The double-negated existence claim is a logically negative statement and implied by, but generally not equivalent to the existence claim itself. Much of the intricacies of constructive analysis can be framed in terms of the weakness of propositions of the logically negative form <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 \phi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mi>ϕ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg \phi }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fc481d4080baeb3f4bb170bb3907bce21b5d4bb4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.486ex; height:2.509ex;" alt="{\displaystyle \neg \neg \phi }"></span>, which is generally weaker than <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 }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ϕ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \phi }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/72b1f30316670aee6270a28334bdf4f5072cdde4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }"></span>. In turn, also an implication <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 {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">(</mo> </mrow> </mrow> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mo>.</mo> <mi>θ</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">)</mo> </mrow> </mrow> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mo>.</mo> <mi mathvariant="normal">¬</mi> <mi>θ</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4678b89e1e7108d71c22b8254138d9f8689f969c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:24.616ex; height:3.176ex;" alt="{\displaystyle {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}"></span> can generally be not reversed. </p><p>While a constructive theory proves fewer theorems than its classical counter-part in its classical presentation, it may exhibit attractive meta-logical properties. For example, if a theory <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 {\mathsf {T}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7860e4d66c67ce669b88f07a796b143537193daf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle {\mathsf {T}}}"></span> exhibits the <a href="/wiki/Disjunction_property" class="mw-redirect" title="Disjunction property">disjunction property</a>, then if it proves a disjunction <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 {\mathsf {T}}\vdash \phi \lor \psi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mo>⊢</mo> <mi>ϕ</mi> <mo>∨</mo> <mi>ψ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\vdash \phi \lor \psi }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/eec656dc528d224327179d5be60471d57649cffa" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.775ex; height:2.509ex;" alt="{\displaystyle {\mathsf {T}}\vdash \phi \lor \psi }"></span> then also <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 {\mathsf {T}}\vdash \phi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mo>⊢</mo> <mi>ϕ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\vdash \phi }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e4ef68f1cd32308bf79f3c0073222338786b2cf1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.679ex; height:2.509ex;" alt="{\displaystyle {\mathsf {T}}\vdash \phi }"></span> or <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 {\mathsf {T}}\vdash \psi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mo>⊢</mo> <mi>ψ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\vdash \psi }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7a54dc8e706b03aa64da4fa4bc076fb8f1e1f634" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.807ex; height:2.509ex;" alt="{\displaystyle {\mathsf {T}}\vdash \psi }"></span>. Already in classical arithmetic, this is violated for the most basic propositions about sequences of numbers - as demonstrated next. </p> <div class="mw-heading mw-heading3"><h3 id="Undecidable_predicates">Undecidable predicates</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=3" title="Edit section: Undecidable predicates"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>A common strategy of formalization of real numbers is in terms of sequences or rationals, <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span> and so we draw motivation and examples in terms of those. So to define terms, consider a <a href="/wiki/Decidable_problem" class="mw-redirect" title="Decidable problem">decidable</a> predicate on the naturals, which in the constructive vernacular means <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">(</mo> </mrow> </mrow> <mi>Q</mi> <mo stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mi>Q</mi> <mo stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">)</mo> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2bbb0f76a7238c9642a54bc78f4ee7725cbcf867" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:20.069ex; height:3.176ex;" alt="{\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}"></span> is provable, and let <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 \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>χ</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>Q</mi> </mrow> </msub> <mo>:</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> <mo stretchy="false">→</mo> <mo fence="false" stretchy="false">{</mo> <mn>0</mn> <mo>,</mo> <mn>1</mn> <mo fence="false" stretchy="false">}</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b059f5531404f67b1bbf682f35c2690b0689c1b3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:14.997ex; height:3.009ex;" alt="{\displaystyle \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}"></span> be the characteristic function defined to equal <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 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2aae8864a3c1fec9585261791a809ddec1489950" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}"></span> exactly 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 Q}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>Q</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle Q}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8752c7023b4b3286800fe3238271bbca681219ed" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.838ex; height:2.509ex;" alt="{\displaystyle Q}"></span> is true. The associated sequence <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_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>q</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <msubsup> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mo>∑</mo> </mstyle> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mi>k</mi> <mo>=</mo> <mn>0</mn> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msubsup> <msub> <mi>χ</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>Q</mi> </mrow> </msub> <mo stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo> <mrow class="MJX-TeXAtom-ORD"> <mo>/</mo> </mrow> <msup> <mn>2</mn> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> <mo>+</mo> <mn>1</mn> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle q_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f72d3d768f582f720979a06821821a1e1b4c3da1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:24.253ex; height:3.343ex;" alt="{\displaystyle q_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}"></span> is monotone, with values non-strictly growing between the bounds <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 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2aae8864a3c1fec9585261791a809ddec1489950" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 1}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>1</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 1}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/92d98b82a3778f043108d4e20960a9193df57cbf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 1}"></span>. Here, for the sake of demonstration, defining an extensional equality to the zero sequence <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\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>q</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <msub> <mi>q</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>=</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (q\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3ad42ed2d50c3805b28016add21cd5e86aa97693" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.367ex; height:2.843ex;" alt="{\displaystyle (q\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}"></span>, it follows that <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\cong _{\mathrm {ext} }0\leftrightarrow \forall n.Q(n)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>q</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">↔</mo> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <mi>Q</mi> <mo stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle q\cong _{\mathrm {ext} }0\leftrightarrow \forall n.Q(n)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1284ea113e545352302aae8e9da878e8c462498f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.178ex; height:2.843ex;" alt="{\displaystyle q\cong _{\mathrm {ext} }0\leftrightarrow \forall n.Q(n)}"></span>. Note that the symbol "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2aae8864a3c1fec9585261791a809ddec1489950" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}"></span>" is used in several contexts here. For any theory capturing arithmetic, there are many yet undecided and even provenly independent such statements <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall n.Q(n)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <mi>Q</mi> <mo stretchy="false">(</mo> <mi>n</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall n.Q(n)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/68030cd7f61156606044e338685b83a9a8845af8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.764ex; height:2.843ex;" alt="{\displaystyle \forall n.Q(n)}"></span>. Two <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 \Pi _{1}^{0}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msubsup> <mi mathvariant="normal">Π</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msubsup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \Pi _{1}^{0}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b0b3c0e79d8a5db977a9838be477eb3e30348937" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.797ex; height:3.176ex;" alt="{\displaystyle \Pi _{1}^{0}}"></span>-examples are the <a href="/wiki/Goldbach_conjecture" class="mw-redirect" title="Goldbach conjecture">Goldbach conjecture</a> and the <a href="/wiki/Rosser%27s_trick" title="Rosser's trick">Rosser sentence</a> of a theory. </p><p>Consider any theory <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 {\mathsf {T}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7860e4d66c67ce669b88f07a796b143537193daf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle {\mathsf {T}}}"></span> with quantifiers ranging over <a href="/wiki/Primitive_recursive" class="mw-redirect" title="Primitive recursive">primitive recursive</a>, rational-valued sequences. Already <a href="/wiki/Minimal_logic" title="Minimal logic">minimal logic</a> proves the non-contradiction claim for any proposition, and that the negation of excluded middle for any given proposition would be absurd. This also means there is no consistent theory (even if anti-classical) rejecting the excluded middle disjunction for any given proposition. Indeed, it holds that </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 {\mathsf {T}}\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,\neg \neg {\big (}(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0){\big )}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mo>⊢</mo> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mi mathvariant="normal">∀</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>∈</mo> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> <mo stretchy="false">)</mo> <mo>.</mo> <mspace width="thinmathspace" /> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">(</mo> </mrow> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mo maxsize="1.2em" minsize="1.2em">)</mo> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,\neg \neg {\big (}(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0){\big )}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b981baaea28c27ba75de2b983e0f006027197c8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:47.639ex; height:3.343ex;" alt="{\displaystyle {\mathsf {T}}\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,\neg \neg {\big (}(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0){\big )}}"></span></dd></dl> <p>This theorem is <a href="/wiki/Intuitionistic_logic#Non-interdefinability_of_operators" title="Intuitionistic logic">logically equivalent</a> to the non-existence claim of a sequence for which the excluded middle disjunction about equality-to-zero would be disprovable. No sequence with that disjunction being rejected can be exhibited. Assume the theories at hand are <a href="/wiki/Consistency" title="Consistency">consistent</a> and arithmetically sound. Now <a href="/wiki/G%C3%B6del%27s_theorems" class="mw-redirect" title="Gödel's theorems">Gödel's theorems</a> mean that there is an explicit sequence <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 g\in {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>g</mi> <mo>∈</mo> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle g\in {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d98878f8354f01a55d7e78cd8d40724b673f9c56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.184ex; height:3.009ex;" alt="{\displaystyle g\in {\mathbb {Q} }^{\mathbb {N} }}"></span> such that, for any fixed precision, <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 {\mathsf {T}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7860e4d66c67ce669b88f07a796b143537193daf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle {\mathsf {T}}}"></span> proves the zero-sequence to be a good approximation to <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 g}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>g</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle g}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d3556280e66fe2c0d0140df20935a6f057381d77" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}"></span>, but it can also meta-logically be established that <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 {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mspace width="thinmathspace" /> <mo>⊬</mo> <mspace width="thinmathspace" /> <mo stretchy="false">(</mo> <mi>g</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4c1f043501f3251ebfd08e8be249ced142dfca6f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.724ex; height:2.843ex;" alt="{\displaystyle {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}"></span> as well as <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 {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mspace width="thinmathspace" /> <mo>⊬</mo> <mspace width="thinmathspace" /> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>g</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/85f4629e86aacbafa1870a171f33e569fd6ce22a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.274ex; height:2.843ex;" alt="{\displaystyle {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}"></span>.<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> Here this proposition <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 g\cong _{\mathrm {ext} }0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>g</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle g\cong _{\mathrm {ext} }0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d5527524a66f41f981a79ca143208b2ed65d591d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.847ex; height:2.509ex;" alt="{\displaystyle g\cong _{\mathrm {ext} }0}"></span> again amounts to the proposition of universally quantified form. Trivially </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 {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">T</mi> </mrow> </mrow> <mo>+</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mo>⊢</mo> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mspace width="thinmathspace" /> <mi mathvariant="normal">∀</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>∈</mo> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> <mo stretchy="false">)</mo> <mo>.</mo> <mspace width="thinmathspace" /> <mo stretchy="false">(</mo> <mi>x</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <msub> <mo>≅</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">e</mi> <mi mathvariant="normal">x</mi> <mi mathvariant="normal">t</mi> </mrow> </mrow> </msub> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e5c52c3502a3717c3f40b293e67ab59a4d9bb139" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:50.546ex; height:3.176ex;" alt="{\displaystyle {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}"></span></dd></dl> <p>even if these disjunction claims here do not carry any information. In the absence of further axioms breaking the meta-logical properties, constructive entailment instead generally reflects provability. Taboo statements that ought not be decidable (if the aim is to respect the provability interpretation of constructive claims) can be designed for definitions of a custom equivalence "<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 \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>" in formalizations below as well. For implications of disjunctions of yet not proven or disproven propositions, one speaks of <a href="/wiki/Constructive_proof#Brouwerian_counterexamples" title="Constructive proof">weak Brouwerian counterexamples</a>. </p> <div class="mw-heading mw-heading3"><h3 id="Order_vs._disjunctions">Order vs. disjunctions</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=4" title="Edit section: Order vs. disjunctions"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The theory of the <a href="/wiki/Real_closed_field" title="Real closed field">real closed field</a> may be axiomatized such that all the non-logical axioms are in accordance with constructive principles. This concerns a <a href="/wiki/Commutative_ring" title="Commutative ring">commutative ring</a> with postulates for a positivity predicate <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 x>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/80d24be5f0eb4a9173da6038badc8659546021d0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x>0}"></span>, with a positive unit and non-positive zero, i.e., <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 1>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>1</mn> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 1>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efdd11636ca6f235c5057ead13e53ac89a9ba25c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.423ex; height:2.176ex;" alt="{\displaystyle 1>0}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg (0>0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mn>0</mn> <mo>></mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (0>0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ac177b35221d869739119f5ee8b546ac6ad8c84d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.783ex; height:2.843ex;" alt="{\displaystyle \neg (0>0)}"></span>. In any such ring, one may define <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 y>x\,:=\,(y-x>0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> <mo>></mo> <mi>x</mi> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <mo stretchy="false">(</mo> <mi>y</mi> <mo>−</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y>x\,:=\,(y-x>0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f8027e5289debcab4acc65db342a6eb7a4ffe659" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.499ex; height:2.843ex;" alt="{\displaystyle y>x\,:=\,(y-x>0)}"></span>, which constitutes a strict total order in its constructive formulation (also called linear order or, to be explicit about the context, a <a href="/wiki/Pseudo-order" title="Pseudo-order">pseudo-order</a>). As is usual, <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 x<0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo><</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x<0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1a4dbbf970b2d2863dcab589eafe006f08e727d7" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x<0}"></span> is defined as <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 0>x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> <mo>></mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0>x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2e360f746d49774c4ff8e5bd3c476de18e316a1c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle 0>x}"></span>. </p><p>This <a href="/wiki/First-order_logic" title="First-order logic">first-order</a> theory is relevant as the structures discussed below are model thereof.<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> However, this section thus does not concern aspects akin to <a href="/wiki/Topology" title="Topology">topology</a> and relevant arithmetic substructures are not <a href="/wiki/Definable_set" title="Definable set">definable</a> therein. </p><p>As explained, various predicates will fail to be decidable in a constructive formulation, such as these formed from order-theoretical relations. This includes "<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 \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>", which will be rendered equivalent to a negation. Crucial disjunctions are now discussed explicitly. </p> <div class="mw-heading mw-heading4"><h4 id="Trichotomy">Trichotomy</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=5" title="Edit section: Trichotomy"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In intuitonistic logic, the <a href="/wiki/Disjunctive_syllogism" title="Disjunctive syllogism">disjunctive syllogism</a> in the form <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 \lor \psi )\to (\neg \phi \to \psi )}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>ϕ</mi> <mo>∨</mo> <mi>ψ</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mi>ψ</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\phi \lor \psi )\to (\neg \phi \to \psi )}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ee4464f6a45ceeb2439b0e3a3d5e7bbf376f5dd1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.777ex; height:2.843ex;" alt="{\displaystyle (\phi \lor \psi )\to (\neg \phi \to \psi )}"></span> generally really only goes in the <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 \to }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">→</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \to }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1daab843254cfcb23a643070cf93f3badc4fbbbd" 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 \to }"></span>-direction. In a pseudo-order, one has </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 (x>0\lor 0>x)\to x\cong 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo>∨</mo> <mn>0</mn> <mo>></mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x>0\lor 0>x)\to x\cong 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3bf8ab84c1a2fdd6e6c80b1343981fa5e16dc772" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.328ex; height:2.843ex;" alt="{\displaystyle \neg (x>0\lor 0>x)\to x\cong 0}"></span></dd></dl> <p>and indeed at most one of the three can hold at once. But the stronger, <i>logically positive</i> <b><a href="/wiki/Law_of_trichotomy" title="Law of trichotomy">law of trichotomy</a> disjunction does not hold in general</b>, i.e. it is not provable that for all reals, </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 (x>0\lor 0>x)\lor x\cong 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo>∨</mo> <mn>0</mn> <mo>></mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x>0\lor 0>x)\lor x\cong 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6975b0947ba3f7186ad3cffd732655f831c80965" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.746ex; height:2.843ex;" alt="{\displaystyle (x>0\lor 0>x)\lor x\cong 0}"></span></dd></dl> <p>See <a href="/wiki/Limited_principle_of_omniscience" title="Limited principle of omniscience">analytical <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 {\mathrm {LPO} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">L</mi> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">O</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {LPO} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/94cee689bfc12a9cc5e96bc182462ecc8dde8ed2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.844ex; height:2.176ex;" alt="{\displaystyle {\mathrm {LPO} }}"></span></a>. Other disjunctions are however implied based on other positivity results, e.g. <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 (x+y>0)\to (x>0\lor y>0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mo>+</mo> <mi>y</mi> <mo>></mo> <mn>0</mn> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo>∨</mo> <mi>y</mi> <mo>></mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x+y>0)\to (x>0\lor y>0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7e40c1b3bd199617d524e371b4d4f6e9dbdde212" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.409ex; height:2.843ex;" alt="{\displaystyle (x+y>0)\to (x>0\lor y>0)}"></span>. Likewise, the asymmetric order in the theory ought to fulfill the weak linearity property <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 (y>x)\to (y>t\lor t>x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>y</mi> <mo>></mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>y</mi> <mo>></mo> <mi>t</mi> <mo>∨</mo> <mi>t</mi> <mo>></mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (y>x)\to (y>t\lor t>x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/038ac5c432366ec5c216cda2ddd384f621e90ddb" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.76ex; height:2.843ex;" alt="{\displaystyle (y>x)\to (y>t\lor t>x)}"></span> for all <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 t}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>t</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle t}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/65658b7b223af9e1acc877d848888ecdb4466560" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}"></span>, related to locatedness of the reals. </p><p>The theory shall validate further axioms concerning the relation between the positivity predicate <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 x>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/80d24be5f0eb4a9173da6038badc8659546021d0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x>0}"></span> and the algebraic operations including multiplicative inversion, as well as the <a href="/wiki/Intermediate_value_theorem" title="Intermediate value theorem">intermediate value theorem</a> for polynomial. In this theory, between any two separated numbers, other numbers exist. </p> <div class="mw-heading mw-heading4"><h4 id="Apartness">Apartness</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=6" title="Edit section: Apartness"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In the context of analysis, the auxiliary <b>logically positive</b> predicate </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 x\#y\,:=\,(x>y\lor y>x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mi>y</mi> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <mo stretchy="false">(</mo> <mi>x</mi> <mo>></mo> <mi>y</mi> <mo>∨</mo> <mi>y</mi> <mo>></mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#y\,:=\,(x>y\lor y>x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb00ff82061763310ebc881da49a6fa763b10634" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.5ex; height:2.843ex;" alt="{\displaystyle x\#y\,:=\,(x>y\lor y>x)}"></span></dd></dl> <p>may be independently defined and constitutes an <i><a href="/wiki/Apartness_relation" title="Apartness relation">apartness relation</a></i>. With it, the substitute of the principles above give tightness </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 (x\#0)\leftrightarrow (x\cong 0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> <mo stretchy="false">)</mo> <mo stretchy="false">↔</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x\#0)\leftrightarrow (x\cong 0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c7679a62b16d246a6bacd069d2e551ee812a2a07" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.802ex; height:2.843ex;" alt="{\displaystyle \neg (x\#0)\leftrightarrow (x\cong 0)}"></span></dd></dl> <p>Thus, apartness can also function as a definition of "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>", rendering it a negation. All negations are stable in intuitionistic logic, and therefore </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 (x\cong y)\leftrightarrow (x\cong y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mi>y</mi> <mo stretchy="false">)</mo> <mo stretchy="false">↔</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \neg (x\cong y)\leftrightarrow (x\cong y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/44e77d396c8fa66cc4d34b8e51d0049725f6c4bb" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.501ex; height:2.843ex;" alt="{\displaystyle \neg \neg (x\cong y)\leftrightarrow (x\cong y)}"></span></dd></dl> <p>The elusive trichotomy disjunction itself then reads </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 (x\#0)\lor \neg (x\#0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x\#0)\lor \neg (x\#0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d6f0b0b1ffda217e4a6957284447f857c4cab4ab" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.608ex; height:2.843ex;" alt="{\displaystyle (x\#0)\lor \neg (x\#0)}"></span></dd></dl> <p>Importantly, a <b>proof of the disjunction <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 x\#y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8837a99fdfb5774ea17a5be3a5b6bd44f60a9b99" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.421ex; height:2.509ex;" alt="{\displaystyle x\#y}"></span> carries positive information</b>, in both senses of the word. Via <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 \neg \psi )\leftrightarrow (\psi \to \neg \phi )}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>ϕ</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>ψ</mi> <mo stretchy="false">)</mo> <mo stretchy="false">↔</mo> <mo stretchy="false">(</mo> <mi>ψ</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>ϕ</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8dba5d85615ed87e1de382bb4046219d3a3fb532" 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 (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}"></span> it also follows that <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 x\#0\to \neg (x\cong 0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#0\to \neg (x\cong 0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/48fa95a25e9ed2d50d772b5a8a3d1fc3187bf2c5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.992ex; height:2.843ex;" alt="{\displaystyle x\#0\to \neg (x\cong 0)}"></span>. In words: A demonstration that a number is somehow apart from zero is also a demonstration that this number is non-zero. But constructively it does not follow that the doubly negative statement <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 (x\cong 0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x\cong 0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d483f62162f17815e24768bc404871f095ae246f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.95ex; height:2.843ex;" alt="{\displaystyle \neg (x\cong 0)}"></span> would imply <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 x\#0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a1e58087c94c2b08741dec96b34dc8f02edd04bd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.428ex; height:2.509ex;" alt="{\displaystyle x\#0}"></span>. Consequently, many classically equivalent statements bifurcate into distinct statement. For example, for a fixed polynomial <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\in {\mathbb {R} }[x]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> <mo>∈</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">R</mi> </mrow> </mrow> <mo stretchy="false">[</mo> <mi>x</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p\in {\mathbb {R} }[x]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/843791c2a18cbe264757e6f16e49f7e0f67119a1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:8.401ex; height:2.843ex;" alt="{\displaystyle p\in {\mathbb {R} }[x]}"></span> and fixed <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 k\in {\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>k</mi> <mo>∈</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle k\in {\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/11fd486baa162a64c7bdef6a0007b999f3a3e079" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.73ex; height:2.176ex;" alt="{\displaystyle k\in {\mathbb {N} }}"></span>, the statement that the <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 k}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>k</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle k}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c3c9a2c7b599b37105512c5d570edc034056dd40" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}"></span>'th coefficient <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_{k}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>a</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>k</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle a_{k}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/05e256a120c3ab9f8958de71acdf81cd75065e3b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.319ex; height:2.009ex;" alt="{\displaystyle a_{k}}"></span> of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/81eac1e205430d1f40810df36a0edffdc367af36" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}"></span> is apart from zero is stronger than the mere statement that it is non-zero. A demonstration of former explicates how <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_{k}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>a</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>k</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle a_{k}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/05e256a120c3ab9f8958de71acdf81cd75065e3b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.319ex; height:2.009ex;" alt="{\displaystyle a_{k}}"></span> and zero are related, with respect to the ordering predicate on the reals, while a demonstration of the latter shows how negation of such conditions would imply to a contradiction. In turn, there is then also a strong and a looser notion of, e.g., being a third-order polynomial. </p><p>So the excluded middle for <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 x\#0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a1e58087c94c2b08741dec96b34dc8f02edd04bd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.428ex; height:2.509ex;" alt="{\displaystyle x\#0}"></span> is apriori stronger than that for <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 x\cong 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≅</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\cong 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/162b4b1fabdcd260c8fa207f376378dfc155d8dc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x\cong 0}"></span>. However, see the discussion of possible further axiomatic principles regarding the strength of "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>" below. </p> <div class="mw-heading mw-heading4"><h4 id="Non-strict_partial_order">Non-strict partial order</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=7" title="Edit section: Non-strict partial order"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Lastly, the relation <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 0\geq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> <mo>≥</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0\geq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6abf8cf26d716845ee5b0be7291bcfc79ca76cf2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.591ex; height:2.343ex;" alt="{\displaystyle 0\geq x}"></span> may be defined by or proven equivalent to the <b>logically negative</b> statement <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 (x>0)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x>0)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9e04bb3ccd211d5a85f76f072e063e5f840e61ec" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.95ex; height:2.843ex;" alt="{\displaystyle \neg (x>0)}"></span>, and then <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/210ba4b4ee0797159d249e2322c142760d476707" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.591ex; height:2.343ex;" alt="{\displaystyle x\leq 0}"></span> is defined as <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 0\geq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> <mo>≥</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0\geq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6abf8cf26d716845ee5b0be7291bcfc79ca76cf2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.591ex; height:2.343ex;" alt="{\displaystyle 0\geq x}"></span>. Decidability of positivity may thus be expressed as <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 x>0\lor 0\geq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mn>0</mn> <mo>∨</mo> <mn>0</mn> <mo>≥</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>0\lor 0\geq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb755890b9a9589118b04d37fd169f593e44012" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:13.764ex; height:2.343ex;" alt="{\displaystyle x>0\lor 0\geq x}"></span>, which as noted will not be provable in general. But neither will the totality disjunction <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 x\geq 0\lor 0\geq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≥</mo> <mn>0</mn> <mo>∨</mo> <mn>0</mn> <mo>≥</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\geq 0\lor 0\geq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b7a51ab70b73ef416ca77764636da2d8877ccdbf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:13.764ex; height:2.343ex;" alt="{\displaystyle x\geq 0\lor 0\geq x}"></span>, see also <a href="/wiki/Limited_principle_of_omniscience" title="Limited principle of omniscience">analytical <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 {\mathrm {LLPO} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">L</mi> <mi mathvariant="normal">L</mi> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">O</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {LLPO} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3dc1dd301051b278ca3d61c44092e0c4574029da" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {LLPO} }}"></span></a>. </p><p>By a valid <a href="/wiki/De_Morgan%27s_laws#In_intuitionistic_logic" title="De Morgan's laws">De Morgan's law</a>, the conjunction of such statements is also rendered a negation of apartness, and so </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 (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≥</mo> <mi>y</mi> <mo>∧</mo> <mi>y</mi> <mo>≥</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">↔</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cf0c52242ded3ba95d98841e8ab8b83dac06f458" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.566ex; height:2.843ex;" alt="{\displaystyle (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}"></span></dd></dl> <p>The disjunction <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 x>y\lor x\cong y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mi>y</mi> <mo>∨</mo> <mi>x</mi> <mo>≅</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>y\lor x\cong y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c4527857bb04da554ac2ce999c7d3eb809840f67" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.75ex; height:2.343ex;" alt="{\displaystyle x>y\lor x\cong y}"></span> implies <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 x\geq y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≥</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\geq y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/aded94d634c48071188bf96a76a4d3b7dfb28470" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\geq y}"></span>, but the other direction is also not provable in general. In a constructive real closed field, <b>the relation "<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 \geq }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≥</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \geq }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bcef7c0e95bb77a35fd1a874ca91f425215f3c26" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \geq }"></span>" is a negation and is not equivalent to the disjunction in general</b>. </p> <div class="mw-heading mw-heading4"><h4 id="Variations">Variations</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=8" title="Edit section: Variations"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Demanding good order properties as above but strong completeness properties at the same time implies <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 {\mathrm {PEM} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {PEM} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/933a14d796125020390d99ccd8a3db5647abe2a8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {PEM} }}"></span>. Notably, the <a href="/wiki/Dedekind%E2%80%93MacNeille_completion" title="Dedekind–MacNeille completion">MacNeille completion</a> has better completeness properties as a collection, but a more intricate theory of its order-relation and, in turn, worse locatedness properties. While less commonly employed, also this construction simplifies to the classical real numbers when assuming <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 {\mathrm {PEM} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {PEM} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/933a14d796125020390d99ccd8a3db5647abe2a8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {PEM} }}"></span>. </p> <div class="mw-heading mw-heading3"><h3 id="Invertibility">Invertibility</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=9" title="Edit section: Invertibility"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In the commutative ring of real numbers, a provably non-invertible element equals zero. This and the most basic locality structure is abstracted in the theory of <a href="/wiki/Heyting_field" title="Heyting field">Heyting fields</a>. </p> <div class="mw-heading mw-heading2"><h2 id="Formalization">Formalization</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=10" title="Edit section: Formalization"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Rational_sequences">Rational sequences</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=11" title="Edit section: Rational sequences"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>A common approach is to identify the real numbers with non-volatile sequences in <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span>. The constant sequences correspond to rational numbers. Algebraic operations such as addition and multiplication can be defined component-wise, together with a systematic reindexing for speedup. The definition in terms of sequences furthermore enables the definition of a strict order "<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 >}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>></mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle >}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1b27b77ab4e3293ea9ce65cef60fea655c398423" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle >}"></span>" fulfilling the desired axioms. Other relations discussed above may then be defined in terms of it. In particular, any number <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 x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> apart from <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 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2aae8864a3c1fec9585261791a809ddec1489950" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}"></span>, i.e. <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 x\#0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\#0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a1e58087c94c2b08741dec96b34dc8f02edd04bd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.428ex; height:2.509ex;" alt="{\displaystyle x\#0}"></span>, eventually has an index beyond which all its elements are invertible.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> Various implications between the relations, as well as between sequences with various properties, may then be proven. </p> <div class="mw-heading mw-heading4"><h4 id="Moduli">Moduli</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=12" title="Edit section: Moduli"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>As the <a href="/wiki/Maximum_and_minimum" title="Maximum and minimum">maximum</a> on a finite set of rationals is decidable, an absolute value map on the reals may be defined and <a href="/wiki/Cauchy_sequence" title="Cauchy sequence">Cauchy convergence</a> and limits of sequences of reals can be defined as usual. </p><p>A <a href="/wiki/Modulus_of_convergence" title="Modulus of convergence">modulus of convergence</a> is often employed in the constructive study of Cauchy sequences of reals, meaning the association of any <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 \varepsilon >0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ε</mi> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \varepsilon >0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e04ec3670b50384a3ce48aca42e7cc5131a06b12" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.344ex; height:2.176ex;" alt="{\displaystyle \varepsilon >0}"></span> to an appropriate index (beyond which the sequences are closer than <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 \varepsilon }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ε</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \varepsilon }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a30c89172e5b88edbd45d3e2772c7f5e562e5173" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.083ex; height:1.676ex;" alt="{\displaystyle \varepsilon }"></span>) is required in the form of an explicit, strictly increasing function <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 \varepsilon \mapsto N(\varepsilon )}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ε</mi> <mo stretchy="false">↦</mo> <mi>N</mi> <mo stretchy="false">(</mo> <mi>ε</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \varepsilon \mapsto N(\varepsilon )}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/50c8f4c83c38eadfbad38ee296f11a8adab6cc0f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.654ex; height:2.843ex;" alt="{\displaystyle \varepsilon \mapsto N(\varepsilon )}"></span>. Such a modulus may be considered for a sequence of reals, but it may also be considered for all the reals themselves, in which case one is really dealing with a sequence of pairs. </p> <div class="mw-heading mw-heading4"><h4 id="Bounds_and_suprema">Bounds and suprema</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=13" title="Edit section: Bounds and suprema"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Given such a model then enables the definition of more set theoretic notions. For any subset of reals, one may speak of an <a href="/wiki/Upper_and_lower_bounds" title="Upper and lower bounds">upper bound</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>b</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle b}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f11423fbb2e967f986e36804a8ae4271734917c3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.998ex; height:2.176ex;" alt="{\displaystyle b}"></span>, negatively characterized using <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 x\leq b}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>b</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq b}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8d1803bf9d4c215835aab217a666aa8225f1626a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.426ex; height:2.343ex;" alt="{\displaystyle x\leq b}"></span>. One may speak of least upper bounds with respect to "<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 \leq }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≤</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leq }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/440568a09c3bfdf0e1278bfa79eb137c04e94035" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \leq }"></span>". A <a href="/wiki/Supremum" class="mw-redirect" title="Supremum">supremum</a> is an upper bound given through a sequence of reals, positively characterized using "<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 <}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo><</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle <}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/33737c89a17785dacc8638b4d66db3d5c8670de1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle <}"></span>". If a subset with an upper bound is well-behaved with respect to "<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 <}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo><</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle <}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/33737c89a17785dacc8638b4d66db3d5c8670de1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle <}"></span>" (discussed below), it has a supremum. </p> <div class="mw-heading mw-heading4"><h4 id="Bishop's_formalization"><span id="Bishop.27s_formalization"></span>Bishop's formalization</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=14" title="Edit section: Bishop's formalization"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p><a href="/wiki/Errett_Bishop" title="Errett Bishop">One formalization</a> of constructive analysis, modeling the order properties described above, proves theorems for sequences of rationals <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 x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> fulfilling the <i>regularity</i> condition <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 |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>−</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>m</mi> </mrow> </msub> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mo>≤</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> <mo>+</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>m</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bf64217962a0be7aebac4298c93ce81dd404a72d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:19.727ex; height:3.343ex;" alt="{\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}"></span>. An alternative is using the tighter <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 2^{-n}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mn>2</mn> <mrow class="MJX-TeXAtom-ORD"> <mo>−</mo> <mi>n</mi> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 2^{-n}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0414b5d9e81c2eb5bd85a6ca4af24b69d5336dad" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.659ex; height:2.509ex;" alt="{\displaystyle 2^{-n}}"></span> instead of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\tfrac {1}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\tfrac {1}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ee46f3d1f145f31319826905e4ce0750792d55b7" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:1.822ex; height:3.343ex;" alt="{\displaystyle {\tfrac {1}{n}}}"></span>, and in the latter case non-zero indices ought to be used. No two of the rational entries in a regular sequence are more than <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 {\tfrac {3}{2}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>3</mn> <mn>2</mn> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\tfrac {3}{2}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/631d66184353d37ebfe470a07a6a61487da227ac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.171ex; width:1.658ex; height:3.509ex;" alt="{\displaystyle {\tfrac {3}{2}}}"></span> apart and so one may compute natural numbers exceeding any real. For the regular sequences, one defines the logically positive loose positivity property as <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 x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>></mo> <mn>0</mn> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <mi mathvariant="normal">∃</mi> <mi>n</mi> <mo>.</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>></mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8cb435ed3fd483fc72fbdf97f7039c8da5b35765" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:21.3ex; height:3.343ex;" alt="{\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}"></span>, where the relation on the right hand side is in terms of rational numbers. Formally, a positive real in this language is a regular sequence together with a natural witnessing positivity. Further, <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 x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≅</mo> <mi>y</mi> <mspace width="thinmathspace" /> <mo>:=</mo> <mspace width="thinmathspace" /> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>−</mo> <msub> <mi>y</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mo>≤</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>2</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8a65dd7aa26859520af4f88598066da77f1d959a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:27.785ex; height:3.343ex;" alt="{\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}"></span>, which is logically equivalent to the negation <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 \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi mathvariant="normal">∃</mi> <mi>n</mi> <mo>.</mo> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>−</mo> <msub> <mi>y</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mo>></mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>2</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/12e90614bbba1863cdb50a51ef5bec7792ed7c7a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:19.232ex; height:3.343ex;" alt="{\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}"></span>. This is provably transitive and in turn an <a href="/wiki/Equivalence_relation" title="Equivalence relation">equivalence relation</a>. Via this predicate, the regular sequences in the band <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 |x_{n}|\leq {\tfrac {2}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mo>≤</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>2</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/323372554dcd950b22a139f95dd5c3210cb68fe0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:8.763ex; height:3.343ex;" alt="{\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}"></span> are deemed equivalent to the zero sequence. Such definitions are of course compatible with classical investigations and variations thereof were well studied also before. One has <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 y>x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> <mo>></mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y>x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a22112f92b4b6d0c2f20283a6b5cb93e384091ca" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.176ex;" alt="{\displaystyle y>x}"></span> as <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 (y-x)>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>y</mi> <mo>−</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (y-x)>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8bcc12c03745716f0cd466920566fb9f5495ca71" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.396ex; height:2.843ex;" alt="{\displaystyle (y-x)>0}"></span>. Also, <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 x\geq 0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≥</mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\geq 0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a2608e2b392b079f5b763f27bf52883dbee3b64a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.591ex; height:2.343ex;" alt="{\displaystyle x\geq 0}"></span> may be defined from a numerical non-negativity property, as <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 x_{n}\geq -{\tfrac {1}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>≥</mo> <mo>−</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{n}\geq -{\tfrac {1}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6127f4819225445f2f0e790f59a765476609d919" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:9.277ex; height:3.343ex;" alt="{\displaystyle x_{n}\geq -{\tfrac {1}{n}}}"></span> for all <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 n}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>n</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle n}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}"></span>, but then shown to be equivalent of the logical negation of the former.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading4"><h4 id="Variations_2">Variations</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=15" title="Edit section: Variations"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The above definition of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\cong y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≅</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\cong y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d0b6980bf35381448462f68d2758cd315a283238" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\cong y}"></span> uses a common bound <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 {\tfrac {2}{n}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>2</mn> <mi>n</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\tfrac {2}{n}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ada21e7887bd500f615e37467aa9a0780c48a983" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:1.822ex; height:3.343ex;" alt="{\displaystyle {\tfrac {2}{n}}}"></span>. Other formalizations directly take as definition that for any fixed bound <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 {\tfrac {2}{N}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>2</mn> <mi>N</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\tfrac {2}{N}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2aa21ea5235613e30f08baeb6aee5b02c404bedc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.171ex; width:2.295ex; height:3.509ex;" alt="{\displaystyle {\tfrac {2}{N}}}"></span>, the numbers <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 x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b8a6208ec717213d4317e666f1ae872e00620a0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}"></span> must eventually be forever at least as close. Exponentially falling bounds <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 2^{-n}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mn>2</mn> <mrow class="MJX-TeXAtom-ORD"> <mo>−</mo> <mi>n</mi> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 2^{-n}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0414b5d9e81c2eb5bd85a6ca4af24b69d5336dad" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.659ex; height:2.509ex;" alt="{\displaystyle 2^{-n}}"></span> are also used, also say in a real number condition <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>n</mi> <mo>.</mo> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo>−</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> <mo>+</mo> <mn>1</mn> </mrow> </msub> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mo><</mo> <msup> <mn>2</mn> <mrow class="MJX-TeXAtom-ORD"> <mo>−</mo> <mi>n</mi> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f1f4b5b9995461b191e4a9345743c45414cc1eb6" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.81ex; height:3.009ex;" alt="{\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}"></span>, and likewise for the equality of two such reals. And also the sequences of rationals may be required to carry a modulus of convergence. Positivity properties may defined as being eventually forever apart by some rational. </p><p><a href="/wiki/Axiom_of_non-choice" title="Axiom of non-choice">Function choice</a> in <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 {\mathbb {N} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {N} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e6699687943087822616a37468d23367daaef9fa" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.097ex; height:2.676ex;" alt="{\displaystyle {\mathbb {N} }^{\mathbb {N} }}"></span> or stronger principles aid such frameworks. </p> <div class="mw-heading mw-heading4"><h4 id="Coding">Coding</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=16" title="Edit section: Coding"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>It is worth noting that sequences in <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span> can be coded rather compactly, as they each may be mapped to a unique subclass of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9bbdf4a20a0a0a50daaa524863051d5d22c9fb23" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle {\mathbb {N} }}"></span>. A sequence rationals <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 i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>i</mi> <mo stretchy="false">↦</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <msub> <mi>n</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> <msub> <mi>d</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> </mfrac> </mstyle> </mrow> <mo stretchy="false">(</mo> <mo>−</mo> <mn>1</mn> <msup> <mo stretchy="false">)</mo> <mrow class="MJX-TeXAtom-ORD"> <msub> <mi>s</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2d78a6c6793d8fbf21eb18532fdeea412a833458" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.671ex; width:13.272ex; height:4.009ex;" alt="{\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}"></span> may be encoded as set of quadruples <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 \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo fence="false" stretchy="false">⟨</mo> <mi>i</mi> <mo>,</mo> <msub> <mi>n</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> <mo>,</mo> <msub> <mi>d</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> <mo>,</mo> <msub> <mi>s</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> <mo fence="false" stretchy="false">⟩</mo> <mo>∈</mo> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mn>4</mn> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4a8b487007381fa77a77230dc1648a89af6fea7a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.38ex; height:3.176ex;" alt="{\displaystyle \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}"></span>. In turn, this can be encoded as unique naturals <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 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mn>2</mn> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msup> <mo>⋅</mo> <msup> <mn>3</mn> <mrow class="MJX-TeXAtom-ORD"> <msub> <mi>n</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> </mrow> </msup> <mo>⋅</mo> <msup> <mn>5</mn> <mrow class="MJX-TeXAtom-ORD"> <msub> <mi>d</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> </mrow> </msup> <mo>⋅</mo> <msup> <mn>7</mn> <mrow class="MJX-TeXAtom-ORD"> <msub> <mi>s</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msub> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/24f33a933e9f161e5f4c6fd7e5447dcc9d41ec0f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:15.67ex; height:2.676ex;" alt="{\displaystyle 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}"></span> using the <a href="/wiki/Fundamental_theorem_of_arithmetic" title="Fundamental theorem of arithmetic">fundamental theorem of arithmetic</a>. There are more economic <a href="/wiki/Pairing_function" title="Pairing function">pairing functions</a> as well, or extension encoding tags or metadata. For an example using this encoding, the sequence <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 i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>i</mi> <mo stretchy="false">↦</mo> <msubsup> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mo>∑</mo> </mstyle> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mi>k</mi> <mo>=</mo> <mn>0</mn> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mi>i</mi> </mrow> </msubsup> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>1</mn> <mi>k</mi> </mfrac> </mstyle> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/df66e691ae94967d95d2bb8cc436562f15fdfe9b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:11.752ex; height:3.843ex;" alt="{\displaystyle i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k}}}"></span>, or <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 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>1</mn> <mo>,</mo> <mn>2</mn> <mo>,</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>5</mn> <mn>2</mn> </mfrac> </mstyle> </mrow> <mo>,</mo> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="false" scriptlevel="0"> <mfrac> <mn>8</mn> <mn>3</mn> </mfrac> </mstyle> </mrow> <mo>,</mo> <mo>…</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c23b093fd29114e0a7e56ee0b33eb6064c549057" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:12.5ex; height:3.676ex;" alt="{\displaystyle 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }"></span>, may be used to compute <a href="/wiki/Euler%27s_number" class="mw-redirect" title="Euler's number">Euler's number</a> and with the above coding it maps to the subclass <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 \{15,90,24300,6561000,\dots \}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo fence="false" stretchy="false">{</mo> <mn>15</mn> <mo>,</mo> <mn>90</mn> <mo>,</mo> <mn>24300</mn> <mo>,</mo> <mn>6561000</mn> <mo>,</mo> <mo>…</mo> <mo fence="false" stretchy="false">}</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \{15,90,24300,6561000,\dots \}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cdb0ff158c1368ee3b171a1e3ebfcc8de507e4c9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.783ex; height:2.843ex;" alt="{\displaystyle \{15,90,24300,6561000,\dots \}}"></span> of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9bbdf4a20a0a0a50daaa524863051d5d22c9fb23" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle {\mathbb {N} }}"></span>. While this example, an explicit sequence of sums, is a <a href="/wiki/Total_recursive_function" class="mw-redirect" title="Total recursive function">total recursive function</a> to begin with, the encoding also means these objects are in scope of the quantifiers in second-order arithmetic. </p> <div class="mw-heading mw-heading3"><h3 id="Set_theory">Set theory</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=17" title="Edit section: Set theory"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading4"><h4 id="Cauchy_reals">Cauchy reals</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=18" title="Edit section: Cauchy reals"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In some frameworks of analysis, the name <i>real numbers</i> is given to such well-behaved sequences or rationals, and relations such as <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 x\cong y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≅</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\cong y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d0b6980bf35381448462f68d2758cd315a283238" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\cong y}"></span> are called the <i>equality or real numbers</i>. Note, however, that there are properties which can distinguish between two <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 \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>-related reals. </p><p>In contrast, in a set theory that models the naturals <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 {\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9bbdf4a20a0a0a50daaa524863051d5d22c9fb23" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle {\mathbb {N} }}"></span> and validates the existence of even classically uncountable function spaces (and certainly <a href="/wiki/Constructive_set_theory#Constructive_Zermelo–Fraenkel" title="Constructive set theory">say <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 {\mathsf {CZF}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">C</mi> <mi mathvariant="sans-serif">Z</mi> <mi mathvariant="sans-serif">F</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {CZF}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/68735fcc4a56810ef5e5662f4ab1a4ad4dde9e51" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.228ex; height:2.176ex;" alt="{\displaystyle {\mathsf {CZF}}}"></span></a> or even <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 {\mathsf {ZFC}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="sans-serif">Z</mi> <mi mathvariant="sans-serif">F</mi> <mi mathvariant="sans-serif">C</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathsf {ZFC}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3d397b9d5a1a8a9507a2ec5ab37c5f60da51f249" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.228ex; height:2.176ex;" alt="{\displaystyle {\mathsf {ZFC}}}"></span>) the numbers equivalent with respect to "<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 \cong }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≅</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \cong }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a725ebc5ab8de11d7b71a8aa5a3706c2ea467885" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.049ex; margin-bottom: -0.22ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \cong }"></span>" in <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span> may be collected into a set and then this is called the <i><a href="/wiki/Construction_of_the_real_numbers#Construction_from_Cauchy_sequences" title="Construction of the real numbers">Cauchy real number</a></i>. In that language, regular rational sequences are degraded to a mere representative of a Cauchy real. Equality of those reals is then given by the equality of sets, which is governed by the set theoretical <a href="/wiki/Axiom_of_extensionality" title="Axiom of extensionality">axiom of extensionality</a>. An upshot is that the set theory will prove properties for the reals, i.e. for this class of sets, expressed using the logical equality. Constructive reals in the presence of appropriate choice axioms will be Cauchy-complete but not automatically order-complete.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading4"><h4 id="Dedekind_reals">Dedekind reals</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=19" title="Edit section: Dedekind reals"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In this context it may also be possible to model a theory or real numbers in terms of <a href="/wiki/Construction_of_the_real_numbers#Construction_by_Dedekind_cuts" title="Construction of the real numbers">Dedekind cuts</a> of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathbb {Q} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/76e0e7d809de86faa824ae83e574aaed26fb410a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.808ex; height:2.509ex;" alt="{\displaystyle {\mathbb {Q} }}"></span>. At least when assuming <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 {\mathrm {PEM} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {PEM} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/933a14d796125020390d99ccd8a3db5647abe2a8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {PEM} }}"></span> or dependent choice, these structures are isomorphic. </p> <div class="mw-heading mw-heading4"><h4 id="Interval_arithmetic">Interval arithmetic</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=20" title="Edit section: Interval arithmetic"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Another approach is to define a real number as a certain subset of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathbb {Q} }\times {\mathbb {Q} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mo>×</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }\times {\mathbb {Q} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cb42c136b0d18481b713d14ec37834d791d34fe0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.457ex; height:2.509ex;" alt="{\displaystyle {\mathbb {Q} }\times {\mathbb {Q} }}"></span>, holding pairs representing inhabited, pairwise intersecting intervals. </p> <div class="mw-heading mw-heading4"><h4 id="Uncountability">Uncountability</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=21" title="Edit section: Uncountability"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Recall that the preorder on <a href="/wiki/Cardinal_number" title="Cardinal number">cardinals</a> "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leq }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≤</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leq }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/440568a09c3bfdf0e1278bfa79eb137c04e94035" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \leq }"></span>" in set theory is the primary notion defined as <a href="/wiki/Injective_function" title="Injective function">injection</a> existence. As a result, the constructive theory of cardinal order can diverge substantially from the classical one. Here, sets like <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span> or some models of the reals can be taken to be <a href="/wiki/Subcountability" title="Subcountability">subcountable</a>. </p><p>That said, <a href="/wiki/Cantor%27s_diagonal_argument#In_the_absence_of_excluded_middle" title="Cantor's diagonal argument">Cantors diagonal construction</a> proving uncountability of powersets like <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 {\mathcal {P}}{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi class="MJX-tex-caligraphic" mathvariant="script">P</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathcal {P}}{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c8f155efb93c1814c15a969f86cddc36257f44cf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.382ex; height:2.176ex;" alt="{\displaystyle {\mathcal {P}}{\mathbb {N} }}"></span> and plain function spaces like <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 {\mathbb {Q} }^{\mathbb {N} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">Q</mi> </mrow> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9aaad80db22c6ac71d931533380fab9b3f131529" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.227ex; height:3.009ex;" alt="{\displaystyle {\mathbb {Q} }^{\mathbb {N} }}"></span> is <a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">intuitionistically</a> valid. Assuming <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 {\mathrm {PEM} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">P</mi> <mi mathvariant="normal">E</mi> <mi mathvariant="normal">M</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {PEM} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/933a14d796125020390d99ccd8a3db5647abe2a8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.297ex; height:2.176ex;" alt="{\displaystyle {\mathrm {PEM} }}"></span> or alternatively the <a href="/wiki/Countable_choice" class="mw-redirect" title="Countable choice">countable choice</a> axiom, models of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathbb {R} }}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">R</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathbb {R} }}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c35d4fb24ff006be5c264f4a3cf7760653a06b30" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle {\mathbb {R} }}"></span> are always uncountable also over a constructive framework.<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> One variant of the diagonal construction relevant for the present context may be formulated as follows, proven using countable choice and for reals as sequences of rationals:<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> </p> <dl><dd>For any two pair of reals <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<b}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>a</mi> <mo><</mo> <mi>b</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle a<b}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/91a7698e4c7401bb321f97888b872b583a9e4642" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.326ex; height:2.176ex;" alt="{\displaystyle a<b}"></span> and any sequence of reals <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 x_{n}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{n}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7c5ea190699149306d242b70439e663559e3ffbe" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.548ex; height:2.009ex;" alt="{\displaystyle x_{n}}"></span>, there exists a real <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 z}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>z</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle z}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bf368e72c009decd9b6686ee84a375632e11de98" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.088ex; height:1.676ex;" alt="{\displaystyle z}"></span> with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a<z<b}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>a</mi> <mo><</mo> <mi>z</mi> <mo><</mo> <mi>b</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle a<z<b}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/22240f2af5666a67e52c8bace8779b0d72d1e404" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:9.512ex; height:2.176ex;" alt="{\displaystyle a<z<b}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mo stretchy="false">(</mo> <mi>n</mi> <mo>∈</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="double-struck">N</mi> </mrow> </mrow> <mo stretchy="false">)</mo> <mo>.</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mspace width="thinmathspace" /> <mi mathvariant="normal">#</mi> <mspace width="thinmathspace" /> <mi>z</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e7dbf9af16ae7b5522df5581a342f76c95ff5e24" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.396ex; height:2.843ex;" alt="{\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}"></span>.</dd></dl> <p>Formulations of the reals aided by explicit moduli permit separate treatments. </p><p>According to <a href="/wiki/Akihiro_Kanamori" title="Akihiro Kanamori">Kanamori</a>, "a historical misrepresentation has been perpetuated that associates diagonalization with non-constructivity" and a constructive component of the <a href="/w/index.php?title=Diagonal_argument_(proof_technique)&action=edit&redlink=1" class="new" title="Diagonal argument (proof technique) (page does not exist)">diagonal argument</a> already appeared in Cantor's work.<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading3"><h3 id="Category_and_type_theory">Category and type theory</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=22" title="Edit section: Category and type theory"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>All these considerations may also be undertaken in a topos or appropriate dependent type theory. </p> <div class="mw-heading mw-heading2"><h2 id="Principles">Principles</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=23" title="Edit section: Principles"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>For practical mathematics, the <a href="/wiki/Axiom_of_dependent_choice" title="Axiom of dependent choice">axiom of dependent choice</a> is adopted in various schools. </p><p><a href="/wiki/Markov%27s_principle#In_constructive_analysis" title="Markov's principle">Markov's principle</a> is adopted in the Russian school of recursive mathematics. This principle strengthens the impact of proven negation of strict equality. A so-called analytical form of it grants <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 (x\leq 0)\to x>0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≤</mo> <mn>0</mn> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>x</mi> <mo>></mo> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x\leq 0)\to x>0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/36040972109acfba0dd83f2f4292b017c6d08191" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.155ex; height:2.843ex;" alt="{\displaystyle \neg (x\leq 0)\to x>0}"></span> or <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 (x\cong 0)\to x\#0}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≅</mo> <mn>0</mn> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>x</mi> <mi mathvariant="normal">#</mi> <mn>0</mn> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \neg (x\cong 0)\to x\#0}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b242e7c95b7f7531aa844174d56a8130fbbb256c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.992ex; height:2.843ex;" alt="{\displaystyle \neg (x\cong 0)\to x\#0}"></span>. Weaker forms may be formulated. </p><p>The <a href="/wiki/L._E._J._Brouwer" title="L. E. J. Brouwer">Brouwerian</a> school reasons in terms of <a href="/wiki/Spread_(intuitionism)" title="Spread (intuitionism)">spreads</a> and adopts the classically valid <a href="/wiki/Bar_induction" title="Bar induction">bar induction</a>. </p> <div class="mw-heading mw-heading3"><h3 id="Anti-classical_schools">Anti-classical schools</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=24" title="Edit section: Anti-classical schools"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Through the optional adoption of further consistent axioms, the negation of decidability may be provable. For example, equality-to-zero is rejected to be decidable when adopting Brouwerian continuity principles or <a href="/wiki/Church%27s_thesis_(constructive_mathematics)" title="Church's thesis (constructive mathematics)">Church's thesis</a> in recursive mathematics.<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> The weak continuity principle as well as <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 {\mathrm {CT} _{0}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <msub> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">C</mi> <mi mathvariant="normal">T</mi> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {CT} _{0}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9356445668640deacf4704ef8974894969d5ecb9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.41ex; height:2.509ex;" alt="{\displaystyle {\mathrm {CT} _{0}}}"></span> even refute <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 x\geq 0\lor 0\geq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≥</mo> <mn>0</mn> <mo>∨</mo> <mn>0</mn> <mo>≥</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\geq 0\lor 0\geq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b7a51ab70b73ef416ca77764636da2d8877ccdbf" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:13.764ex; height:2.343ex;" alt="{\displaystyle x\geq 0\lor 0\geq x}"></span>. The existence of a <a href="/wiki/Specker_sequence" title="Specker sequence">Specker sequence</a> is proven from <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 {\mathrm {CT} _{0}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <msub> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">C</mi> <mi mathvariant="normal">T</mi> </mrow> <mrow class="MJX-TeXAtom-ORD"> <mn>0</mn> </mrow> </msub> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\mathrm {CT} _{0}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/9356445668640deacf4704ef8974894969d5ecb9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.41ex; height:2.509ex;" alt="{\displaystyle {\mathrm {CT} _{0}}}"></span>. Such phenomena also occur in <a href="/wiki/Effective_topos#Realizability_topoi" title="Effective topos">realizability topoi</a>. Notably, there are two anti-classical schools as incompatible with one-another. This article discusses principles compatible with the classical theory and choice is made explicit. </p> <div class="mw-heading mw-heading2"><h2 id="Theorems">Theorems</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=25" title="Edit section: Theorems"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Many classical theorems can only be proven in a formulation that is <a href="/wiki/Logically_equivalent" class="mw-redirect" title="Logically equivalent">logically equivalent</a>, over <a href="/wiki/Classical_logic" title="Classical logic">classical logic</a>. Generally speaking, theorem formulation in constructive analysis mirrors the classical theory closest in <a href="/wiki/Separable_space" title="Separable space">separable spaces</a>. Some theorems can only be formulated in terms of <a href="/wiki/Approximation" title="Approximation">approximations</a>. </p> <div class="mw-heading mw-heading3"><h3 id="The_intermediate_value_theorem">The intermediate value theorem</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=26" title="Edit section: The intermediate value theorem"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>For a simple example, consider the <a href="/wiki/Intermediate_value_theorem" title="Intermediate value theorem">intermediate value theorem</a> (IVT). In classical analysis, IVT implies that, given any <a href="/wiki/Continuous_function" title="Continuous function">continuous function</a> <i>f</i> from a <a href="/wiki/Closed_interval" class="mw-redirect" title="Closed interval">closed interval</a> [<i>a</i>,<i>b</i>] to the <a href="/wiki/Real_line" class="mw-redirect" title="Real line">real line</a> <i>R</i>, if <i>f</i>(<i>a</i>) is <a href="/wiki/Negative_number" title="Negative number">negative</a> while <i>f</i>(<i>b</i>) is <a href="/wiki/Positive_number" class="mw-redirect" title="Positive number">positive</a>, then there exists a <a href="/wiki/Real_number" title="Real number">real number</a> <i>c</i> in the interval such that <i>f</i>(<i>c</i>) is exactly <a href="/wiki/0_(number)" class="mw-redirect" title="0 (number)">zero</a>. In constructive analysis, this does not hold, because the constructive interpretation of <a href="/wiki/Existential_quantification" title="Existential quantification">existential quantification</a> ("there exists") requires one to be able to <i>construct</i> the real number <i>c</i> (in the sense that it can be approximated to any desired precision by a <a href="/wiki/Rational_number" title="Rational number">rational number</a>). But if <i>f</i> hovers near zero during a stretch along its domain, then this cannot necessarily be done. </p><p>However, constructive analysis provides several alternative formulations of IVT, all of which are equivalent to the usual form in classical analysis, but not in constructive analysis. For example, under the same conditions on <i>f</i> as in the classical theorem, given any <a href="/wiki/Natural_number" title="Natural number">natural number</a> <i>n</i> (no matter how large), there exists (that is, we can construct) a real number <i>c</i><sub><i>n</i></sub> in the interval such that the <a href="/wiki/Absolute_value" title="Absolute value">absolute value</a> of <i>f</i>(<i>c</i><sub><i>n</i></sub>) is less than 1/<i>n</i>. That is, we can get as close to zero as we like, even if we can't construct a <i>c</i> that gives us <i>exactly</i> zero. </p><p>Alternatively, we can keep the same conclusion as in the classical IVT—a single <i>c</i> such that <i>f</i>(<i>c</i>) is exactly zero—while strengthening the conditions on <i>f</i>. We require that <i>f</i> be <i>locally non-zero</i>, meaning that given any point <i>x</i> in the interval [<i>a</i>,<i>b</i>] and any natural number <i>m</i>, there exists (we can construct) a real number <i>y</i> in the interval such that |<i>y</i> - <i>x</i>| < 1/<i>m</i> and |<i>f</i>(<i>y</i>)| > 0. In this case, the desired number <i>c</i> can be constructed. This is a complicated condition, but there are several other conditions that imply it and that are commonly met; for example, every <a href="/wiki/Analytic_function" title="Analytic function">analytic function</a> is locally non-zero (assuming that it already satisfies <i>f</i>(<i>a</i>) < 0 and <i>f</i>(<i>b</i>) > 0). </p><p>For another way to view this example, notice that according to <a href="/wiki/Classical_logic" title="Classical logic">classical logic</a>, if the <i>locally non-zero</i> condition fails, then it must fail at some specific point <i>x</i>; and then <i>f</i>(<i>x</i>) will equal 0, so that IVT is valid automatically. Thus in classical analysis, which uses classical logic, in order to prove the full IVT, it is sufficient to prove the constructive version. From this perspective, the full IVT fails in constructive analysis simply because constructive analysis does not accept classical logic. Conversely, one may argue that the true meaning of IVT, even in classical mathematics, is the constructive version involving the <i>locally non-zero</i> condition, with the full IVT following by "pure logic" afterwards. Some logicians, while accepting that classical mathematics is correct, still believe that the constructive approach gives a better insight into the true meaning of theorems, in much this way. </p> <div class="mw-heading mw-heading3"><h3 id="The_least-upper-bound_principle_and_compact_sets">The least-upper-bound principle and compact sets</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=27" title="Edit section: The least-upper-bound principle and compact sets"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Another difference between classical and constructive analysis is that constructive analysis does not prove the <a href="/wiki/Least-upper-bound_principle" class="mw-redirect" title="Least-upper-bound principle">least-upper-bound principle</a>, i.e. that any <a href="/wiki/Subset" title="Subset">subset</a> of the real line <b>R</b> would have a <a href="/wiki/Least_upper_bound" class="mw-redirect" title="Least upper bound">least upper bound</a> (or supremum), possibly infinite. However, as with the intermediate value theorem, an alternative version survives; in constructive analysis, any <i>located</i> subset of the real line has a supremum. (Here a subset <i>S</i> of <b>R</b> is <i>located</i> if, whenever <i>x</i> < <i>y</i> are real numbers, either there exists an element <i>s</i> of <i>S</i> such that <i>x</i> < <i>s</i>, <a href="/wiki/Logical_disjunction" title="Logical disjunction">or</a> <i>y</i> is an <a href="/wiki/Upper_bound" class="mw-redirect" title="Upper bound">upper bound</a> of <i>S</i>.) Again, this is classically equivalent to the full least upper bound principle, since every set is located in classical mathematics. And again, while the definition of located set is complicated, nevertheless it is satisfied by many commonly studied sets, including all <a href="/wiki/Interval_(mathematics)" title="Interval (mathematics)">intervals</a> and all <a href="/wiki/Compact_set" class="mw-redirect" title="Compact set">compact sets</a>. </p><p>Closely related to this, in constructive mathematics, fewer characterisations of <a href="/wiki/Compact_space" title="Compact space">compact spaces</a> are constructively valid—or from another point of view, there are several different concepts that are classically equivalent but not constructively equivalent. Indeed, if the interval [<i>a</i>,<i>b</i>] were <a href="/wiki/Sequentially_compact" class="mw-redirect" title="Sequentially compact">sequentially compact</a> in constructive analysis, then the classical IVT would follow from the first constructive version in the example; one could find <i>c</i> as a <a href="/wiki/Cluster_point" class="mw-redirect" title="Cluster point">cluster point</a> of the <a href="/wiki/Infinite_sequence" class="mw-redirect" title="Infinite sequence">infinite sequence</a> (<i>c</i><sub><i>n</i></sub>)<sub><i>n</i>∈<b>N</b></sub>. </p> <div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=28" title="Edit section: See also"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239009302">.mw-parser-output .portalbox{padding:0;margin:0.5em 0;display:table;box-sizing:border-box;max-width:175px;list-style:none}.mw-parser-output .portalborder{border:1px solid var(--border-color-base,#a2a9b1);padding:0.1em;background:var(--background-color-neutral-subtle,#f8f9fa)}.mw-parser-output .portalbox-entry{display:table-row;font-size:85%;line-height:110%;height:1.9em;font-style:italic;font-weight:bold}.mw-parser-output .portalbox-image{display:table-cell;padding:0.2em;vertical-align:middle;text-align:center}.mw-parser-output .portalbox-link{display:table-cell;padding:0.2em 0.2em 0.2em 0.3em;vertical-align:middle}@media(min-width:720px){.mw-parser-output .portalleft{clear:left;float:left;margin:0.5em 1em 0.5em 0}.mw-parser-output .portalright{clear:right;float:right;margin:0.5em 0 0.5em 1em}}</style><ul role="navigation" aria-label="Portals" class="noprint portalbox portalborder portalright"> <li class="portalbox-entry"><span class="portalbox-image"><span class="noviewer" typeof="mw:File"><a href="/wiki/File:Nuvola_apps_edu_mathematics_blue-p.svg" class="mw-file-description"><img alt="icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/28px-Nuvola_apps_edu_mathematics_blue-p.svg.png" decoding="async" width="28" height="28" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/42px-Nuvola_apps_edu_mathematics_blue-p.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/3/3e/Nuvola_apps_edu_mathematics_blue-p.svg/56px-Nuvola_apps_edu_mathematics_blue-p.svg.png 2x" data-file-width="128" data-file-height="128" /></a></span></span><span class="portalbox-link"><a href="/wiki/Portal:Mathematics" title="Portal:Mathematics">Mathematics portal</a></span></li></ul> <ul><li><a href="/wiki/Computable_analysis" title="Computable analysis">Computable analysis</a></li> <li><a href="/wiki/Constructive_nonstandard_analysis" title="Constructive nonstandard analysis">Constructive nonstandard analysis</a></li> <li><a href="/wiki/Heyting_field" title="Heyting field">Heyting field</a></li> <li><a href="/wiki/Indecomposability_(constructive_mathematics)" class="mw-redirect" title="Indecomposability (constructive mathematics)">Indecomposability (constructive mathematics)</a></li> <li><a href="/wiki/Pseudo-order" title="Pseudo-order">Pseudo-order</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=29" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap mw-references-columns"><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">Troelstra, A. S., van Dalen D., <i>Constructivism in mathematics: an introduction 1</i>; Studies in Logic and the Foundations of Mathematics; Springer, 1988;</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"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFSmith2007" class="citation book cs1">Smith, Peter (2007). <a rel="nofollow" class="external text" href="http://www.godelbook.net/"><i>An introduction to Gödel's Theorems</i></a>. Cambridge, U.K.: Cambridge University Press. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-0-521-67453-9" title="Special:BookSources/978-0-521-67453-9"><bdi>978-0-521-67453-9</bdi></a>. <a href="/wiki/MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=2384958">2384958</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=An+introduction+to+G%C3%B6del%27s+Theorems&rft.place=Cambridge%2C+U.K.&rft.pub=Cambridge+University+Press&rft.date=2007&rft.isbn=978-0-521-67453-9&rft_id=https%3A%2F%2Fmathscinet.ams.org%2Fmathscinet-getitem%3Fmr%3D2384958%23id-name%3DMR&rft.aulast=Smith&rft.aufirst=Peter&rft_id=http%3A%2F%2Fwww.godelbook.net%2F&rfr_id=info%3Asid%2Fen.wikipedia.org%3AConstructive+analysis" class="Z3988"></span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text">Erik Palmgren, <i>An Intuitionistic Axiomatisation of Real Closed Fields</i>, Mathematical Logic Quarterly, Volume 48, Issue 2, Pages: 163-320, February 2002</span> </li> <li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text">Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editors), <i>Handbook of Constructive Mathematics</i>; Studies in Logic and the Foundations of Mathematics; (2023) pp. 201-207</span> </li> <li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text">Errett Bishop, <i>Foundations of Constructive Analysis</i>, July 1967</span> </li> <li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFStolzenberg,_Gabriel1970" class="citation journal cs1">Stolzenberg, Gabriel (1970). <a rel="nofollow" class="external text" href="http://projecteuclid.org/euclid.bams/1183531480">"Review: Errett Bishop, <i>Foundations of Constructive Analysis</i>"</a>. <i><a href="/wiki/Bull._Amer._Math._Soc." class="mw-redirect" title="Bull. Amer. Math. Soc.">Bull. Amer. Math. Soc.</a></i> <b>76</b> (2): 301–323. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1090%2Fs0002-9904-1970-12455-7">10.1090/s0002-9904-1970-12455-7</a></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Bull.+Amer.+Math.+Soc.&rft.atitle=Review%3A+Errett+Bishop%2C+Foundations+of+Constructive+Analysis&rft.volume=76&rft.issue=2&rft.pages=301-323&rft.date=1970&rft_id=info%3Adoi%2F10.1090%2Fs0002-9904-1970-12455-7&rft.au=Stolzenberg%2C+Gabriel&rft_id=http%3A%2F%2Fprojecteuclid.org%2Feuclid.bams%2F1183531480&rfr_id=info%3Asid%2Fen.wikipedia.org%3AConstructive+analysis" class="Z3988"></span></span> </li> <li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text">Robert S. Lubarsky, <a rel="nofollow" class="external text" href="https://arxiv.org/pdf/1510.00639.pdf"><i>On the Cauchy Completeness of the Constructive Cauchy Reals</i></a>, July 2015</span> </li> <li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text">Bauer, A., Hanson, J. A. "The countable reals", 2022</span> </li> <li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text">See, e.g., Theorem 1 in Bishop, 1967, p. 25</span> </li> <li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text"><a href="/wiki/Akihiro_Kanamori" title="Akihiro Kanamori">Akihiro Kanamori</a>, "The Mathematical Development of Set Theory from Cantor to Cohen", <i><a href="/wiki/Bulletin_of_Symbolic_Logic" class="mw-redirect" title="Bulletin of Symbolic Logic">Bulletin of Symbolic Logic</a></i> / Volume 2 / Issue 01 / March 1996, pp 1-71</span> </li> <li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFDiener2020" class="citation arxiv cs1">Diener, Hannes (2020). "Constructive Reverse Mathematics". <a href="/wiki/ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/1804.05495">1804.05495</a></span> [<a rel="nofollow" class="external text" href="https://arxiv.org/archive/math.LO">math.LO</a>].</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=preprint&rft.jtitle=arXiv&rft.atitle=Constructive+Reverse+Mathematics&rft.date=2020&rft_id=info%3Aarxiv%2F1804.05495&rft.aulast=Diener&rft.aufirst=Hannes&rfr_id=info%3Asid%2Fen.wikipedia.org%3AConstructive+analysis" class="Z3988"></span></span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Constructive_analysis&action=edit&section=30" title="Edit section: Further reading"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFBishop1967" class="citation book cs1"><a href="/wiki/Errett_Bishop" title="Errett Bishop">Bishop, Errett</a> (1967). <i>Foundations of Constructive Analysis</i>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/4-87187-714-0" title="Special:BookSources/4-87187-714-0"><bdi>4-87187-714-0</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Foundations+of+Constructive+Analysis&rft.date=1967&rft.isbn=4-87187-714-0&rft.aulast=Bishop&rft.aufirst=Errett&rfr_id=info%3Asid%2Fen.wikipedia.org%3AConstructive+analysis" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFBridger2007" class="citation book cs1">Bridger, Mark (2007). <i>Real Analysis: A Constructive Approach</i>. Hoboken: Wiley. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-471-79230-6" title="Special:BookSources/0-471-79230-6"><bdi>0-471-79230-6</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Real+Analysis%3A+A+Constructive+Approach&rft.place=Hoboken&rft.pub=Wiley&rft.date=2007&rft.isbn=0-471-79230-6&rft.aulast=Bridger&rft.aufirst=Mark&rfr_id=info%3Asid%2Fen.wikipedia.org%3AConstructive+analysis" class="Z3988"></span></li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Non-classical_logic" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Non-classical_logic" title="Template:Non-classical logic"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Non-classical_logic" title="Template talk:Non-classical logic"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Non-classical_logic" title="Special:EditPage/Template:Non-classical logic"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Non-classical_logic" style="font-size:114%;margin:0 4em"><a href="/wiki/Non-classical_logic" title="Non-classical logic">Non-classical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Intuitionism" title="Intuitionism">Intuitionistic</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Intuitionistic_logic" title="Intuitionistic logic">Intuitionistic logic</a></li> <li><a class="mw-selflink selflink">Constructive analysis</a></li> <li><a href="/wiki/Heyting_arithmetic" title="Heyting arithmetic">Heyting arithmetic</a></li> <li><a href="/wiki/Intuitionistic_type_theory" title="Intuitionistic type theory">Intuitionistic type theory</a></li> <li><a href="/wiki/Constructive_set_theory" title="Constructive set theory">Constructive set theory</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Fuzzy_logic" title="Fuzzy logic">Fuzzy</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Degree_of_truth" title="Degree of truth">Degree of truth</a></li> <li><a href="/wiki/Fuzzy_rule" title="Fuzzy rule">Fuzzy rule</a></li> <li><a href="/wiki/Fuzzy_set" title="Fuzzy set">Fuzzy set</a></li> <li><a href="/wiki/Fuzzy_finite_element" title="Fuzzy finite element">Fuzzy finite element</a></li> <li><a href="/wiki/Fuzzy_set_operations" title="Fuzzy set operations">Fuzzy set operations</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Substructural_logic" title="Substructural logic">Substructural</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Structural_rule" title="Structural rule">Structural rule</a></li> <li><a href="/wiki/Relevance_logic" title="Relevance logic">Relevance logic</a></li> <li><a href="/wiki/Linear_logic" title="Linear logic">Linear logic</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Paraconsistent_logic" title="Paraconsistent logic">Paraconsistent</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Dialetheism" title="Dialetheism">Dialetheism</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Description_logic" title="Description logic">Description</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Ontology_(computer_science)" class="mw-redirect" title="Ontology (computer science)">Ontology (computer science)</a></li> <li><a href="/wiki/Ontology_language" title="Ontology language">Ontology language</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Many-valued_logic" title="Many-valued logic">Many-valued</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Three-valued_logic" title="Three-valued logic">Three-valued</a></li> <li><a href="/wiki/Four-valued_logic" title="Four-valued logic">Four-valued</a></li> <li><a href="/wiki/%C5%81ukasiewicz_logic" title="Łukasiewicz logic">Łukasiewicz</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Logic_synthesis" title="Logic synthesis">Digital logic</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Three-state_logic" title="Three-state logic">Three-state logic</a> <ul><li><a href="/wiki/Tri-state_buffer" class="mw-redirect" title="Tri-state buffer">Tri-state buffer</a></li></ul></li> <li><a href="/wiki/Four-valued_logic" title="Four-valued logic">Four-valued</a> <ul><li><a href="/wiki/Verilog" title="Verilog">Verilog</a></li></ul></li> <li><a href="/wiki/IEEE_1164" title="IEEE 1164">IEEE 1164</a> <ul><li><a href="/wiki/VHDL" title="VHDL">VHDL</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Others</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Dynamic_semantics" title="Dynamic semantics">Dynamic semantics</a></li> <li><a href="/wiki/Inquisitive_semantics" title="Inquisitive semantics">Inquisitive logic</a></li> <li><a href="/wiki/Intermediate_logic" title="Intermediate logic">Intermediate logic</a></li> <li><a href="/wiki/Non-monotonic_logic" title="Non-monotonic logic">Non-monotonic logic</a></li></ul> </div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox authority-control" aria-label="Navbox" style="padding:3px"><table class="nowraplinks hlist navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Help:Authority_control" title="Help:Authority control">Authority control databases</a>: National <span class="mw-valign-text-top noprint" typeof="mw:File/Frameless"><a href="https://www.wikidata.org/wiki/Q2845197#identifiers" title="Edit this at Wikidata"><img alt="Edit this at Wikidata" src="//upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/10px-OOjs_UI_icon_edit-ltr-progressive.svg.png" decoding="async" width="10" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/15px-OOjs_UI_icon_edit-ltr-progressive.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/8/8a/OOjs_UI_icon_edit-ltr-progressive.svg/20px-OOjs_UI_icon_edit-ltr-progressive.svg.png 2x" data-file-width="20" data-file-height="20" /></a></span></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4473957-6">Germany</a></span></li></ul></div></td></tr></tbody></table></div>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Constructive_analysis&oldid=1238917105">https://en.wikipedia.org/w/index.php?title=Constructive_analysis&oldid=1238917105</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/wiki/Category:Mathematical_analysis" title="Category:Mathematical analysis">Mathematical analysis</a></li><li><a href="/wiki/Category:Constructivism_(mathematics)" title="Category:Constructivism (mathematics)">Constructivism (mathematics)</a></li><li><a href="/wiki/Category:Intuitionism" title="Category:Intuitionism">Intuitionism</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Articles_with_short_description" title="Category:Articles with short description">Articles with short description</a></li><li><a href="/wiki/Category:Short_description_is_different_from_Wikidata" title="Category:Short description is different from Wikidata">Short description is different from Wikidata</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 6 August 2024, at 11:02<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Constructive_analysis&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-f69cdc8f6-br4qw","wgBackendResponseTime":176,"wgPageParseReport":{"limitreport":{"cputime":"0.551","walltime":"0.752","ppvisitednodes":{"value":1595,"limit":1000000},"postexpandincludesize":{"value":22895,"limit":2097152},"templateargumentsize":{"value":444,"limit":2097152},"expansiondepth":{"value":8,"limit":100},"expensivefunctioncount":{"value":2,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":38665,"limit":5000000},"entityaccesscount":{"value":1,"limit":400},"timingprofile":["100.00% 421.665 1 -total"," 28.83% 121.579 1 Template:Reflist"," 27.18% 114.593 1 Template:Non-classical_logic"," 26.85% 113.230 1 Template:Short_description"," 26.78% 112.929 1 Template:Navbox"," 22.36% 94.305 3 Template:Cite_book"," 16.55% 69.785 2 Template:Pagetype"," 6.85% 28.888 3 Template:Main_other"," 6.30% 26.557 1 Template:SDcat"," 6.05% 25.529 1 Template:Authority_control"]},"scribunto":{"limitreport-timeusage":{"value":"0.271","limit":"10.000"},"limitreport-memusage":{"value":5422650,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-f69cdc8f6-2l27l","timestamp":"20241122144535","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Constructive analysis","url":"https:\/\/en.wikipedia.org\/wiki\/Constructive_analysis","sameAs":"http:\/\/www.wikidata.org\/entity\/Q2845197","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q2845197","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-06-04T06:42:29Z","dateModified":"2024-08-06T11:02:19Z","headline":"mathematical analysis done according to some principles of constructive mathematics"}</script> </body> </html>