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="fr" dir="ltr"> <head> <meta charset="UTF-8"> <title>Calcul des prédicats — Wikipédia</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(/(?:^|; )frwikimwclientpreferences=([^;]+)/);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":[",\t."," \t,"],"wgDigitTransformTable":["",""], "wgDefaultDateFormat":"dmy","wgMonthNames":["","janvier","février","mars","avril","mai","juin","juillet","août","septembre","octobre","novembre","décembre"],"wgRequestId":"b949eed0-1939-4a51-9f57-5cd87a2c0768","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Calcul_des_prédicats","wgTitle":"Calcul des prédicats","wgCurRevisionId":218203062,"wgRevisionId":218203062,"wgArticleId":108828,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Article à référence nécessaire","Article à référence souhaitée","Article avec une section vide ou incomplète","Portail:Logique/Articles liés","Projet:Mathématiques/Articles","Portail:Sciences/Articles liés","Portail:Informatique théorique/Articles liés","Portail:Informatique/Articles liés","Logique","Logique mathématique","Modèle conceptuel"],"wgPageViewLanguage":"fr","wgPageContentLanguage":"fr","wgPageContentModel": "wikitext","wgRelevantPageName":"Calcul_des_prédicats","wgRelevantArticleId":108828,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":true,"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"fr","pageLanguageDir":"ltr","pageVariantFallbacks":"fr"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":true,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":30000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q4055684","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","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","mediawiki.page.media","site","mediawiki.page.ready","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ArchiveLinks","ext.gadget.Wdsearch","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=fr&modules=ext.cite.styles%7Cext.math.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cext.wikimediamessages.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=fr&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=fr&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="Calcul des prédicats — Wikipédia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//fr.m.wikipedia.org/wiki/Calcul_des_pr%C3%A9dicats"> <link rel="alternate" type="application/x-wiki" title="Modifier" href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&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="Wikipédia (fr)"> <link rel="EditURI" type="application/rsd+xml" href="//fr.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://fr.wikipedia.org/wiki/Calcul_des_pr%C3%A9dicats"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.fr"> <link rel="alternate" type="application/atom+xml" title="Flux Atom de Wikipédia" href="/w/index.php?title=Sp%C3%A9cial:Modifications_r%C3%A9centes&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-Calcul_des_prédicats rootpage-Calcul_des_prédicats skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Aller au contenu</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="Menu principal" > <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">Menu principal</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">Menu principal</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">masquer</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/Wikip%C3%A9dia:Accueil_principal" title="Accueil général [z]" accesskey="z"><span>Accueil</span></a></li><li id="n-thema" class="mw-list-item"><a href="/wiki/Portail:Accueil"><span>Portails thématiques</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Page_au_hasard" title="Affiche un article au hasard [x]" accesskey="x"><span>Article au hasard</span></a></li><li id="n-contact" class="mw-list-item"><a href="/wiki/Wikip%C3%A9dia:Contact"><span>Contact</span></a></li> </ul> </div> </div> <div id="p-Contribuer" class="vector-menu mw-portlet mw-portlet-Contribuer" > <div class="vector-menu-heading"> Contribuer </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-aboutwp" class="mw-list-item"><a href="/wiki/Aide:D%C3%A9buter"><span>Débuter sur Wikipédia</span></a></li><li id="n-help" class="mw-list-item"><a href="/wiki/Aide:Accueil" title="Accès à l’aide"><span>Aide</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikip%C3%A9dia:Accueil_de_la_communaut%C3%A9" title="À propos du projet, ce que vous pouvez faire, où trouver les informations"><span>Communauté</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Modifications_r%C3%A9centes" title="Liste des modifications récentes sur le wiki [r]" accesskey="r"><span>Modifications récentes</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Wikip%C3%A9dia:Accueil_principal" 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="Wikipédia" src="/static/images/mobile/copyright/wikipedia-wordmark-fr.svg" style="width: 7.4375em; height: 1.125em;"> <img class="mw-logo-tagline" alt="l'encyclopédie libre" src="/static/images/mobile/copyright/wikipedia-tagline-fr.svg" width="120" height="13" style="width: 7.5em; 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/Sp%C3%A9cial:Recherche" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Rechercher sur Wikipédia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Rechercher</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="Rechercher sur Wikipédia" aria-label="Rechercher sur Wikipédia" autocapitalize="sentences" title="Rechercher sur Wikipédia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Spécial:Recherche"> </div> <button class="cdx-button cdx-search-input__end-button">Rechercher</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Outils personnels"> <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="Apparence"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Modifier l'apparence de la taille, de la largeur et de la couleur de la police de la page" > <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="Apparence" > <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">Apparence</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="//donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_fr.wikipedia.org&uselang=fr" class=""><span>Faire un don</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=Sp%C3%A9cial:Cr%C3%A9er_un_compte&returnto=Calcul+des+pr%C3%A9dicats" title="Nous vous encourageons à créer un compte utilisateur et vous connecter ; ce n’est cependant pas obligatoire." class=""><span>Créer un compte</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=Sp%C3%A9cial:Connexion&returnto=Calcul+des+pr%C3%A9dicats" title="Nous vous encourageons à vous connecter ; ce n’est cependant pas obligatoire. [o]" accesskey="o" class=""><span>Se connecter</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="Plus d’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="Outils personnels" > <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">Outils personnels</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="Menu utilisateur" > <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="//donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_fr.wikipedia.org&uselang=fr"><span>Faire un don</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Cr%C3%A9er_un_compte&returnto=Calcul+des+pr%C3%A9dicats" title="Nous vous encourageons à créer un compte utilisateur et vous connecter ; ce n’est cependant pas obligatoire."><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Créer un compte</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Connexion&returnto=Calcul+des+pr%C3%A9dicats" title="Nous vous encourageons à vous connecter ; ce n’est cependant pas obligatoire. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Se connecter</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 pour les contributeurs déconnectés <a href="/wiki/Aide:Premiers_pas" aria-label="En savoir plus sur la contribution"><span>en savoir plus</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/Sp%C3%A9cial:Mes_contributions" title="Une liste des modifications effectuées depuis cette adresse IP [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Mes_discussions" title="La page de discussion pour les contributions depuis cette adresse IP [n]" accesskey="n"><span>Discussion</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="Sommaire" 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">Sommaire</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">masquer</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">Début</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-Histoire" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Histoire"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>Histoire</span> </div> </a> <ul id="toc-Histoire-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Syntaxe" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Syntaxe"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Syntaxe</span> </div> </a> <button aria-controls="toc-Syntaxe-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>Afficher / masquer la sous-section Syntaxe</span> </button> <ul id="toc-Syntaxe-sublist" class="vector-toc-list"> <li id="toc-Signature" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Signature"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1</span> <span>Signature</span> </div> </a> <ul id="toc-Signature-sublist" class="vector-toc-list"> <li id="toc-Exemples" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Exemples"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1.1</span> <span>Exemples</span> </div> </a> <ul id="toc-Exemples-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Termes" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Termes"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2</span> <span>Termes</span> </div> </a> <ul id="toc-Termes-sublist" class="vector-toc-list"> <li id="toc-Exemples_2" class="vector-toc-list-item vector-toc-level-3"> <a class="vector-toc-link" href="#Exemples_2"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2.1</span> <span>Exemples</span> </div> </a> <ul id="toc-Exemples_2-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Formule" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Formule"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.3</span> <span>Formule</span> </div> </a> <ul id="toc-Formule-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Exemples_3" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Exemples_3"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.4</span> <span>Exemples</span> </div> </a> <ul id="toc-Exemples_3-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Prédicats,_formules_closes,_formules_polies,_variables_libres,_variables_liées" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Prédicats,_formules_closes,_formules_polies,_variables_libres,_variables_liées"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.5</span> <span>Prédicats, formules closes, formules polies, variables libres, variables liées</span> </div> </a> <ul id="toc-Prédicats,_formules_closes,_formules_polies,_variables_libres,_variables_liées-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Sémantique" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Sémantique"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Sémantique</span> </div> </a> <button aria-controls="toc-Sémantique-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>Afficher / masquer la sous-section Sémantique</span> </button> <ul id="toc-Sémantique-sublist" class="vector-toc-list"> <li id="toc-Modèle" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Modèle"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.1</span> <span>Modèle</span> </div> </a> <ul id="toc-Modèle-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Conditions_de_vérité" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Conditions_de_vérité"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.2</span> <span>Conditions de vérité</span> </div> </a> <ul id="toc-Conditions_de_vérité-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Formule_satisfaisable" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Formule_satisfaisable"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.3</span> <span>Formule satisfaisable</span> </div> </a> <ul id="toc-Formule_satisfaisable-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Formule_valide" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Formule_valide"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.4</span> <span>Formule valide</span> </div> </a> <ul id="toc-Formule_valide-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Conséquence_sémantique" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Conséquence_sémantique"> <div class="vector-toc-text"> <span class="vector-toc-numb">4.5</span> <span>Conséquence sémantique</span> </div> </a> <ul id="toc-Conséquence_sémantique-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Système_de_déduction" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Système_de_déduction"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>Système de déduction</span> </div> </a> <ul id="toc-Système_de_déduction-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Propriétés" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Propriétés"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>Propriétés</span> </div> </a> <button aria-controls="toc-Propriétés-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>Afficher / masquer la sous-section Propriétés</span> </button> <ul id="toc-Propriétés-sublist" class="vector-toc-list"> <li id="toc-Complétude" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Complétude"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.1</span> <span>Complétude</span> </div> </a> <ul id="toc-Complétude-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Indécidabilité" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Indécidabilité"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.2</span> <span>Indécidabilité</span> </div> </a> <ul id="toc-Indécidabilité-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Compacité" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Compacité"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.3</span> <span>Compacité</span> </div> </a> <ul id="toc-Compacité-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Expressivité" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Expressivité"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.4</span> <span>Expressivité</span> </div> </a> <ul id="toc-Expressivité-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Théorème_de_Löwenheim-Skolem" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Théorème_de_Löwenheim-Skolem"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.5</span> <span>Théorème de Löwenheim-Skolem</span> </div> </a> <ul id="toc-Théorème_de_Löwenheim-Skolem-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Incomplétude" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Incomplétude"> <div class="vector-toc-text"> <span class="vector-toc-numb">6.6</span> <span>Incomplétude</span> </div> </a> <ul id="toc-Incomplétude-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Fragments_décidables" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Fragments_décidables"> <div class="vector-toc-text"> <span class="vector-toc-numb">7</span> <span>Fragments décidables</span> </div> </a> <ul id="toc-Fragments_décidables-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Variantes" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Variantes"> <div class="vector-toc-text"> <span class="vector-toc-numb">8</span> <span>Variantes</span> </div> </a> <ul id="toc-Variantes-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Notes_et_références" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Notes_et_références"> <div class="vector-toc-text"> <span class="vector-toc-numb">9</span> <span>Notes et références</span> </div> </a> <button aria-controls="toc-Notes_et_références-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>Afficher / masquer la sous-section Notes et références</span> </button> <ul id="toc-Notes_et_références-sublist" class="vector-toc-list"> <li id="toc-Notes" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Notes"> <div class="vector-toc-text"> <span class="vector-toc-numb">9.1</span> <span>Notes</span> </div> </a> <ul id="toc-Notes-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Références" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Références"> <div class="vector-toc-text"> <span class="vector-toc-numb">9.2</span> <span>Références</span> </div> </a> <ul id="toc-Références-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Annexes" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Annexes"> <div class="vector-toc-text"> <span class="vector-toc-numb">10</span> <span>Annexes</span> </div> </a> <button aria-controls="toc-Annexes-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>Afficher / masquer la sous-section Annexes</span> </button> <ul id="toc-Annexes-sublist" class="vector-toc-list"> <li id="toc-Articles_connexes" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Articles_connexes"> <div class="vector-toc-text"> <span class="vector-toc-numb">10.1</span> <span>Articles connexes</span> </div> </a> <ul id="toc-Articles_connexes-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Bibliographie" class="vector-toc-list-item vector-toc-level-1"> <a class="vector-toc-link" href="#Bibliographie"> <div class="vector-toc-text"> <span class="vector-toc-numb">11</span> <span>Bibliographie</span> </div> </a> <ul id="toc-Bibliographie-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="Sommaire" 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="Basculer la table des matières" > <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">Basculer la table des matières</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">Calcul des prédicats</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="Aller à un article dans une autre langue. Disponible en 30 langues." > <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-30" 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">30 langues</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-ar mw-list-item"><a href="https://ar.wikipedia.org/wiki/%D9%85%D9%86%D8%B7%D9%82_%D8%A7%D9%84%D8%B1%D8%AA%D8%A8%D8%A9_%D8%A7%D9%84%D8%A3%D9%88%D9%84%D9%89" title="منطق الرتبة الأولى – arabe" lang="ar" hreflang="ar" data-title="منطق الرتبة الأولى" data-language-autonym="العربية" data-language-local-name="arabe" class="interlanguage-link-target"><span>العربية</span></a></li><li class="interlanguage-link interwiki-ca mw-list-item"><a href="https://ca.wikipedia.org/wiki/L%C3%B2gica_de_primer_ordre" title="Lògica de primer ordre – catalan" lang="ca" hreflang="ca" data-title="Lògica de primer ordre" data-language-autonym="Català" data-language-local-name="catalan" class="interlanguage-link-target"><span>Català</span></a></li><li class="interlanguage-link interwiki-cs mw-list-item"><a href="https://cs.wikipedia.org/wiki/Predik%C3%A1tov%C3%A1_logika_prvn%C3%ADho_%C5%99%C3%A1du" title="Predikátová logika prvního řádu – tchèque" lang="cs" hreflang="cs" data-title="Predikátová logika prvního řádu" data-language-autonym="Čeština" data-language-local-name="tchèque" class="interlanguage-link-target"><span>Čeština</span></a></li><li class="interlanguage-link interwiki-de mw-list-item"><a href="https://de.wikipedia.org/wiki/Pr%C3%A4dikatenlogik_erster_Stufe" title="Prädikatenlogik erster Stufe – allemand" lang="de" hreflang="de" data-title="Prädikatenlogik erster Stufe" data-language-autonym="Deutsch" data-language-local-name="allemand" class="interlanguage-link-target"><span>Deutsch</span></a></li><li class="interlanguage-link interwiki-el mw-list-item"><a href="https://el.wikipedia.org/wiki/%CE%9B%CE%BF%CE%B3%CE%B9%CE%BA%CE%AE_%CF%80%CF%81%CF%8E%CF%84%CE%BF%CF%85_%CE%B2%CE%B1%CE%B8%CE%BC%CE%BF%CF%8D" title="Λογική πρώτου βαθμού – grec" lang="el" hreflang="el" data-title="Λογική πρώτου βαθμού" data-language-autonym="Ελληνικά" data-language-local-name="grec" class="interlanguage-link-target"><span>Ελληνικά</span></a></li><li class="interlanguage-link interwiki-en mw-list-item"><a href="https://en.wikipedia.org/wiki/First-order_logic" title="First-order logic – anglais" lang="en" hreflang="en" data-title="First-order logic" data-language-autonym="English" data-language-local-name="anglais" class="interlanguage-link-target"><span>English</span></a></li><li class="interlanguage-link interwiki-eo mw-list-item"><a href="https://eo.wikipedia.org/wiki/Predikatkalkulo" title="Predikatkalkulo – espéranto" lang="eo" hreflang="eo" data-title="Predikatkalkulo" data-language-autonym="Esperanto" data-language-local-name="espéranto" class="interlanguage-link-target"><span>Esperanto</span></a></li><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/L%C3%B3gica_de_primer_orden" title="Lógica de primer orden – espagnol" lang="es" hreflang="es" data-title="Lógica de primer orden" data-language-autonym="Español" data-language-local-name="espagnol" class="interlanguage-link-target"><span>Español</span></a></li><li class="interlanguage-link interwiki-eu mw-list-item"><a href="https://eu.wikipedia.org/wiki/Lehen_mailako_logika" title="Lehen mailako logika – basque" lang="eu" hreflang="eu" data-title="Lehen mailako logika" data-language-autonym="Euskara" data-language-local-name="basque" class="interlanguage-link-target"><span>Euskara</span></a></li><li class="interlanguage-link interwiki-fa mw-list-item"><a href="https://fa.wikipedia.org/wiki/%D9%85%D9%86%D8%B7%D9%82_%D9%85%D8%B1%D8%AA%D8%A8%D9%87_%D8%A7%D9%88%D9%84" title="منطق مرتبه اول – persan" lang="fa" hreflang="fa" data-title="منطق مرتبه اول" data-language-autonym="فارسی" data-language-local-name="persan" class="interlanguage-link-target"><span>فارسی</span></a></li><li class="interlanguage-link interwiki-he mw-list-item"><a href="https://he.wikipedia.org/wiki/%D7%A9%D7%A4%D7%94_%D7%9E%D7%A1%D7%93%D7%A8_%D7%A8%D7%90%D7%A9%D7%95%D7%9F" title="שפה מסדר ראשון – hébreu" lang="he" hreflang="he" data-title="שפה מסדר ראשון" data-language-autonym="עברית" data-language-local-name="hébreu" class="interlanguage-link-target"><span>עברית</span></a></li><li class="interlanguage-link interwiki-hu mw-list-item"><a href="https://hu.wikipedia.org/wiki/Els%C5%91rend%C5%B1_nyelv" title="Elsőrendű nyelv – hongrois" lang="hu" hreflang="hu" data-title="Elsőrendű nyelv" data-language-autonym="Magyar" data-language-local-name="hongrois" class="interlanguage-link-target"><span>Magyar</span></a></li><li class="interlanguage-link interwiki-hy mw-list-item"><a href="https://hy.wikipedia.org/wiki/%D5%8A%D6%80%D5%A5%D5%A4%D5%AB%D5%AF%D5%A1%D5%BF%D5%B6%D5%A5%D6%80%D5%AB_%D5%BF%D6%80%D5%A1%D5%B4%D5%A1%D5%A2%D5%A1%D5%B6%D5%B8%D6%82%D5%A9%D5%B5%D5%B8%D6%82%D5%B6" title="Պրեդիկատների տրամաբանություն – arménien" lang="hy" hreflang="hy" data-title="Պրեդիկատների տրամաբանություն" data-language-autonym="Հայերեն" data-language-local-name="arménien" class="interlanguage-link-target"><span>Հայերեն</span></a></li><li class="interlanguage-link interwiki-id mw-list-item"><a href="https://id.wikipedia.org/wiki/Logika_predikat_tingkat_pertama" title="Logika predikat tingkat pertama – indonésien" lang="id" hreflang="id" data-title="Logika predikat tingkat pertama" data-language-autonym="Bahasa Indonesia" data-language-local-name="indonésien" class="interlanguage-link-target"><span>Bahasa Indonesia</span></a></li><li class="interlanguage-link interwiki-it mw-list-item"><a href="https://it.wikipedia.org/wiki/Teoria_del_primo_ordine" title="Teoria del primo ordine – italien" lang="it" hreflang="it" data-title="Teoria del primo ordine" data-language-autonym="Italiano" data-language-local-name="italien" class="interlanguage-link-target"><span>Italiano</span></a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/%E4%B8%80%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86" title="一階述語論理 – japonais" lang="ja" hreflang="ja" data-title="一階述語論理" data-language-autonym="日本語" data-language-local-name="japonais" class="interlanguage-link-target"><span>日本語</span></a></li><li class="interlanguage-link interwiki-ko mw-list-item"><a href="https://ko.wikipedia.org/wiki/1%EC%B0%A8_%EB%85%BC%EB%A6%AC" title="1차 논리 – coréen" lang="ko" hreflang="ko" data-title="1차 논리" data-language-autonym="한국어" data-language-local-name="coréen" class="interlanguage-link-target"><span>한국어</span></a></li><li class="interlanguage-link interwiki-no mw-list-item"><a href="https://no.wikipedia.org/wiki/F%C3%B8rsteordens_logikk" title="Førsteordens logikk – norvégien bokmål" lang="nb" hreflang="nb" data-title="Førsteordens logikk" data-language-autonym="Norsk bokmål" data-language-local-name="norvégien bokmål" class="interlanguage-link-target"><span>Norsk bokmål</span></a></li><li class="interlanguage-link interwiki-pl mw-list-item"><a href="https://pl.wikipedia.org/wiki/Rachunek_predykat%C3%B3w_pierwszego_rz%C4%99du" title="Rachunek predykatów pierwszego rzędu – polonais" lang="pl" hreflang="pl" data-title="Rachunek predykatów pierwszego rzędu" data-language-autonym="Polski" data-language-local-name="polonais" class="interlanguage-link-target"><span>Polski</span></a></li><li class="interlanguage-link interwiki-ps mw-list-item"><a href="https://ps.wikipedia.org/wiki/%D8%AF_%D9%84%D9%88%D9%85%DA%93%D9%8A_%D8%AA%D8%B1%D8%AA%DB%8C%D8%A8_%D9%85%D9%86%D8%B7%D9%82" title="د لومړي ترتیب منطق – pachto" lang="ps" hreflang="ps" data-title="د لومړي ترتیب منطق" data-language-autonym="پښتو" data-language-local-name="pachto" class="interlanguage-link-target"><span>پښتو</span></a></li><li class="interlanguage-link interwiki-pt mw-list-item"><a href="https://pt.wikipedia.org/wiki/L%C3%B3gica_de_primeira_ordem" title="Lógica de primeira ordem – portugais" lang="pt" hreflang="pt" data-title="Lógica de primeira ordem" data-language-autonym="Português" data-language-local-name="portugais" class="interlanguage-link-target"><span>Português</span></a></li><li class="interlanguage-link interwiki-ru mw-list-item"><a href="https://ru.wikipedia.org/wiki/%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_%D0%BF%D0%B5%D1%80%D0%B2%D0%BE%D0%B3%D0%BE_%D0%BF%D0%BE%D1%80%D1%8F%D0%B4%D0%BA%D0%B0" title="Логика первого порядка – russe" lang="ru" hreflang="ru" data-title="Логика первого порядка" data-language-autonym="Русский" data-language-local-name="russe" class="interlanguage-link-target"><span>Русский</span></a></li><li class="interlanguage-link interwiki-sh mw-list-item"><a href="https://sh.wikipedia.org/wiki/Logika_prvog_reda" title="Logika prvog reda – serbo-croate" lang="sh" hreflang="sh" data-title="Logika prvog reda" data-language-autonym="Srpskohrvatski / српскохрватски" data-language-local-name="serbo-croate" class="interlanguage-link-target"><span>Srpskohrvatski / српскохрватски</span></a></li><li class="interlanguage-link interwiki-simple mw-list-item"><a href="https://simple.wikipedia.org/wiki/First_order_logic" title="First order logic – Simple English" lang="en-simple" hreflang="en-simple" data-title="First order logic" data-language-autonym="Simple English" data-language-local-name="Simple English" class="interlanguage-link-target"><span>Simple English</span></a></li><li class="interlanguage-link interwiki-sr mw-list-item"><a href="https://sr.wikipedia.org/wiki/%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_%D0%BF%D1%80%D0%B2%D0%BE%D0%B3_%D1%80%D0%B5%D0%B4%D0%B0" title="Логика првог реда – serbe" lang="sr" hreflang="sr" data-title="Логика првог реда" data-language-autonym="Српски / srpski" data-language-local-name="serbe" class="interlanguage-link-target"><span>Српски / srpski</span></a></li><li class="interlanguage-link interwiki-sv mw-list-item"><a href="https://sv.wikipedia.org/wiki/F%C3%B6rsta_ordningens_logik" title="Första ordningens logik – suédois" lang="sv" hreflang="sv" data-title="Första ordningens logik" data-language-autonym="Svenska" data-language-local-name="suédois" class="interlanguage-link-target"><span>Svenska</span></a></li><li class="interlanguage-link interwiki-tl mw-list-item"><a href="https://tl.wikipedia.org/wiki/Lohika_ng_unang_orden" title="Lohika ng unang orden – tagalog" lang="tl" hreflang="tl" data-title="Lohika ng unang orden" data-language-autonym="Tagalog" data-language-local-name="tagalog" class="interlanguage-link-target"><span>Tagalog</span></a></li><li class="interlanguage-link interwiki-uk mw-list-item"><a href="https://uk.wikipedia.org/wiki/%D0%9B%D0%BE%D0%B3%D1%96%D0%BA%D0%B0_%D0%BF%D0%B5%D1%80%D1%88%D0%BE%D0%B3%D0%BE_%D0%BF%D0%BE%D1%80%D1%8F%D0%B4%D0%BA%D1%83" title="Логіка першого порядку – ukrainien" lang="uk" hreflang="uk" data-title="Логіка першого порядку" data-language-autonym="Українська" data-language-local-name="ukrainien" class="interlanguage-link-target"><span>Українська</span></a></li><li class="interlanguage-link interwiki-vi mw-list-item"><a href="https://vi.wikipedia.org/wiki/Logic_b%E1%BA%ADc_nh%E1%BA%A5t" title="Logic bậc nhất – vietnamien" lang="vi" hreflang="vi" data-title="Logic bậc nhất" data-language-autonym="Tiếng Việt" data-language-local-name="vietnamien" class="interlanguage-link-target"><span>Tiếng Việt</span></a></li><li class="interlanguage-link interwiki-zh mw-list-item"><a href="https://zh.wikipedia.org/wiki/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91" title="一阶逻辑 – chinois" lang="zh" hreflang="zh" data-title="一阶逻辑" data-language-autonym="中文" data-language-local-name="chinois" class="interlanguage-link-target"><span>中文</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q4055684#sitelinks-wikipedia" title="Modifier les liens interlangues" class="wbc-editpage">Modifier les liens</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="Espaces de noms"> <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/Calcul_des_pr%C3%A9dicats" title="Voir le contenu de la page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Discussion:Calcul_des_pr%C3%A9dicats" rel="discussion" title="Discussion au sujet de cette page de contenu [t]" accesskey="t"><span>Discussion</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="Modifier la variante de langue" > <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">français</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="Affichages"> <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/Calcul_des_pr%C3%A9dicats"><span>Lire</span></a></li><li id="ca-ve-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit" title="Modifier cette page [v]" accesskey="v"><span>Modifier</span></a></li><li id="ca-edit" class="collapsible vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit" title="Modifier le wikicode de cette page [e]" accesskey="e"><span>Modifier le code</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=history" title="Historique des versions de cette page [h]" accesskey="h"><span>Voir l’historique</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Outils de la page"> <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="Outils" > <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">Outils</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">Outils</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">masquer</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="Plus d’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/Calcul_des_pr%C3%A9dicats"><span>Lire</span></a></li><li id="ca-more-ve-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit" title="Modifier cette page [v]" accesskey="v"><span>Modifier</span></a></li><li id="ca-more-edit" class="collapsible vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit" title="Modifier le wikicode de cette page [e]" accesskey="e"><span>Modifier le code</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=history"><span>Voir l’historique</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> Général </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Pages_li%C3%A9es/Calcul_des_pr%C3%A9dicats" title="Liste des pages liées qui pointent sur celle-ci [j]" accesskey="j"><span>Pages liées</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Suivi_des_liens/Calcul_des_pr%C3%A9dicats" rel="nofollow" title="Liste des modifications récentes des pages appelées par celle-ci [k]" accesskey="k"><span>Suivi des pages liées</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Aide:Importer_un_fichier" title="Téléverser des fichiers [u]" accesskey="u"><span>Téléverser un fichier</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Pages_sp%C3%A9ciales" title="Liste de toutes les pages spéciales [q]" accesskey="q"><span>Pages spéciales</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&oldid=218203062" title="Adresse permanente de cette version de cette page"><span>Lien permanent</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=info" title="Davantage d’informations sur cette page"><span>Informations sur la page</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Citer&page=Calcul_des_pr%C3%A9dicats&id=218203062&wpFormIdentifier=titleform" title="Informations sur la manière de citer cette page"><span>Citer cette page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:UrlShortener&url=https%3A%2F%2Ffr.wikipedia.org%2Fwiki%2FCalcul_des_pr%25C3%25A9dicats"><span>Obtenir l'URL raccourcie</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:QrCode&url=https%3A%2F%2Ffr.wikipedia.org%2Fwiki%2FCalcul_des_pr%25C3%25A9dicats"><span>Télécharger le code QR</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"> Imprimer / exporter </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-create_a_book" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Livre&bookcmd=book_creator&referer=Calcul+des+pr%C3%A9dicats"><span>Créer un livre</span></a></li><li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:DownloadAsPdf&page=Calcul_des_pr%C3%A9dicats&action=show-download-screen"><span>Télécharger comme PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&printable=yes" title="Version imprimable de cette page [p]" accesskey="p"><span>Version imprimable</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"> Dans d’autres projets </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/Q4055684" title="Lien vers l’élément dans le dépôt de données connecté [g]" accesskey="g"><span>Élément Wikidata</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="Outils de la page"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Apparence"> <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">Apparence</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">masquer</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">Un article de Wikipédia, l'encyclopédie libre.</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="fr" dir="ltr"><p>En <a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">logique mathématique</a>, le <b>calcul des prédicats du premier ordre</b>, <b>logique du premier ordre</b>, <b>calcul des relations</b>, <b>logique quantificationnelle</b><sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 23 juillet 2023) ; voir l'aide.">[réf. nécessaire]</span></a></sup>, ou tout simplement <b>calcul des prédicats</b>, est un <a href="/wiki/Syst%C3%A8me_formel" title="Système formel">système formel</a> utilisé pour raisonner et décrire des énoncés en <a href="/wiki/Math%C3%A9matiques" title="Mathématiques">mathématiques</a>, <a href="/wiki/Informatique" title="Informatique">informatique</a>, <a href="/wiki/Intelligence_artificielle" title="Intelligence artificielle">intelligence artificielle</a><sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite_crochet">[</span>1<span class="cite_crochet">]</span></a></sup>, <a href="/wiki/Philosophie" title="Philosophie">philosophie</a> et <a href="/wiki/Linguistique" title="Linguistique">linguistique</a>. Il a été proposé par <a href="/wiki/Gottlob_Frege" title="Gottlob Frege">Gottlob Frege</a><sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite_crochet">[</span>2<span class="cite_crochet">]</span></a></sup> comme une formalisation du langage des <a href="/wiki/Math%C3%A9matiques" title="Mathématiques">mathématiques</a> entre la fin du <abbr class="abbr" title="19ᵉ siècle"><span class="romain">XIX</span><sup style="font-size:72%">e</sup></abbr> siècle et le début du <abbr class="abbr" title="20ᵉ siècle"><span class="romain">XX</span><sup style="font-size:72%">e</sup></abbr> siècle. La logique du premier ordre comporte deux parties : </p> <ul><li>la <i><a href="/wiki/Syntaxe_(logique)" title="Syntaxe (logique)">syntaxe</a></i> définit le vocabulaire symbolique de base ainsi que les règles permettant de construire des énoncés ;</li> <li>la <i><a href="/wiki/S%C3%A9mantique_axiomatique" title="Sémantique axiomatique">sémantique</a></i> interprète ces énoncés comme exprimant des relations entre les éléments d'un domaine, également appelé <i>modèle</i>.</li></ul> <p>Sur le plan syntaxique, les langages du premier ordre opposent deux grandes classes linguistiques : </p> <ul><li>les constituants servant à identifier ou nommer des éléments du domaine : <i>variables</i>, <i>symboles de constantes</i>, <i>termes</i> ;</li> <li>les constituants servant à exprimer des propriétés ou des relations entre ces éléments : <i>prédicats</i> et <i>formules</i>.</li></ul> <p>Un <a href="/wiki/Pr%C3%A9dicat_(linguistique)" title="Prédicat (linguistique)">prédicat</a> est une expression linguistique qui peut être reliée à un ou plusieurs éléments du domaine pour former une phrase. Par exemple, dans la phrase « Mars est une planète », l'expression « est une planète » est un prédicat qui est relié au nom (symbole de constante) « Mars » pour former une phrase. Et dans la phrase « Jupiter est plus grand que Mars », l'expression « est plus grand que » est un prédicat qui se relie aux deux noms, « Jupiter » et « Mars », pour former une phrase. </p><p>Lorsqu'un prédicat est lié à une expression, on dit qu'il exprime une propriété (telle que la propriété d'être une planète), et lorsqu'il est lié à deux ou plusieurs expressions, on dit qu'il exprime une relation (telle que la relation d'être plus grand). Ainsi on peut raisonner sur des énoncés comme « il existe un <span class="mwe-math-element"><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> tel que pour tout <span class="mwe-math-element"><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>, <span class="mwe-math-element"><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> est ami avec <span class="mwe-math-element"><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> », ce qui est exprimé symboliquement par la formule : </p> <center><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\mathrm {amis} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">s</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\mathrm {amis} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6d36eca96e98744906ace5dbe522de339060ca4f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.641ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\mathrm {amis} (x,y)}"></span>.</center> <p>Il convient de noter cependant que la logique du premier ordre ne contient aucune relation spécifique (comme telle <a href="/wiki/Relation_d%27ordre" title="Relation d'ordre">relation d'ordre</a>, d'inclusion ou d'égalité) ; en fait, il ne s'agit que d'étudier la façon dont on doit parler et raisonner avec les expressions du <a href="/wiki/Langage_math%C3%A9matique" title="Langage mathématique">langage mathématique</a>. </p><p>Les traits caractéristiques de la logique du premier ordre sont : </p> <ul><li>l'utilisation de <a href="/wiki/Variable_(math%C3%A9matiques)" title="Variable (mathématiques)"><i>variables</i></a> comme <span class="mwe-math-element"><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>, <span class="mwe-math-element"><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>, <abbr class="abbr" title="et cetera">etc.</abbr> pour dénoter des éléments du domaine d'interprétation ;</li> <li>l'utilisation de <a href="/wiki/Pr%C3%A9dicat_(logique_math%C3%A9matique)" title="Prédicat (logique mathématique)"><i>prédicats</i></a> (ou <i>relations</i>) sur les éléments ;</li> <li>l'utilisation d'<a href="/wiki/Connecteur_logique" title="Connecteur logique">opérations logiques</a> (<i>et, ou, implique</i>, <abbr class="abbr" title="et cetera">etc.</abbr>) ;</li> <li>l'utilisation de <a href="/wiki/Quantification_(logique)" title="Quantification (logique)"><i>quantifications</i></a>, par exemple, l'une universelle (« Quel que soit », « pour tout » noté <a href="/wiki/%E2%88%80" class="mw-redirect" title="∀">∀</a>) et l'autre existentielle (« il existe au moins un… tel que », noté <a href="/wiki/%E2%88%83" class="mw-redirect" title="∃">∃</a>).</li></ul> <p>Le <i>calcul des prédicats du premier ordre égalitaire</i> adjoint au calcul des prédicats un symbole de relation, l'égalité, dont l'interprétation est l'affirmation que deux éléments sont les mêmes, et qui est axiomatisée en conséquence. Suivant le contexte, on peut parler simplement de calcul des prédicats pour le calcul des prédicats égalitaire. </p><p>On parle de logique du premier ordre par opposition aux <a href="/wiki/Logique_d%27ordre_sup%C3%A9rieur" title="Logique d'ordre supérieur">logiques d'ordre supérieur</a>, où l'on peut aussi appliquer les quantificateurs et les prédicats aux prédicats ou aux fonctions, en plus des variables. En outre, cet article ne traite que de la logique du premier ordre <a href="/wiki/Logique_classique" title="Logique classique">classique</a>, mais on notera qu'il existe aussi une <a href="/wiki/Logique_intuitionniste#Le_calcul_des_prédicats_intuitionniste" title="Logique intuitionniste">logique du premier ordre intuitionniste</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=Calcul_des_pr%C3%A9dicats&veaction=edit&section=1" title="Modifier la section : Introduction" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=1" title="Modifier le code source de la section : Introduction"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Alors que la <a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">logique propositionnelle</a> traite des propositions déclaratives simples, la logique du premier ordre couvre en plus les prédicats et la quantification. </p><p>Un prédicat prend en entrée une ou plusieurs entités du domaine du discours et en sortie, il est soit Vrai, soit Faux. Considérons les deux phrases « Socrate est un philosophe » et « <a href="/wiki/Platon" title="Platon">Platon</a> est un philosophe ». En logique propositionnelle, ces phrases sont considérées comme non liées et peuvent être désignées, par exemple, par des variables telles que <span class="nowrap">p et q</span>. Le prédicat « est un philosophe » apparaît dans les deux phrases, dont la structure commune est « a est un philosophe ». La variable a est instanciée en tant que « Socrate » dans la première phrase, et est instanciée en tant que « Platon » dans la deuxième phrase. Alors que la logique du premier ordre permet l'utilisation de prédicats, tels que « est un philosophe » dans cet exemple, la logique propositionnelle ne le permet pas. </p><p>Les relations entre les prédicats peuvent être énoncées à l'aide de connecteurs logiques. Considérons, par exemple, la formule du premier ordre « si a est un philosophe, alors a est un savant ». Cette formule est un énoncé conditionnel dont l'hypothèse est « a est un philosophe » et la conclusion « a est un savant ». La vérité de cette formule dépend de l'objet désigné par a, et des interprétations des prédicats « est un philosophe » et « est un savant ». </p><p>Les quantificateurs peuvent être appliqués aux variables d'une formule. La variable a de la formule précédente peut être quantifiée universellement, par exemple avec la phrase du premier ordre « Pour tout a, si a est un philosophe, alors a est un savant ». Le quantificateur universel « pour chaque » dans cette phrase exprime l'idée que l'affirmation « si a est un philosophe, alors a est un savant » est valable pour tous les choix de a. </p><p>La négation de la phrase « Pour tout a, si a est un philosophe, alors a est un savant » est logiquement équivalente à la phrase « Il existe a tel que a est un philosophe et a n'est pas un savant ». Le quantificateur existentiel « il existe » exprime l'idée que l'affirmation « a est un philosophe et a n'est pas un savant » est valable pour un certain choix de a. </p><p>Les prédicats « est un philosophe » et « est un savant » prennent chacun une seule variable. En général, les prédicats peuvent prendre plusieurs variables. Dans la phrase du premier ordre « Socrate est le professeur de Platon », le prédicat « est le professeur de » prend deux variables. </p> <div class="mw-heading mw-heading2"><h2 id="Histoire">Histoire</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=2" title="Modifier la section : Histoire" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=2" title="Modifier le code source de la section : Histoire"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p><a href="/wiki/Emmanuel_Kant" title="Emmanuel Kant">Emmanuel Kant</a> croyait à tort que la logique de son temps, celle d’<a href="/wiki/Aristote" title="Aristote">Aristote</a>, était une <a href="/wiki/Science" title="Science">science</a> complète et définitivement achevée (préface de la seconde édition de la <a href="/wiki/Critique_de_la_raison_pure" title="Critique de la raison pure">critique de la raison pure</a>, 1787<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite_crochet">[</span>3<span class="cite_crochet">]</span></a></sup>). Les logiciens<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite_crochet">[</span>4<span class="cite_crochet">]</span></a></sup> du <abbr class="abbr" title="19ᵉ siècle"><span class="romain">XIX</span><sup style="font-size:72%">e</sup></abbr> siècle se sont rendu compte que la théorie d’Aristote ne dit rien ou presque sur la logique des relations. <a href="/wiki/Gottlob_Frege" title="Gottlob Frege">Gottlob Frege</a> et beaucoup d'autres ont comblé cette lacune en définissant le calcul des prédicats au premier ordre. </p><p><a href="/wiki/Kurt_G%C3%B6del" title="Kurt Gödel">Kurt Gödel</a> a démontré en 1929 (dans sa thèse de doctorat) que le calcul des prédicats est complet, au sens où on peut donner un nombre fini de principes (<a href="/wiki/Axiome_logique" title="Axiome logique">axiomes logiques</a>, <a href="/wiki/Sch%C3%A9ma_d%27axiomes" title="Schéma d'axiomes">schémas d'axiomes</a> logiques et <a href="/wiki/D%C3%A9duction_logique" title="Déduction logique">règles de déduction</a><sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite_crochet">[</span>5<span class="cite_crochet">]</span></a></sup>) qui suffisent pour déduire de façon mécanique toutes les lois logiques (voir le <a href="/wiki/Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del" title="Théorème de complétude de Gödel">théorème de complétude de Gödel</a>). Il y a équivalence entre la présentation sémantique et la présentation syntaxique du calcul des prédicats. Tout énoncé universellement valide (c'est-à-dire vrai dans tout modèle du langage utilisé) est un <a href="/wiki/Th%C3%A9or%C3%A8me" title="Théorème">théorème</a> (c'est-à-dire qu'il peut être déduit d'un calcul, un système de règles logiques et d'axiomes, de façon équivalente un <a href="/wiki/Syst%C3%A8me_%C3%A0_la_Hilbert" title="Système à la Hilbert">système à la Hilbert</a>, la <a href="/wiki/D%C3%A9duction_naturelle" title="Déduction naturelle">déduction naturelle</a>, ou le <a href="/wiki/Calcul_des_s%C3%A9quents" title="Calcul des séquents">calcul des séquents</a>), et réciproquement. La logique du premier ordre est donc achevée au sens où le problème de la correction logique des démonstrations y est résolu. Elle continue cependant à faire l’objet d’importantes recherches : <a href="/wiki/Th%C3%A9orie_des_mod%C3%A8les" title="Théorie des modèles">théorie des modèles</a>, <a href="/wiki/Th%C3%A9orie_de_la_d%C3%A9monstration" title="Théorie de la démonstration">théorie de la démonstration</a>, <a href="/wiki/Assistant_de_preuve" title="Assistant de preuve">mécanisation du raisonnement</a>… </p> <div class="mw-heading mw-heading2"><h2 id="Syntaxe">Syntaxe</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=3" title="Modifier la section : Syntaxe" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=3" title="Modifier le code source de la section : Syntaxe"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <figure typeof="mw:File/Thumb"><a href="/wiki/Fichier:Logiquepremierordre_syntaxe.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/c/c1/Logiquepremierordre_syntaxe.svg/292px-Logiquepremierordre_syntaxe.svg.png" decoding="async" width="292" height="175" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/c1/Logiquepremierordre_syntaxe.svg/438px-Logiquepremierordre_syntaxe.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/c1/Logiquepremierordre_syntaxe.svg/584px-Logiquepremierordre_syntaxe.svg.png 2x" data-file-width="292" data-file-height="175" /></a><figcaption>Exemple d'une formule de la logique du premier ordre. Le schéma montre les quantificateurs, les occurrences des symboles de fonctions et des symboles de prédicats.</figcaption></figure> <p>Contrairement à un <a href="/wiki/Langage_naturel" title="Langage naturel">langage naturel</a>, comme le <a href="/wiki/Fran%C3%A7ais" title="Français">français</a>, la logique du premier ordre est un <a href="/wiki/Langage_formel" title="Langage formel">langage formel</a>. Cette section donne une brève présentation de la syntaxe du langage formel du calcul des prédicats. Pour cela, on a besoin d'un <i>alphabet</i>, c'est-à-dire un ensemble de symboles utilisées pour écrire les <i>énoncés</i> (ou <i>formules</i>). On se donne un ensemble des symboles appelés <i><a href="/wiki/Variable_(math%C3%A9matiques)" title="Variable (mathématiques)">variables</a></i>, toujours infini : <span class="mwe-math-element"><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>, <span class="mwe-math-element"><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>, <span class="mwe-math-element"><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>, <abbr class="abbr" title="et cetera">etc.</abbr> </p> <div class="mw-heading mw-heading3"><h3 id="Signature">Signature</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=4" title="Modifier la section : Signature" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=4" title="Modifier le code source de la section : Signature"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>On se donne une signature<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite_crochet">[</span>6<span class="cite_crochet">]</span></a></sup>, c'est-à-dire : </p> <ul><li>un ensemble de symboles de fonctions : <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/132e57acb643253e7810ee9702d9581f159a1c61" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}"></span>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 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>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>h</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle h}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b26be3e694314bc90c3215047e4a2010c6ee184a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}"></span>, <abbr class="abbr" title="et cetera">etc.</abbr> ;</li> <li>un ensemble de symboles de <i>prédicats</i> : <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 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/b4dc73bf40314945ff376bd363916a738548d40a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}"></span>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 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>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>R</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle R}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4b0bfb3769bf24d80e15374dc37b0441e2616e33" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}"></span>, <abbr class="abbr" title="et cetera">etc.</abbr></li></ul> <p>Chaque symbole de fonction et chaque symbole de prédicat a une <i><a href="/wiki/Arit%C3%A9" title="Arité">arité</a></i> : il s'agit du nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle B}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>B</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle B}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/47136aad860d145f75f3eed3022df827cee94d7a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle B}"></span> pour « est bleu(e) » a une arité égale à 1 (on dit qu'il est unaire ou <a href="https://fr.wiktionary.org/wiki/monadique" class="extiw" title="wikt:monadique">monadique</a>), tandis que le prédicat <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle amis}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>a</mi> <mi>m</mi> <mi>i</mi> <mi>s</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle amis}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cd720cb3b650581b7c8907dc4ee8a2f81a616da8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.163ex; height:2.176ex;" alt="{\displaystyle amis}"></span> pour « être amis » a une arité de deux (on dit qu'il est binaire ou dyadique). Il peut y avoir des symboles de fonction ou de prédicat d'arité 0. Un symbole de fonction d'arité 0 s'appelle une <i>constante.</i> Les constantes se notent généralement <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle a}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>a</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle a}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ffd2487510aa438433a2579450ab2b3d557e5edc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.23ex; height:1.676ex;" alt="{\displaystyle a}"></span>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle b}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>b</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle b}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/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>, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle c}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>c</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle c}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.007ex; height:1.676ex;" alt="{\displaystyle c}"></span>, <abbr class="abbr" title="et cetera">etc.</abbr> </p> <div class="mw-heading mw-heading4"><h4 id="Exemples">Exemples</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=5" title="Modifier la section : Exemples" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=5" title="Modifier le code source de la section : Exemples"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li>Si l'on veut parler de personnes, Bob est un symbole de constante, mère(.) est un symbole de fonction d'<span class="nowrap">arité 1</span>, amis(., .) est un symbole de prédicats d'<span class="nowrap">arité 2</span>.</li> <li>Si l'on veut parler d'entiers naturels, « 0, 1 » sont des symboles de constantes. Les symboles <span class="nowrap">+ et ×</span> sont des symboles de fonctions d'<span class="nowrap">arité 2</span>. Les symboles <span class="nowrap">= et ≤</span> sont des symboles de prédicats d'<span class="nowrap">arité 2</span>.</li></ul> <div class="mw-heading mw-heading3"><h3 id="Termes">Termes</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=6" title="Modifier la section : Termes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=6" title="Modifier le code source de la section : Termes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone-css loupe">Article détaillé : <a href="/wiki/Terme_(logique)" title="Terme (logique)">Terme (logique)</a>.</div></div> <p>Les termes sont définis par induction : </p> <ul><li>un symbole de variable est un terme ;</li> <li>un symbole de constante est un terme ;</li> <li>si <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/132e57acb643253e7810ee9702d9581f159a1c61" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}"></span> est un symbole de fonctions d'arité <i>n</i>, et que <i>t</i><sub>1</sub>, …, <i>t<sub>n</sub></i> sont des termes alors <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f(t_{1},\dots ,t_{n})}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> <mo stretchy="false">(</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>,</mo> <mo>…</mo> <mo>,</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f(t_{1},\dots ,t_{n})}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/df8b94d323cd8c7e9e534d8634ffa50162117eea" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.218ex; height:2.843ex;" alt="{\displaystyle f(t_{1},\dots ,t_{n})}"></span> est un terme.</li></ul> <div class="mw-heading mw-heading4"><h4 id="Exemples_2">Exemples</h4><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=7" title="Modifier la section : Exemples" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=7" title="Modifier le code source de la section : Exemples"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li>Bob, mère(Bob), mère(mère(Bob)), mère(x) sont des termes</li> <li><span class="nowrap">0 + 1, x + 3 × y × y</span> sont des termes.</li></ul> <div class="mw-heading mw-heading3"><h3 id="Formule">Formule</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=8" title="Modifier la section : Formule" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=8" title="Modifier le code source de la section : Formule"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Les <i>formules</i> du calcul des prédicats du premier ordre sont définies par induction : </p> <ul><li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(t_{1},\dots ,t_{n})}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>P</mi> <mo stretchy="false">(</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>,</mo> <mo>…</mo> <mo>,</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle P(t_{1},\dots ,t_{n})}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/587aa8d9272ed14bd42569fc66e15e300ccafc39" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.685ex; height:2.843ex;" alt="{\displaystyle P(t_{1},\dots ,t_{n})}"></span> si <span class="mwe-math-element"><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/b4dc73bf40314945ff376bd363916a738548d40a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.745ex; height:2.176ex;" alt="{\displaystyle P}"></span> un symbole de prédicat d'arité <i>n</i> et <i>t</i><sub>1</sub>, …, <i>t<sub>n</sub></i> sont des <a href="/wiki/Terme_(logique)" title="Terme (logique)">termes</a></li> <li>¬<i>e</i> si e est une formule ;</li> <li>(<i>e</i><sub>1</sub>∧<i>e</i><sub>2</sub>) si <i>e</i><sub>1</sub> et <i>e</i><sub>2</sub> sont des formules ;</li> <li>(<i>e</i><sub>1</sub>∨<i>e</i><sub>2</sub>) si <i>e</i><sub>1</sub> et <i>e</i><sub>2</sub> sont des formules ;</li> <li>(<i>e</i><sub>1</sub>→<i>e</i><sub>2</sub>) si <i>e</i><sub>1</sub> et <i>e</i><sub>2</sub> sont des formules ;</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x\;e}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mspace width="thickmathspace" /> <mi>e</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall x\;e}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d1afb460978d294bb27215b5184c0460cc343752" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.351ex; height:2.176ex;" alt="{\displaystyle \forall x\;e}"></span> si <i>e</i> est une formule ;</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\;e}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mspace width="thickmathspace" /> <mi>e</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\;e}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f90239ab4a462f774eef00022c7354c94a558d0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.351ex; height:2.176ex;" alt="{\displaystyle \exists x\;e}"></span> si <i>e</i> est une formule.</li></ul> <p>Une formule de la forme <span class="mwe-math-element"><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(t_{1},\dots ,t_{n})}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>P</mi> <mo stretchy="false">(</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>,</mo> <mo>…</mo> <mo>,</mo> <msub> <mi>t</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>n</mi> </mrow> </msub> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle P(t_{1},\dots ,t_{n})}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/587aa8d9272ed14bd42569fc66e15e300ccafc39" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.685ex; height:2.843ex;" alt="{\displaystyle P(t_{1},\dots ,t_{n})}"></span> s'appelle un <i>atome</i> ou une <i>formule atomique</i>. Les symboles <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/099107443792f5fec9bebe39b919a690db7198c1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \lnot }"></span> (<i>non</i>), <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∧</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \land }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d6823e5a222eb3ca49672818ac3d13ec607052c4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \land }"></span> (<i>et</i>), <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lor }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∨</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lor }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ab47f6b1f589aedcf14638df1d63049d233d851a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \lor }"></span> (<i>ou</i>) et <span class="mwe-math-element"><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> (<i>implique</i>), qui sont des <i>connecteurs</i> que possède aussi le <a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">calcul des propositions</a>. Les symboles <span class="mwe-math-element"><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 }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bfc1a1a9c4c0f8d5df989c98aa2773ed657c5937" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \forall }"></span> (<i>quel que soit</i>) et <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/77ed842b6b90b2fdd825320cf8e5265fa937b583" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \exists }"></span> (<i>il existe</i>), appelés <i>quantificateurs</i>. On pourrait se contenter d'un seul quantificateur <span class="mwe-math-element"><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 }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bfc1a1a9c4c0f8d5df989c98aa2773ed657c5937" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \forall }"></span> et de deux connecteurs logiques <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/099107443792f5fec9bebe39b919a690db7198c1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \lnot }"></span> et <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>∧</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \land }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d6823e5a222eb3ca49672818ac3d13ec607052c4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \land }"></span> en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\;P(x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mspace width="thickmathspace" /> <mi>P</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\;P(x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7c76e3fc072f0a37da2ee414b2172676bf0b5ef1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.152ex; height:2.843ex;" alt="{\displaystyle \exists x\;P(x)}"></span> est défini comme <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot (\forall x\;\lnot P(x))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mspace width="thickmathspace" /> <mi mathvariant="normal">¬</mi> <mi>P</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot (\forall x\;\lnot P(x))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/3a084598663cadd2af887369feb88f9055d4ebf9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.062ex; height:2.843ex;" alt="{\displaystyle \lnot (\forall x\;\lnot P(x))}"></span>. Les symboles de parenthèses « ) » et « ( » sont comparables aux symboles de ponctuations dans une langue naturelle. On appelle <i>énoncé</i> une formule dont toutes les variables sont liées par un quantificateur (donc qui n'a pas de <a href="/wiki/Variable_libre" title="Variable libre">variable libre</a>). </p> <div class="mw-heading mw-heading3"><h3 id="Exemples_3">Exemples</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=9" title="Modifier la section : Exemples" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=9" title="Modifier le code source de la section : Exemples"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <dl><dt>Exemple 1</dt></dl> <p>Si on se donne pour constantes les deux symboles <span class="nowrap">0 et 1</span>, pour symboles de fonctions binaires <span class="nowrap">+ et .</span>, et pour symboles de prédicats binaires les symboles <span class="nowrap">= et <</span>, alors le langage utilisé peut être interprété comme étant celui de l'arithmétique. <span class="nowrap"><i>x</i> et <i>y</i></span> désignant des variables, <span class="nowrap"><i>x</i> + 1</span> est un <a href="/wiki/Terme_(logique)" title="Terme (logique)">terme</a>, <span class="nowrap">0 + 1 + 1</span> est un <a href="/wiki/Terme_(logique)" title="Terme (logique)">terme</a> clos, <span class="nowrap"><i>x</i> < <i>y</i> + 1</span> est une formule, <span class="nowrap">0 + 1 + 1 < 0 + 1 + 1 +1</span> est une formule close. </p> <dl><dt>Exemple 2</dt></dl> <p>Si on se donne un ensemble de variables quelconque, une constante notée « <i>e</i> », un symbole de fonction binaire noté « * », un symbole de fonction unaire notée « <sup>-1</sup> », un symbole de <a href="/wiki/Relation_binaire" title="Relation binaire">relation binaire</a> « = », alors le langage utilisé peut être interprété comme étant celui de la <a href="/wiki/Th%C3%A9orie_des_groupes" title="Théorie des groupes">théorie des groupes</a>. Si <span class="nowrap"><i>x</i> et <i>y</i></span> désignent des variables, <span class="nowrap"><i>x</i> * <i>y</i></span> est un terme, <span class="nowrap"><i>e</i> * <i>e</i></span> est un terme clos, <span class="nowrap"><i>x</i> = <i>y</i> * <i>y</i></span> est une formule, <span class="nowrap"><i>e</i> = <i>e</i> * <i>e</i><sup>-1</sup></span> et (<span class="nowrap"><i>e</i><sup>-1</sup> * <i>e</i>)<sup>-1</sup> = (<i>e</i><sup>-1</sup>)<sup>-1</sup></span> sont des formules closes. </p> <div class="mw-heading mw-heading3"><h3 id="Prédicats,_formules_closes,_formules_polies,_variables_libres,_variables_liées"><span id="Pr.C3.A9dicats.2C_formules_closes.2C_formules_polies.2C_variables_libres.2C_variables_li.C3.A9es"></span>Prédicats, formules closes, formules polies, variables libres, variables liées</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=10" title="Modifier la section : Prédicats, formules closes, formules polies, variables libres, variables liées" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=10" title="Modifier le code source de la section : Prédicats, formules closes, formules polies, variables libres, variables liées"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Lorsqu’une variable <span class="mwe-math-element"><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> appartient à une sous-formule précédée d’un quantificateur, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1a3fa2fb002baecbc5038bd3dd42bab57448b315" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.622ex; height:2.176ex;" alt="{\displaystyle \forall x}"></span> ou <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ab833914405cde960b3b9af3feaa9e4fef96ffa9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.622ex; height:2.176ex;" alt="{\displaystyle \exists x}"></span>, elle est dite liée par ce quantificateur. Si une variable n’est liée par aucun quantificateur, elle est libre. </p><p>La distinction entre variable libre et variable liée est importante. Une variable liée ne possède pas d'identité propre et peut être remplacée par n'importe quel autre nom de variable qui n'apparaît pas dans la formule. Ainsi, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x(x<y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo><</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x(x<y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/db8fd474af5254988acf1237bfb770f619695b3c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.015ex; height:2.843ex;" alt="{\displaystyle \exists x(x<y)}"></span> est identique à <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists z(z<y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>z</mi> <mo stretchy="false">(</mo> <mi>z</mi> <mo><</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists z(z<y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bcea8ed0a10103897f9c4191464b3347e7d4884a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.532ex; height:2.843ex;" alt="{\displaystyle \exists z(z<y)}"></span> mais pas à <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x(x<z)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo><</mo> <mi>z</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x(x<z)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/839ee45c5f00b82fe48b512895c242b93ce36283" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.948ex; height:2.843ex;" alt="{\displaystyle \exists x(x<z)}"></span> et encore moins à <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists y(y<y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>y</mi> <mo stretchy="false">(</mo> <mi>y</mi> <mo><</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists y(y<y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/70a26d917ca3fd587b750ffd1cd9d8fc3a7fb916" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.667ex; height:2.843ex;" alt="{\displaystyle \exists y(y<y)}"></span>. </p><p>Une formule close est une formule dont toutes les variables sont liées. Un prédicat est une formule qui contient une ou plusieurs variables libres. On peut considérer les prédicats comme des concepts. Ainsi, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x\exists y(x<y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi mathvariant="normal">∃</mi> <mi>y</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo><</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall x\exists y(x<y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/20a1cd8cadaf1a91bc579af4f75b37f0f879536f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.463ex; height:2.843ex;" alt="{\displaystyle \forall x\exists y(x<y)}"></span> est une formule close du langage de l'arithmétique. <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x(x<z)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo><</mo> <mi>z</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall x(x<z)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/74efecb698ce91f34fdf3ff97ec78eb6de77264a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.948ex; height:2.843ex;" alt="{\displaystyle \forall x(x<z)}"></span> est un prédicat portant sur la variable <i>z</i>. </p><p>Une formule est dite <b>polie</b> lorsque d'une part aucune variable n'y a à la fois d'occurrences libres et d'occurrences liées et que d'autre part aucune variable liée n'est soumise à plus d'une <i>mutification</i> (on dit qu'un signe est <i>mutificateur</i> lorsqu'il permet de confirmer l'hypothèse d'une variable liée). </p> <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone-css loupe">Article détaillé : <a href="/wiki/Variable_libre" title="Variable libre">Variable libre</a>.</div></div> <div class="mw-heading mw-heading2"><h2 id="Sémantique"><span id="S.C3.A9mantique"></span>Sémantique</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=11" title="Modifier la section : Sémantique" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=11" title="Modifier le code source de la section : Sémantique"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/Fichier:Logiquepremierordre_modele_exemple.png" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/6/6f/Logiquepremierordre_modele_exemple.png/220px-Logiquepremierordre_modele_exemple.png" decoding="async" width="220" height="196" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/6/6f/Logiquepremierordre_modele_exemple.png/330px-Logiquepremierordre_modele_exemple.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/6/6f/Logiquepremierordre_modele_exemple.png/440px-Logiquepremierordre_modele_exemple.png 2x" data-file-width="767" data-file-height="684" /></a><figcaption>Voici un modèle pour la logique du premier ordre. Le domaine a trois éléments : un bonhomme de neige, un oiseau et une cerise. Le modèle permet d'interpréter un prédicat binaire <span class="mwe-math-element"><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 {aime} }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \mathrm {aime} }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6255ed667fd0c60269df9d5f4f7b238d552ec317" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.778ex; height:2.176ex;" alt="{\displaystyle \mathrm {aime} }"></span> : le bonhomme de neige aime l'oiseau, l'oiseau aime tout le monde (y compris lui-même) et la cerise n'aime personne.</figcaption></figure> <p>La théorie de la vérité des formules du calcul des prédicats a été appelée par <a href="/wiki/Alfred_Tarski" title="Alfred Tarski">Tarski</a> sa sémantique<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. </p><p>Une <i>interprétation</i> d'un langage du premier ordre dans un domaine d'interprétation, appelé aussi <i>modèle</i> du langage, décrit les valeurs prises par les constituants du premier ordre (variables, symboles de constantes, termes) et les relations associées aux prédicats. Chaque énoncé se voit attribuer une <a href="/wiki/Valeur_de_v%C3%A9rit%C3%A9" title="Valeur de vérité">valeur de vérité</a>. L'étude des interprétations des langages formels est appelée <i>sémantique formelle</i> ou <i>théorie des modèles</i>. Ce qui suit est une description de la sémantique standard ou tarskienne pour la logique du premier ordre. Il existe d'autres types de sémantique, notamment la <a href="/w/index.php?title=S%C3%A9mantique_des_jeux&action=edit&redlink=1" class="new" title="Sémantique des jeux (page inexistante)">sémantique des jeux</a>, qui ne sont pas détaillés dans cet article. </p> <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone-css loupe">Article détaillé : <a href="/wiki/Th%C3%A9orie_des_mod%C3%A8les" title="Théorie des modèles">Théorie des modèles</a>.</div></div> <div class="mw-heading mw-heading3"><h3 id="Modèle"><span id="Mod.C3.A8le"></span>Modèle</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=12" title="Modifier la section : Modèle" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=12" title="Modifier le code source de la section : Modèle"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Un modèle M d'un langage du premier ordre est une structure : c'est un ensemble d'éléments (appelé domaine) dans lequel on donne un sens aux symboles du langage. Généralement, si le langage possède un prédicat binaire pour le symbole d'égalité « = », alors son interprétation dans la structure est l'égalité. </p> <div class="mw-heading mw-heading3"><h3 id="Conditions_de_vérité"><span id="Conditions_de_v.C3.A9rit.C3.A9"></span>Conditions de vérité</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=13" title="Modifier la section : Conditions de vérité" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=13" title="Modifier le code source de la section : Conditions de vérité"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Un modèle donne une valeur de vérité (<i>vrai</i> ou <i>faux</i>) à toute formule close du langage. Les conditions de vérité sont définies par <a href="/wiki/Induction_structurelle" title="Induction structurelle">induction structurelle</a> sur les formules. Par exemple, dans le modèle ci-contre : </p> <ul><li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/495214cd25f8c94fa4d305fa307de7c634f1d3e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.757ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"></span> est vraie dans le modèle M car il existe un élément (l'oiseau) qui aime tout le monde ;</li> <li><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\lnot \mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mi mathvariant="normal">¬</mi> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\lnot \mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/89cb4ef856fbc267acb1ceea1088b215672bbe81" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.307ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\lnot \mathrm {aime} (x,y)}"></span> est vraie dans le modèle M car il existe un élément (la cerise) qui n'aime personne.</li></ul> <div class="mw-heading mw-heading3"><h3 id="Formule_satisfaisable">Formule satisfaisable</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=14" title="Modifier la section : Formule satisfaisable" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=14" title="Modifier le code source de la section : Formule satisfaisable"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Une formule est <b>satisfaisable</b> s'il existe un modèle M qui la rend vraie. Par exemple <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/495214cd25f8c94fa4d305fa307de7c634f1d3e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.757ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"></span> est satisfaisable. </p> <div class="mw-heading mw-heading3"><h3 id="Formule_valide">Formule valide</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=15" title="Modifier la section : Formule valide" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=15" title="Modifier le code source de la section : Formule valide"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>On dit qu'une formule F du langage est une formule <b>valide</b> si cette formule est vraie dans tout modèle du langage, ce qu'on note <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \vDash F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>⊨</mo> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \vDash F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d0e28b18555015b07471b4673e3dde123131c8df" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.401ex; height:2.843ex;" alt="{\displaystyle \vDash F}"></span>. Par exemple, la formule <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)\to \forall y\exists x~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)\to \forall y\exists x~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bc97e88cb8d73fc3401ea444fe6357ae8eeed0d9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.128ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)\to \forall y\exists x~\mathrm {aime} (x,y)}"></span> est une formule valide. Dans un modèle M, si <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/495214cd25f8c94fa4d305fa307de7c634f1d3e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.757ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}"></span> est vraie alors, il existe un élément <span class="mwe-math-element"><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> dans le domaine qui aime tout le monde. Mais alors tout le monde est aimé et donc la formule <span class="mwe-math-element"><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 y\exists x~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall y\exists x~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/021b5674e02a3cc397014bb8b44b8cf314c47595" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.757ex; height:2.843ex;" alt="{\displaystyle \forall y\exists x~\mathrm {aime} (x,y)}"></span> est vraie dans le modèle M. L'implication étant vraie dans tout modèle M, la formule est valide. </p><p>Par contre, la formule <span class="mwe-math-element"><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 y\exists x~\mathrm {aime} (x,y)\to \exists x\forall y~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall y\exists x~\mathrm {aime} (x,y)\to \exists x\forall y~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c555e7e312bd2cce2b71dd9a0ac95f6467c4a80d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.128ex; height:2.843ex;" alt="{\displaystyle \forall y\exists x~\mathrm {aime} (x,y)\to \exists x\forall y~\mathrm {aime} (x,y)}"></span> n'est pas valide. En effet, dans un modèle avec deux éléments {<i>a</i>, <i>b</i>} et où <span class="mwe-math-element"><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 {aime} }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \mathrm {aime} }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6255ed667fd0c60269df9d5f4f7b238d552ec317" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.778ex; height:2.176ex;" alt="{\displaystyle \mathrm {aime} }"></span> est interprété par a n'aime que a et b n'aime que b, la formule <span class="mwe-math-element"><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 y\exists x\;~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mspace width="thickmathspace" /> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall y\exists x\;~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4d008aec49e7394a22f4081dbb89c16448b9dc75" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.402ex; height:2.843ex;" alt="{\displaystyle \forall y\exists x\;~\mathrm {aime} (x,y)}"></span> est vraie alors que <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\forall y\;~\mathrm {aime} (x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>x</mi> <mi mathvariant="normal">∀</mi> <mi>y</mi> <mspace width="thickmathspace" /> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">a</mi> <mi mathvariant="normal">i</mi> <mi mathvariant="normal">m</mi> <mi mathvariant="normal">e</mi> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists x\forall y\;~\mathrm {aime} (x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c594bb8a9a3612277625a4c7c5a537d1f431b36b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.402ex; height:2.843ex;" alt="{\displaystyle \exists x\forall y\;~\mathrm {aime} (x,y)}"></span> est fausse. L'implication est donc fausse dans le modèle et la formule n'est pas valide. </p> <div class="mw-heading mw-heading3"><h3 id="Conséquence_sémantique"><span id="Cons.C3.A9quence_s.C3.A9mantique"></span>Conséquence sémantique</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=16" title="Modifier la section : Conséquence sémantique" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=16" title="Modifier le code source de la section : Conséquence sémantique"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>On dit que F est conséquence sémantique d'une théorie T si, tout modèle qui satisfait toutes les formules de T satisfait aussi F. </p> <div class="mw-heading mw-heading2"><h2 id="Système_de_déduction"><span id="Syst.C3.A8me_de_d.C3.A9duction"></span>Système de déduction</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=17" title="Modifier la section : Système de déduction" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=17" title="Modifier le code source de la section : Système de déduction"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Dans le calcul des prédicats, on peut également déduire des formules au moyen de déductions relevant d'un calcul. Une déduction consiste à partir d’hypothèses, ou d'axiomes, à progresser par étapes logiques jusqu'à une conclusion selon des règles prédéfinies. Il existe plusieurs présentations possibles de ces axiomes et de ces règles : </p> <ul><li>la <a href="/wiki/D%C3%A9duction_naturelle" title="Déduction naturelle">déduction naturelle</a>. Les principes logiques y sont présentés d’une façon aussi proche que possible des raisonnements naturels. Elle consiste en une liste de treize règles. Elles pourraient être réduites à un plus petit nombre, mais l'évidence des principes serait moins naturelle ;</li> <li>le <a href="/wiki/Calcul_des_s%C3%A9quents" title="Calcul des séquents">calcul des séquents</a> ;</li> <li>la <a href="/wiki/R%C3%A8gle_de_r%C3%A9solution" title="Règle de résolution">résolution</a> ;</li> <li>les <a href="/wiki/Axiome_logique" title="Axiome logique">axiomes logiques</a>. Plusieurs systèmes d’axiomes équivalents peuvent être proposés. Cette approche, adoptée par presque tous les logiciens depuis les <a href="/wiki/Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a> de <a href="/wiki/Alfred_North_Whitehead" title="Alfred North Whitehead">Whitehead</a> et <a href="/wiki/Bertrand_Russell" title="Bertrand Russell">Russell</a>, a une grande importance à la fois <a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">métamathématique</a> et historique. L'un des systèmes d'axiomes le plus court est constitué du triplet suivant : <dl><dt>Les axiomes du <a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">calcul des propositions</a></dt> <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 f\to (g\to f)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>g</mi> <mo stretchy="false">→</mo> <mi>f</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f\to (g\to f)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2bdceda7ae65d1b268500089d63288460b5212ec" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.711ex; height:2.843ex;" alt="{\displaystyle f\to (g\to f)}"></span></dd> <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 (f\to (g\to h))\to ((f\to g)\to (f\to h))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>f</mi> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>g</mi> <mo stretchy="false">→</mo> <mi>h</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi>f</mi> <mo stretchy="false">→</mo> <mi>g</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>f</mi> <mo stretchy="false">→</mo> <mi>h</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (f\to (g\to h))\to ((f\to g)\to (f\to h))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5275e3f5d3dcbac9278572d2f039733a54afb850" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:39.477ex; height:2.843ex;" alt="{\displaystyle (f\to (g\to h))\to ((f\to g)\to (f\to h))}"></span></dd> <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 (\lnot f\to g)\to ((\lnot f\to \lnot g)\to f)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>f</mi> <mo stretchy="false">→</mo> <mi>g</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <mi>f</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">¬</mi> <mi>g</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>f</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (\lnot f\to g)\to ((\lnot f\to \lnot g)\to f)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e18342ee0125807d00be93dd6da5c3bfb11580ab" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.603ex; height:2.843ex;" alt="{\displaystyle (\lnot f\to g)\to ((\lnot f\to \lnot g)\to f)}"></span></dd> <dd>les axiomes relatifs au quantificateur <span class="mwe-math-element"><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 }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/bfc1a1a9c4c0f8d5df989c98aa2773ed657c5937" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.293ex; height:2.176ex;" alt="{\displaystyle \forall }"></span></dd> <dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x(f\to g(x))\to (f\to \forall xg(x))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mo stretchy="false">(</mo> <mi>f</mi> <mo stretchy="false">→</mo> <mi>g</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mo stretchy="false">(</mo> <mi>f</mi> <mo stretchy="false">→</mo> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>g</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall x(f\to g(x))\to (f\to \forall xg(x))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b63e07697fc21f6b399afca512850953ea3886f0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.772ex; height:2.843ex;" alt="{\displaystyle \forall x(f\to g(x))\to (f\to \forall xg(x))}"></span> où <i>x</i> n'est pas libre dans <i>f</i></dd> <dd><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall xf(x)\to f(a)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>f</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo stretchy="false">→</mo> <mi>f</mi> <mo stretchy="false">(</mo> <mi>a</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall xf(x)\to f(a)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/40ec19d46997c4e29ebed3f62c1442d869d0b5c2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.972ex; height:2.843ex;" alt="{\displaystyle \forall xf(x)\to f(a)}"></span> où <i>x</i> n'a pas d'occurrence libre dans une partie bien formée de <i>f</i> de la forme <span class="mwe-math-element"><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 a,h}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>a</mi> <mo>,</mo> <mi>h</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall a,h}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8cf5e66f9e0abb9e6dc98dd691010851de1a1a41" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.895ex; height:2.509ex;" alt="{\displaystyle \forall a,h}"></span> (ceci pour éviter une substitution embarrassante si par exemple, <i>f</i>(<i>x</i>) est de la forme <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists a,a<x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∃</mi> <mi>a</mi> <mo>,</mo> <mi>a</mi> <mo><</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists a,a<x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6a750b011442fa695a051c5f05e147cb1bc7161f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.214ex; height:2.509ex;" alt="{\displaystyle \exists a,a<x}"></span>).</dd> <dt>La règle du <a href="/wiki/Modus_ponens" title="Modus ponens">modus ponens</a></dt> <dd>si on a prouvé <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f\to g}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> <mo stretchy="false">→</mo> <mi>g</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f\to g}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c84570496acc2eb5f52272d6b679963565b2c312" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.009ex; height:2.509ex;" alt="{\displaystyle f\to g}"></span> et <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/132e57acb643253e7810ee9702d9581f159a1c61" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}"></span>, alors on a prouvé <span class="mwe-math-element"><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></dd> <dt>La règle de généralisation</dt> <dd>si on a prouvé <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f(x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f(x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/202945cce41ecebb6f643f31d119c514bec7a074" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.418ex; height:2.843ex;" alt="{\displaystyle f(x)}"></span>, alors on a prouvé <span class="mwe-math-element"><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 xf(x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>x</mi> <mi>f</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall xf(x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d961b46641b409934c57c4cd15146b939112946e" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.04ex; height:2.843ex;" alt="{\displaystyle \forall xf(x)}"></span> (puisque le <i>x</i> de la première preuve joue un rôle arbitraire).</dd></dl></li></ul> <p>Mais si la recherche de systèmes d'axiomes minimaux met en évidence les principes élémentaires sur lesquels peuvent s'appuyer tous les raisonnements, elle ne montre pas le caractère d’évidence naturelle des principes logiques plus généraux : </p> <ul><li>la <a href="/wiki/Logique_du_dialogue" title="Logique du dialogue">logique du dialogue</a> apporte également un autre éclairage sur la nature des lois logiques ;</li> <li>voir aussi <a href="/wiki/Correspondance_de_Curry-Howard" title="Correspondance de Curry-Howard">correspondance de Curry-Howard</a>.</li></ul> <p>Quelle que soit la présentation abordée, les axiomes et règles peuvent être codés de façon qu'une machine puisse vérifier la validité ou non d'une déduction conduisant à une formule F. Si la déduction est correcte, la formule F est appelé <i>théorème</i>. On dit aussi qu'elle est <i>prouvable</i>, ce qu'on note <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \vdash F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>⊢</mo> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \vdash F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f56e296a4e7254b2645914a063bec335c64310a2" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.806ex; height:2.176ex;" alt="{\displaystyle \vdash F}"></span>. </p> <div class="mw-heading mw-heading2"><h2 id="Propriétés"><span id="Propri.C3.A9t.C3.A9s"></span>Propriétés</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=18" title="Modifier la section : Propriétés" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=18" title="Modifier le code source de la section : Propriétés"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Complétude"><span id="Compl.C3.A9tude"></span>Complétude</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=19" title="Modifier la section : Complétude" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=19" title="Modifier le code source de la section : Complétude"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone-css loupe">Article détaillé : <a href="/wiki/Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del" title="Théorème de complétude de Gödel">Théorème de complétude de Gödel</a>.</div></div> <p>Le <a href="/wiki/Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del" title="Théorème de complétude de Gödel">théorème de complétude</a> dit que F est valide est équivalent à F est prouvable. Mieux, on parle de complétude forte : si F est conséquence sémantique d'une théorie T alors F est prouvable à partir de T. </p> <div class="mw-heading mw-heading3"><h3 id="Indécidabilité"><span id="Ind.C3.A9cidabilit.C3.A9"></span>Indécidabilité</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=20" title="Modifier la section : Indécidabilité" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=20" title="Modifier le code source de la section : Indécidabilité"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Tous les systèmes logiques ne sont pas décidables, autrement dit bien qu'ils soient parfaitement définis, il n'existe pas toujours un <a href="/wiki/Algorithme" title="Algorithme">algorithme</a> pour dire si une formule est oui ou non un théorème. D'ailleurs historiquement la <a href="/wiki/Th%C3%A9orie_de_la_calculabilit%C3%A9" title="Théorie de la calculabilité">théorie de la calculabilité</a> s'est construite pour démontrer précisément leur indécidabilité. Avant de développer ces résultats, voici résumé ce qu'on sait sur la décidabilité et l'indécidabilité des systèmes logiques. </p> <ul><li><i>Calcul propositionnel :</i> décidable et complet. Pour la décidabilité, il y a donc une procédure effective pour décider si une formule du calcul propositionnel est satisfaisable, c'est-à-dire que l'on peut affecter aux variables propositionnelles des valeurs de vérité qui la rendent vraie, mais le problème, nommé <a href="/wiki/Probl%C3%A8me_SAT" title="Problème SAT">problème SAT</a>, est <a href="/wiki/Probl%C3%A8me_NP-complet" title="Problème NP-complet">NP-complet</a>, c'est-à-dire que tous les algorithmes déterministes connus de recherche d'une solution sont en temps exponentiel par rapport au nombre de variables (voir l'article <a href="/wiki/Probl%C3%A8me_SAT" title="Problème SAT">Problème SAT</a>).</li> <li><i>Calcul des prédicats du premier ordre monadique</i>, c'est-à-dire réduit aux relations unaires et sans fonctions : décidable et complet, par réduction au calcul propositionnel.</li> <li><i>Calcul des prédicats du premier ordre :</i> réductible au calcul des prédicats dyadique, soit avec au plus des prédicats binaires (comme il en est en théorie des ensembles n'ayant que l'appartenance et l'égalité comme symboles primitifs) : semi-décidable et <a href="/wiki/Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del" title="Théorème de complétude de Gödel">complet</a>.</li> <li><i><a href="/wiki/Logique_d%27ordre_sup%C3%A9rieur#Logique_du_second_ordre" title="Logique d'ordre supérieur">Calcul des prédicats de deuxième ordre</a></i> : [<i>quid</i> sur sa décidabilité], et <span class="need_ref" title="Une source est souhaitée pour ce passage (demandé le 28 mai 2018)." style="cursor:help;">théorème de complétude partiel sur une sous-classe de formules</span><sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire">[<abbr class="abbr" title="référence">réf.</abbr> souhaitée]</a></sup>.</li> <li><i><a href="/wiki/Logique_d%27ordre_sup%C3%A9rieur" title="Logique d'ordre supérieur">Calcul des prédicats d'ordre supérieur</a></i> : <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone"><span class="mw-valign-text-top noviewer" typeof="mw:File"><a href="/wiki/Fichier:Fairytale_warning.png" class="mw-file-description"><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/8/87/Fairytale_warning.png/17px-Fairytale_warning.png" decoding="async" width="17" height="17" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/8/87/Fairytale_warning.png/26px-Fairytale_warning.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/8/87/Fairytale_warning.png/34px-Fairytale_warning.png 2x" data-file-width="64" data-file-height="64" /></a></span></div><div class="bandeau-cell">Cette section est vide, insuffisamment détaillée ou incomplète. <a href="/wiki/Sp%C3%A9cial:EditPage/Calcul_des_pr%C3%A9dicats" title="Spécial:EditPage/Calcul des prédicats">Votre aide</a> est la bienvenue ! <a href="/wiki/Aide:Comment_modifier_une_page" title="Aide:Comment modifier une page">Comment faire ?</a></div></div></li></ul> <p>Le calcul des prédicats est semi-décidable, dans le sens où une machine peut énumérer les théorèmes les uns après les autres. Mais, contrairement au <a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">calcul des propositions</a>, il n'est pas en général <a href="/wiki/D%C3%A9cidabilit%C3%A9" title="Décidabilité">décidable</a> dans le sens où il n'existe pas de moyen « mécanique » qui, si on se donne une formule F, permette de décider si F est un théorème ou non. La semi-décidabilité ne permet pas de conclure : la confrontation de F avec la liste des théorèmes se terminera si F est effectivement un théorème, mais dans l'attente de la terminaison, a priori on ne sait pas si le calcul des théorèmes n'a pas été mené assez loin pour identifier F comme théorème ou si ce calcul ne se terminera pas parce que F n'est pas un théorème. </p><p>Cela dépend cependant du langage utilisé, en particulier du choix des symboles primitifs (la signature). Le calcul des prédicats égalitaire monadique (n'ayant que des symboles de prédicats unaires et pas de symbole de fonction) est décidable. Le calcul des prédicats égalitaire pour un langage comportant au moins un symbole de prédicat binaire est indécidable (algorithmiquement). </p><p>Des fragments syntaxiques sont décidables comme la <a href="/wiki/Logique_monadique_du_premier_ordre" title="Logique monadique du premier ordre">logique monadique du premier ordre</a> ou la <a href="/wiki/Classe_de_Bernays-Sch%C3%B6nfinkel" title="Classe de Bernays-Schönfinkel">classe de Bernays-Schönfinkel</a>. </p> <div class="mw-heading mw-heading3"><h3 id="Compacité"><span id="Compacit.C3.A9"></span>Compacité</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=21" title="Modifier la section : Compacité" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=21" title="Modifier le code source de la section : Compacité"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Voir <a href="/wiki/Th%C3%A9or%C3%A8me_de_compacit%C3%A9" title="Théorème de compacité">théorème de compacité</a>. </p> <div class="mw-heading mw-heading3"><h3 id="Expressivité"><span id="Expressivit.C3.A9"></span>Expressivité</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=22" title="Modifier la section : Expressivité" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=22" title="Modifier le code source de la section : Expressivité"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Une application intéressante du théorème de compacité est qu'il n'existe pas de formules qui exprime « le domaine est infini ». </p> <div class="mw-heading mw-heading3"><h3 id="Théorème_de_Löwenheim-Skolem"><span id="Th.C3.A9or.C3.A8me_de_L.C3.B6wenheim-Skolem"></span>Théorème de Löwenheim-Skolem</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=23" title="Modifier la section : Théorème de Löwenheim-Skolem" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=23" title="Modifier le code source de la section : Théorème de Löwenheim-Skolem"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Voir <a href="/wiki/Th%C3%A9or%C3%A8me_de_L%C3%B6wenheim-Skolem" title="Théorème de Löwenheim-Skolem">théorème de Löwenheim-Skolem</a>. </p> <div class="bandeau-container bandeau-section metadata bandeau-niveau-information"><div class="bandeau-cell bandeau-icone-css loupe">Article détaillé : <a href="/wiki/Th%C3%A9or%C3%A8me_de_L%C3%B6wenheim-Skolem" title="Théorème de Löwenheim-Skolem">théorème de Löwenheim-Skolem</a>.</div></div> <div class="mw-heading mw-heading3"><h3 id="Incomplétude"><span id="Incompl.C3.A9tude"></span>Incomplétude</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=24" title="Modifier la section : Incomplétude" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=24" title="Modifier le code source de la section : Incomplétude"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>En un sens différent, les <a href="/wiki/Th%C3%A9orie_axiomatique" title="Théorie axiomatique">théories</a> « raisonnables »<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite_crochet">[</span>note 1<span class="cite_crochet">]</span></a></sup> qui permettent de formaliser suffisamment l'arithmétique intuitive, comme l'<a href="/wiki/Axiomes_de_Peano" title="Axiomes de Peano">arithmétique de Peano</a>, ou la <a href="/wiki/Th%C3%A9orie_des_ensembles" title="Théorie des ensembles">théorie des ensembles</a> ne sont pas <a href="/wiki/Compl%C3%A9tude" class="mw-disambig" title="Complétude">complètes</a> : il existe un énoncé non démontrable dont la négation est également non démontrable (voir <a href="/wiki/Th%C3%A9or%C3%A8mes_d%27incompl%C3%A9tude_de_G%C3%B6del" title="Théorèmes d'incomplétude de Gödel">théorèmes d'incomplétude de Gödel</a>). </p> <div class="mw-heading mw-heading2"><h2 id="Fragments_décidables"><span id="Fragments_d.C3.A9cidables"></span>Fragments décidables</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=25" title="Modifier la section : Fragments décidables" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=25" title="Modifier le code source de la section : Fragments décidables"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Le problème de satisfiabilité d'une formule de la logique du premier ordre est indécidable. Mais en se restreignant à certaines classes de formules, le problème de satisfiabilité devient décidable. Le tableau suivant énumère quelques fragments décidables<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite_crochet">[</span>7<span class="cite_crochet">]</span></a></sup>. </p> <table class="wikitable"> <caption> </caption> <tbody><tr> <th>Fragments </th></tr> <tr> <td>Fragment monadique et symboles de fonction d'arité 1 </td></tr> <tr> <td>Fragment à deux variables seulement </td></tr> <tr> <td><a href="/wiki/Classe_de_Bernays-Sch%C3%B6nfinkel" title="Classe de Bernays-Schönfinkel">Classe de Bernays-Schönfinkel</a>, Classe <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists ^{*}\forall ^{*}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> <msup> <mi mathvariant="normal">∀</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists ^{*}\forall ^{*}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/200969b147f0d4a65c93265041be5719d49bd6c1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.694ex; height:2.343ex;" alt="{\displaystyle \exists ^{*}\forall ^{*}}"></span> sans symboles de fonction et égalité </td></tr> <tr> <td>Classe <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> <msup> <mi mathvariant="normal">∀</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msup> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7326b4a887e38036bc8d040ba428e3f56653c4ad" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.04ex; height:2.676ex;" alt="{\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}"></span> sans symboles de fonction </td></tr> <tr> <td>Classe <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists ^{*}\forall \exists ^{*}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> <mi mathvariant="normal">∀</mi> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists ^{*}\forall \exists ^{*}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/993f7b598e4bb191fc898ae639960dde33447bf0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.986ex; height:2.343ex;" alt="{\displaystyle \exists ^{*}\forall \exists ^{*}}"></span> avec symboles de fonction </td></tr> <tr> <td>Classe <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists ^{*}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists ^{*}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5c5566f5a9111f53dd6d75e51a9965f04b05f9b6" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.347ex; height:2.343ex;" alt="{\displaystyle \exists ^{*}}"></span> avec symboles de fonction et égalité </td></tr> <tr> <td>Fragment monadique avec symboles de fonction d'arité et égalité </td></tr> <tr> <td>Classe <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists ^{*}\forall \exists ^{*}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> <mi mathvariant="normal">∀</mi> <msup> <mi mathvariant="normal">∃</mi> <mrow class="MJX-TeXAtom-ORD"> <mo>∗</mo> </mrow> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \exists ^{*}\forall \exists ^{*}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/993f7b598e4bb191fc898ae639960dde33447bf0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.986ex; height:2.343ex;" alt="{\displaystyle \exists ^{*}\forall \exists ^{*}}"></span> avec symboles de fonction d'arité un, et égalité </td></tr></tbody></table> <div class="mw-heading mw-heading2"><h2 id="Variantes">Variantes</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=26" title="Modifier la section : Variantes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=26" title="Modifier le code source de la section : Variantes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Le <a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">calcul des propositions</a> est un fragment syntaxique de la logique du premier ordre où il n'y a pas de variables et où tous les prédicats sont d'arité 0<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. </p><p>La <a href="/wiki/Logique_modale" title="Logique modale">logique modale</a> propositionnelle et la <a href="/wiki/Logique_de_description" title="Logique de description">logique de description</a> sont des fragments syntaxiques de la logique du premier ordre<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. D'ailleurs, toute formule du premier ordre qui est invariante par <a href="/wiki/Bisimulation" title="Bisimulation">bisimulation</a> est équivalente à une formule de la logique modale : c'est le théorème de Van Benthem<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. La logique du premier ordre a aussi été étendu à la logique modale du premier ordre<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. La logique de la dépendance (<i><span class="lang-en" lang="en">dependence logic</span></i>) est une généralisation de la logique du premier ordre où les dépendances entre variables sont explicitement décrites dans le langage<sup class="need_ref_tag" style="padding-left:2px;"><a href="/wiki/Aide:R%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Aide:Référence nécessaire"><span title="Ce passage nécessite une référence (demandé le 25 mai 2016) ; voir l'aide.">[réf. nécessaire]</span></a></sup>. </p> <div class="mw-heading mw-heading2"><h2 id="Notes_et_références"><span id="Notes_et_r.C3.A9f.C3.A9rences"></span>Notes et références</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=27" title="Modifier la section : Notes et références" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=27" title="Modifier le code source de la section : Notes et références"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Notes">Notes</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=28" title="Modifier la section : Notes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=28" title="Modifier le code source de la section : Notes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="references-small decimal" style=""><div class="mw-references-wrap"><ol class="references"> <li id="cite_note-7"><span class="mw-cite-backlink noprint"><a href="#cite_ref-7">↑</a> </span><span class="reference-text">Récursivement axiomatisables et cohérentes.</span> </li> </ol></div> </div> <div class="mw-heading mw-heading3"><h3 id="Références"><span id="R.C3.A9f.C3.A9rences"></span>Références</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=29" title="Modifier la section : Références" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=29" title="Modifier le code source de la section : Références"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="references-small decimal" style=""><div class="mw-references-wrap"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink noprint"><a href="#cite_ref-1">↑</a> </span><span class="reference-text"><span class="ouvrage" id="NORVIG2014"><span class="ouvrage" id="RUSSELL_/_NORVIG2014"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> RUSSELL / <span class="nom_auteur">NORVIG</span>, <cite class="italique" lang="en">Artificial Intelligence: A Modern Approach, Global Edition</cite>, Pearson, <time class="nowrap" datetime="2014-01-01" data-sort-value="2014-01-01"><abbr class="abbr" title="premier">1<sup>er</sup></abbr> janvier 2014</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-292-15396-4" title="Spécial:Ouvrages de référence/978-1-292-15396-4"><span class="nowrap">978-1-292-15396-4</span></a>, <a rel="nofollow" class="external text" href="https://www.amazon.com/Artificial-Intelligence-Modern-Approach-Global/dp/1292153962">lire en ligne</a>)</small>, Chapitre 8 - First order logic<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Artificial+Intelligence%3A+A+Modern+Approach%2C+Global+Edition&rft.pub=Pearson&rft.aulast=NORVIG&rft.aufirst=RUSSELL+%2F&rft.date=2014-01-01&rft.pages=Chapitre+8+-+First+order+logic&rft.isbn=978-1-292-15396-4&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACalcul+des+pr%C3%A9dicats"></span></span></span></span> </li> <li id="cite_note-2"><span class="mw-cite-backlink noprint"><a href="#cite_ref-2">↑</a> </span><span class="reference-text"><span class="ouvrage">« <a rel="nofollow" class="external text" href="https://www.bibmath.net/bios/index.php?action=affiche&quoi=frege"><cite style="font-style:normal;">Biographie de Gottlob Frege</cite></a> », sur <span class="italique">www.bibmath.net</span></span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink noprint"><a href="#cite_ref-3">↑</a> </span><span class="reference-text"><span class="ouvrage" id="Kant1787"><span class="ouvrage" id="Emmanuel_Kant1787">Emmanuel Kant, « <a class="external text" href="https://fr.wikisource.org/wiki/Critique_de_la_raison_pure_(trad._Barni)/Tome_I/Pr%C3%A9face_de_la_2e_%C3%A9dition"><cite style="font-style:normal;">Préface de la Critique de la raison pure</cite></a> », sur <span class="italique">fr.wikisource.org</span>, <time>1787</time></span></span>.</span> </li> <li id="cite_note-4"><span class="mw-cite-backlink noprint"><a href="#cite_ref-4">↑</a> </span><span class="reference-text"><span class="ouvrage">« <a class="external text" href="https://fr.wiktionary.org/wiki/logicien"><cite style="font-style:normal;">logicien — Wiktionnaire</cite></a> », sur <span class="italique">fr.wiktionary.org</span> <small style="line-height:1em;">(consulté le <time class="nowrap" datetime="2020-05-25" data-sort-value="2020-05-25">25 mai 2020</time>)</small></span>.</span> </li> <li id="cite_note-5"><span class="mw-cite-backlink noprint"><a href="#cite_ref-5">↑</a> </span><span class="reference-text"><span class="ouvrage">« <a class="external text" href="https://fr.wikiversity.org/wiki/Logique_(math%C3%A9matiques)/D%C3%A9duction_naturelle"><cite style="font-style:normal;">Logique (mathématiques)/Déduction naturelle — Wikiversité</cite></a> », sur <span class="italique">fr.wikiversity.org</span> <small style="line-height:1em;">(consulté le <time class="nowrap" datetime="2020-05-25" data-sort-value="2020-05-25">25 mai 2020</time>)</small></span>.</span> </li> <li id="cite_note-6"><span class="mw-cite-backlink noprint"><a href="#cite_ref-6">↑</a> </span><span class="reference-text"><span class="ouvrage" id="2023"><cite class="italique">Logique : fondements et applications</cite>, <time class="nowrap" datetime="2023-07-23" data-sort-value="2023-07-23">23 juillet 2023</time> <small style="line-height:1em;">(<a rel="nofollow" class="external text" href="https://www.dunod.com/sciences-techniques/logique-fondements-et-applications-cours-et-exercices-corriges">lire en ligne</a>)</small>, p. 122, Définition 7.1<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Logique+%3A+fondements+et+applications&rft.date=2023-07-23&rft.pages=p.+122%2C+D%C3%A9finition+7.1&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACalcul+des+pr%C3%A9dicats"></span></span></span> </li> <li id="cite_note-8"><span class="mw-cite-backlink noprint"><a href="#cite_ref-8">↑</a> </span><span class="reference-text"><span class="ouvrage"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> <cite class="italique" lang="en">The Classical Decision Problem | Egon Börger | Springer</cite> <small style="line-height:1em;">(<a rel="nofollow" class="external text" href="https://www.springer.com/gp/book/9783540423249">lire en ligne</a>)</small>, Th. 6.02 p. 240<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=The+Classical+Decision+Problem+%7C+Egon+B%C3%B6rger+%7C+Springer&rft.pages=Th.+6.02+p.+240&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACalcul+des+pr%C3%A9dicats"></span></span></span> </li> </ol></div> </div> <div class="mw-heading mw-heading2"><h2 id="Annexes">Annexes</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=30" title="Modifier la section : Annexes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=30" title="Modifier le code source de la section : Annexes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Articles_connexes">Articles connexes</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=31" title="Modifier la section : Articles connexes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=31" title="Modifier le code source de la section : Articles connexes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">Calcul des propositions</a></li> <li><a href="/wiki/Th%C3%A9orie_des_mod%C3%A8les" title="Théorie des modèles">Théorie des modèles</a></li> <li><a href="/wiki/Skol%C3%A9misation" title="Skolémisation">Skolémisation</a></li> <li><a href="/wiki/Notation_(math%C3%A9matiques)" title="Notation (mathématiques)">Langage formel mathématique</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8me_de_Lindstr%C3%B6m" title="Théorème de Lindström">Théorème de Lindström</a></li> <li>Langage informatique <a href="/wiki/Prolog" title="Prolog">Prolog</a></li> <li><a href="/wiki/D%C3%A9duction_naturelle" title="Déduction naturelle">Déduction naturelle</a></li> <li><a href="/wiki/Signature_(logique)" title="Signature (logique)">Signature (logique)</a></li> <li><a href="/wiki/Structure_(logique_math%C3%A9matique)" title="Structure (logique mathématique)">Structure (logique mathématique)</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8me_d%27interpolation_de_Craig" title="Théorème d'interpolation de Craig">Théorème d'interpolation de Craig</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8me_de_Trakhtenbrot" title="Théorème de Trakhtenbrot">Théorème de Trakhtenbrot</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="Bibliographie">Bibliographie</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&veaction=edit&section=32" title="Modifier la section : Bibliographie" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=Calcul_des_pr%C3%A9dicats&action=edit&section=32" title="Modifier le code source de la section : Bibliographie"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li>Stephen Kleene, <i>Logique mathématique</i>, Armand Colin, 1971 ou Gabay 1987 <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/2-87647-005-5" title="Spécial:Ouvrages de référence/2-87647-005-5"><span class="nowrap">2-87647-005-5</span></a>)</small></li> <li>R. David, K. Nour et C. Raffalli, <i>Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés</i>, <a href="/wiki/%C3%89ditions_Dunod" title="Éditions Dunod">Dunod</a>, 2001 <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/2-10-006796-6" title="Spécial:Ouvrages de référence/2-10-006796-6"><span class="nowrap">2-10-006796-6</span></a>)</small></li> <li>Pierre Lebarbenchon, Sophie Pinchinat, François Schwarzentruber, Logique : fondements et applications. Dunod 2022 <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-2100821587" title="Spécial:Ouvrages de référence/978-2100821587"><span class="nowrap">978-2100821587</span></a>)</small></li></ul> <div class="navbox-container" style="clear:both;"> <table class="navbox collapsible noprint autocollapse" style=""> <tbody><tr><th class="navbox-title" colspan="2" style=""><div style="float:left; width:6em; text-align:left"><div class="noprint plainlinks nowrap tnavbar" style="padding:0; font-size:xx-small; color:var(--color-emphasized, #000000);"><a href="/wiki/Mod%C3%A8le:Palette_Logique" title="Modèle:Palette Logique"><abbr class="abbr" title="Voir ce modèle.">v</abbr></a> · <a class="external text" href="https://fr.wikipedia.org/w/index.php?title=Mod%C3%A8le:Palette_Logique&action=edit"><abbr class="abbr" title="Modifier ce modèle. Merci de prévisualiser avant de sauvegarder.">m</abbr></a></div></div><div style="font-size:110%"><a href="/wiki/Logique" title="Logique">Logique</a></div></th> </tr> <tr> <th class="navbox-group" style="">Domaines académiques</th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Th%C3%A9orie_des_ensembles" title="Théorie des ensembles">Théorie des ensembles</a></li> <li><a href="/wiki/Th%C3%A9orie_de_la_d%C3%A9monstration" title="Théorie de la démonstration">Théorie de la démonstration</a></li> <li><a href="/wiki/Th%C3%A9orie_des_mod%C3%A8les" title="Théorie des modèles">Théorie des modèles</a></li> <li><a href="/wiki/Logique_philosophique" title="Logique philosophique">Logique philosophique</a></li> <li><a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">Logique mathématique</a></li> <li><a href="/wiki/Logique_informelle" title="Logique informelle">Logique informelle</a></li> <li><a href="/wiki/Histoire_de_la_logique" title="Histoire de la logique">Histoire de la logique</a></li> <li><a href="/wiki/Philosophie_de_la_logique" title="Philosophie de la logique">Philosophie de la logique</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Concepts fondamentaux</th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Abduction_(logique)" title="Abduction (logique)">Abduction</a></li> <li><a href="/wiki/Conclusion_(logique)" title="Conclusion (logique)">Conclusion</a></li> <li><a href="/wiki/D%C3%A9duction_logique" title="Déduction logique">Déduction</a></li> <li><a href="/wiki/D%C3%A9finition" title="Définition">Définition</a></li> <li><a href="/wiki/D%C3%A9monstration_(logique_et_math%C3%A9matiques)" title="Démonstration (logique et mathématiques)">Démonstration</a></li> <li><a href="/wiki/Description" title="Description">Description</a></li> <li><a href="/wiki/Implication_(logique)" title="Implication (logique)">Implication</a></li> <li><a href="/wiki/Inf%C3%A9rence_(logique)" title="Inférence (logique)">Inférence</a></li> <li><a href="/wiki/Induction_(logique)" title="Induction (logique)">Induction</a></li> <li><a href="/wiki/Sens_(linguistique)" title="Sens (linguistique)">Sens</a></li> <li><a href="/wiki/Paradoxe" title="Paradoxe">Paradoxe</a></li> <li><a href="/wiki/Pr%C3%A9dicat_(logique_math%C3%A9matique)" title="Prédicat (logique mathématique)">Prédicat</a></li> <li><a href="/wiki/Pr%C3%A9misse" title="Prémisse">Prémisse</a></li> <li><a href="/wiki/Proposition_(philosophie)" title="Proposition (philosophie)">Proposition</a></li> <li><a href="/wiki/Mondes_possibles" title="Mondes possibles">Mondes possibles</a></li> <li><a href="/wiki/Pr%C3%A9supposition" title="Présupposition">Présupposition</a></li> <li><a href="/wiki/R%C3%A9f%C3%A9rence_(philosophie)" title="Référence (philosophie)">Référence</a></li> <li><a href="/wiki/S%C3%A9mantique_formelle_(logique)" title="Sémantique formelle (logique)">Sémantique</a></li> <li><a href="/wiki/Syntaxe_(logique)" title="Syntaxe (logique)">Syntaxe</a></li> <li><a href="/wiki/Syllogisme" title="Syllogisme">Syllogisme</a></li> <li><a href="/wiki/V%C3%A9rit%C3%A9_logique" title="Vérité logique">Vérité</a></li> <li><a href="/wiki/Valeur_de_v%C3%A9rit%C3%A9" title="Valeur de vérité">Valeur de vérité</a></li> <li><a href="/wiki/Validit%C3%A9_(logique)" title="Validité (logique)">Validité</a></li> <li><i><a href="/wiki/Cat%C3%A9gorie:Concept_logique" title="Catégorie:Concept logique">Plus</a></i></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Esprit_critique" title="Esprit critique">Esprit critique</a> et <a href="/wiki/Logique_informelle" title="Logique informelle">logique informelle</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Affirmation" title="Affirmation">Affirmation</a></li> <li><a href="/wiki/Analyse_(philosophie)" title="Analyse (philosophie)">Analyse</a></li> <li><a href="/wiki/Ambigu%C3%AFt%C3%A9" title="Ambiguïté">Ambiguïté</a></li> <li><a href="/wiki/Cr%C3%A9dibilit%C3%A9" title="Crédibilité">Crédibilité</a></li> <li><a href="/wiki/%C3%89vidence" title="Évidence">Évidence</a></li> <li><a href="/wiki/Explication" title="Explication">Explication</a></li> <li><a href="/wiki/Sophisme" title="Sophisme">Sophisme</a></li> <li><a href="/wiki/Parcimonie" title="Parcimonie">Parcimonie</a></li> <li><a href="/wiki/Propagande" title="Propagande">Propagande</a></li> <li><a href="/wiki/Rh%C3%A9torique" title="Rhétorique">Rhétorique</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">Logique mathématique</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Alg%C3%A8bre_de_Boole_(logique)" title="Algèbre de Boole (logique)">Algèbre de Boole</a></li> <li><a class="mw-selflink selflink">Calcul des prédicats</a></li> <li><a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">Calcul des propositions</a></li> <li><a href="/wiki/Th%C3%A9orie_de_la_calculabilit%C3%A9" title="Théorie de la calculabilité">Théorie de la calculabilité</a></li> <li><a href="/wiki/D%C3%A9duction_naturelle" title="Déduction naturelle">Déduction naturelle</a></li> <li><a href="/wiki/Logique_traditionnelle" title="Logique traditionnelle">Logique traditionnelle</a></li> <li><a href="/wiki/Logique_classique" title="Logique classique">Logique classique</a></li> <li><a href="/wiki/Logique_lin%C3%A9aire" title="Logique linéaire">Logique linéaire</a></li> <li><a href="/wiki/Lois_de_De_Morgan" title="Lois de De Morgan">Lois de De Morgan</a></li> <li><a href="/wiki/Th%C3%A9orie_de_la_d%C3%A9monstration" title="Théorie de la démonstration">Théorie de la démonstration</a></li> <li><a href="/wiki/Th%C3%A9orie_des_ensembles" title="Théorie des ensembles">Théorie des ensembles</a></li> <li><a href="/wiki/Th%C3%A9orie_des_mod%C3%A8les" title="Théorie des modèles">Théorie des modèles</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Logique_non_classique" title="Logique non classique">Logiques non classiques</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Logique_de_description" title="Logique de description">Logique de description</a></li> <li><a href="/wiki/Logique_intuitionniste" title="Logique intuitionniste">Logique intuitionniste</a></li> <li><a href="/wiki/Logique_minimale" title="Logique minimale">Logique minimale</a></li> <li><a href="/wiki/Logique_floue" title="Logique floue">Logique floue</a></li> <li><a href="/wiki/Logique_modale" title="Logique modale">Logique modale</a></li> <li><a href="/wiki/Logique_non_monotone" title="Logique non monotone">Logique non monotone</a></li> <li><a href="/wiki/Logique_paracoh%C3%A9rente" title="Logique paracohérente">Logique paracohérente</a></li> <li><a href="/wiki/Logiques_sous-structurelles" title="Logiques sous-structurelles">Logiques sous-structurelles</a></li> <li><a href="/wiki/Logique_de_%C5%81ukasiewicz" title="Logique de Łukasiewicz">Logique de Łukasiewicz</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/M%C3%A9talogique" title="Métalogique">Métalogique</a> et <a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">métamathématique</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Th%C3%A9or%C3%A8me_de_Cantor" title="Théorème de Cantor">Théorème de Cantor</a></li> <li><a href="/wiki/Th%C3%A8se_de_Church" title="Thèse de Church">Thèse de Church</a></li> <li><a href="/wiki/Fondements_des_math%C3%A9matiques" title="Fondements des mathématiques">Fondements des mathématiques</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del" title="Théorème de complétude de Gödel">Théorème de complétude de Gödel</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8mes_d%27incompl%C3%A9tude_de_G%C3%B6del" title="Théorèmes d'incomplétude de Gödel">Théorème d'incomplétude de Gödel</a></li> <li><a href="/wiki/Compl%C3%A9tude" class="mw-disambig" title="Complétude">Complétude</a></li> <li><a href="/wiki/D%C3%A9cidabilit%C3%A9" title="Décidabilité">Décidabilité</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8me_de_L%C3%B6wenheim-Skolem" title="Théorème de Löwenheim-Skolem">Théorème de Löwenheim-Skolem</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Philosophie_de_la_logique" title="Philosophie de la logique">Philosophie de la logique</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Atomisme_logique" title="Atomisme logique">Atomisme logique</a></li> <li><a href="/wiki/Constructivisme_(math%C3%A9matiques)" title="Constructivisme (mathématiques)">Constructivisme</a></li> <li><a href="/wiki/Logicisme" title="Logicisme">Logicisme</a></li> <li><a href="/wiki/Intuitionnisme" title="Intuitionnisme">Intuitionnisme</a></li> <li><a href="/wiki/Dialeth%C3%A9isme" title="Dialethéisme">Dialethéisme</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Logique" title="Logique">Logiciens</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Aristote" title="Aristote">Aristote</a></li> <li><a href="/wiki/Avicenne" title="Avicenne">Avicenne</a></li> <li><a href="/wiki/Averro%C3%A8s" title="Averroès">Averroès</a></li> <li><a href="/wiki/Alexander_Bain_(philosophe)" title="Alexander Bain (philosophe)">Bain</a></li> <li><a href="/wiki/Jon_Barwise" title="Jon Barwise">Barwise</a></li> <li><a href="/wiki/Paul_Bernays" title="Paul Bernays">Bernays</a></li> <li><a href="/wiki/George_Boole" title="George Boole">Boole</a></li> <li><a href="/wiki/Georg_Cantor" title="Georg Cantor">Cantor</a></li> <li><a href="/wiki/Rudolf_Carnap" title="Rudolf Carnap">Carnap</a></li> <li><a href="/wiki/Alonzo_Church" title="Alonzo Church">Church</a></li> <li><a href="/wiki/Chrysippe_de_Soles" title="Chrysippe de Soles">Chrysippe de Soles</a></li> <li><a href="/wiki/Haskell_Curry" title="Haskell Curry">Curry</a></li> <li><a href="/wiki/Auguste_De_Morgan" title="Auguste De Morgan">De Morgan</a></li> <li><a href="/wiki/Gottlob_Frege" title="Gottlob Frege">Frege</a></li> <li><a href="/wiki/Gerhard_Gentzen" title="Gerhard Gentzen">Gentzen</a></li> <li><a href="/wiki/Kurt_G%C3%B6del" title="Kurt Gödel">Gödel</a></li> <li><a href="/wiki/David_Hilbert" title="David Hilbert">Hilbert</a></li> <li><a href="/wiki/Stephen_Cole_Kleene" title="Stephen Cole Kleene">Kleene</a></li> <li><a href="/wiki/Saul_Kripke" title="Saul Kripke">Kripke</a></li> <li><a href="/wiki/Gottfried_Wilhelm_Leibniz" title="Gottfried Wilhelm Leibniz">Leibniz</a></li> <li><a href="/wiki/Leopold_L%C3%B6wenheim" title="Leopold Löwenheim">Löwenheim</a></li> <li><a href="/wiki/Guillaume_d%27Ockham" title="Guillaume d'Ockham">Guillaume d'Ockham</a></li> <li><a href="/wiki/Giuseppe_Peano" title="Giuseppe Peano">Peano</a></li> <li><a href="/wiki/Charles_Sanders_Peirce" title="Charles Sanders Peirce">Peirce</a></li> <li><a href="/wiki/Karl_Popper" title="Karl Popper">Popper</a></li> <li><a href="/wiki/Hilary_Putnam" title="Hilary Putnam">Putnam</a></li> <li><a href="/wiki/Willard_Van_Orman_Quine" title="Willard Van Orman Quine">Quine</a></li> <li><a href="/wiki/Bertrand_Russell" title="Bertrand Russell">Russell</a></li> <li><a href="/wiki/Ernst_Schr%C3%B6der" title="Ernst Schröder">Schröder</a></li> <li><a href="/wiki/Jean_Duns_Scot" title="Jean Duns Scot">Scot</a></li> <li><a href="/wiki/Thoralf_Skolem" title="Thoralf Skolem">Skolem</a></li> <li><a href="/wiki/Raymond_Smullyan" title="Raymond Smullyan">Smullyan</a></li> <li><a href="/wiki/Alfred_Tarski" title="Alfred Tarski">Tarski</a></li> <li><a href="/wiki/Alan_Turing" title="Alan Turing">Turing</a></li> <li><a href="/wiki/Alfred_North_Whitehead" title="Alfred North Whitehead">Whitehead</a></li> <li><a href="/wiki/Ludwig_Wittgenstein" title="Ludwig Wittgenstein">Wittgenstein</a></li> <li><a href="/wiki/Ernst_Zermelo" title="Ernst Zermelo">Zermelo</a></li></ul> </div></td> </tr> </tbody></table> <table class="navbox collapsible noprint autocollapse" style=""> <tbody><tr><th class="navbox-title" colspan="2" style=""><div style="float:left; width:6em; text-align:left"><div class="noprint plainlinks nowrap tnavbar" style="padding:0; font-size:xx-small; color:var(--color-emphasized, #000000);"><a href="/wiki/Mod%C3%A8le:Palette_Logique_math%C3%A9matique" title="Modèle:Palette Logique mathématique"><abbr class="abbr" title="Voir ce modèle.">v</abbr></a> · <a class="external text" href="https://fr.wikipedia.org/w/index.php?title=Mod%C3%A8le:Palette_Logique_math%C3%A9matique&action=edit"><abbr class="abbr" title="Modifier ce modèle. Merci de prévisualiser avant de sauvegarder.">m</abbr></a></div></div><div style="font-size:110%">Logique mathématique</div></th> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Calcul_des_propositions" title="Calcul des propositions">Calcul des propositions</a></th> <td class="navbox-list" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style=""><a href="/wiki/R%C3%A8gle_d%27inf%C3%A9rence" title="Règle d'inférence">Règles d'inférence</a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Modus_ponens" title="Modus ponens"><span title="A→B, A ⊢ B"><i>Modus ponens</i></span></a> / <a href="/wiki/Modus_tollens" title="Modus tollens"><span title="A→B, ¬B ⊢ ¬A"><i>Modus tollens</i></span></a></li> <li><a href="/wiki/%C3%89limination_de_la_conjonction" title="Élimination de la conjonction"><span title="A∧B ⊢ A">Élimination</span></a> / <a href="/wiki/R%C3%A8gle_d%27introduction_(logique)" title="Règle d'introduction (logique)"><span title="A, B ⊢ A∧B">introduction de la conjonction</span></a></li> <li><a href="/wiki/%C3%89limination_de_la_disjonction" title="Élimination de la disjonction"><span title="A∨B, A→C, B→C ⊢ C">Élimination</span></a> / <a href="/wiki/Introduction_de_la_disjonction" title="Introduction de la disjonction"><span title="A ⊢ A∨B">introduction de la disjonction</span></a></li> <li><a href="/wiki/Syllogisme_hypoth%C3%A9tique" title="Syllogisme hypothétique"><span title="A→B, B→C ⊢ A→C">Syllogisme hypothétique</span></a> / <a href="/wiki/Syllogisme_disjonctif" title="Syllogisme disjonctif"><span title="A∨B, ¬A ⊢ B">disjonctif</span></a></li> <li><a href="/wiki/Dilemme_constructif" title="Dilemme constructif"><span title="A→P, B→Q, A∨B ⊢ P∨Q">Dilemme constructif</span></a> / <a href="/wiki/Dilemme_destructif" title="Dilemme destructif"><span title="A→P, B→Q, ¬P∨¬Q ⊢ ¬A∨¬B">destructif</span></a></li> <li><a href="/w/index.php?title=Absorption_(logique)&action=edit&redlink=1" class="new" title="Absorption (logique) (page inexistante)"><span title="A→B ⊢ A→A∧B">Absorption</span></a></li> <li><i><a href="/wiki/Modus_ponendo_tollens" title="Modus ponendo tollens">Modus ponendo tollens</a></i></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/R%C3%A8gle_de_remplacement" title="Règle de remplacement">Règles de remplacement</a></th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Associativit%C3%A9" title="Associativité"><span title="A∨(B∨C) = (A∨B)∨C">Associativité</span></a></li> <li><a href="/wiki/Loi_commutative" title="Loi commutative">Commutativité</a></li> <li><a href="/wiki/Distributivit%C3%A9" title="Distributivité"><span title="A∧(B∨C) = (A∧B)∨(A∧C)">Distributivité</span></a></li> <li><a href="/w/index.php?title=N%C3%A9gation_(logique)&action=edit&redlink=1" class="new" title="Négation (logique) (page inexistante)"><span title="¬¬A = A">Double négation</span></a></li> <li><a href="/wiki/Lois_de_De_Morgan" title="Lois de De Morgan">Lois de De Morgan</a></li> <li><a href="/wiki/Transposition_(logique)" title="Transposition (logique)">Transposition</a></li> <li><a href="/wiki/Implication_(logique)" title="Implication (logique)"><span title="A→B ⊢ ¬A∨B">Implication</span></a></li> <li><a href="/wiki/%C3%89quivalence_logique" title="Équivalence logique">Équivalence</a></li> <li><a href="/w/index.php?title=Exportation_(logique)&action=edit&redlink=1" class="new" title="Exportation (logique) (page inexistante)"><span title="(A∧B)→C ⊢ A→(B→C)">Exportation</span></a></li> <li><a href="/wiki/Tautologie_(logique)" title="Tautologie (logique)">Tautologie</a></li> <li><a href="/w/index.php?title=Introduction_de_la_n%C3%A9gation&action=edit&redlink=1" class="new" title="Introduction de la négation (page inexistante)">Introduction de la négation</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style=""><a class="mw-selflink selflink">Calcul des prédicats</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/w/index.php?title=G%C3%A9n%C3%A9ralisation_universelle&action=edit&redlink=1" class="new" title="Généralisation universelle (page inexistante)">Généralisation</a> / <a href="/wiki/Instanciation_universelle" title="Instanciation universelle">instanciation universelle</a></li> <li><a href="/w/index.php?title=G%C3%A9n%C3%A9ralisation_existentielle&action=edit&redlink=1" class="new" title="Généralisation existentielle (page inexistante)">Généralisation</a> / <a href="/w/index.php?title=Instanciation_existentielle&action=edit&redlink=1" class="new" title="Instanciation existentielle (page inexistante)">instanciation existentielle</a></li></ul> </div></td> </tr> </tbody></table> <table class="navbox collapsible noprint autocollapse" style=""> <tbody><tr><th class="navbox-title" colspan="2" style=""><div style="float:left; width:6em; text-align:left"><div class="noprint plainlinks nowrap tnavbar" style="padding:0; font-size:xx-small; color:var(--color-emphasized, #000000);"><a href="/wiki/Mod%C3%A8le:Palette_Informatique_th%C3%A9orique" title="Modèle:Palette Informatique théorique"><abbr class="abbr" title="Voir ce modèle.">v</abbr></a> · <a class="external text" href="https://fr.wikipedia.org/w/index.php?title=Mod%C3%A8le:Palette_Informatique_th%C3%A9orique&action=edit"><abbr class="abbr" title="Modifier ce modèle. Merci de prévisualiser avant de sauvegarder.">m</abbr></a></div></div><div style="font-size:110%"><a href="/wiki/Informatique_th%C3%A9orique" title="Informatique théorique">Informatique théorique</a></div></th> </tr> <tr> <th class="navbox-group" style="">Codage</th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Codage_de_l%27information" title="Codage de l'information">Codage de l'information</a></li> <li><a href="/wiki/Compression_de_donn%C3%A9es" title="Compression de données">Compression de données</a></li> <li><a href="/wiki/Chiffrement" title="Chiffrement">Chiffrement</a></li> <li><a href="/wiki/Cryptanalyse" title="Cryptanalyse">Cryptanalyse</a></li> <li><a href="/wiki/Cryptographie" title="Cryptographie">Cryptographie</a></li> <li><a href="/wiki/Th%C3%A9orie_de_l%27information" title="Théorie de l'information">Théorie de l'information</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Modèles de calcul</th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Th%C3%A9orie_de_la_calculabilit%C3%A9" title="Théorie de la calculabilité">Calculabilité</a></li> <li><a href="/wiki/D%C3%A9cidabilit%C3%A9" title="Décidabilité">Décidabilité et indécidabilité</a></li> <li><a href="/wiki/Ensemble_r%C3%A9cursif" title="Ensemble récursif">Ensemble récursif</a></li> <li><a href="/wiki/Probl%C3%A8me_de_l%27arr%C3%AAt" title="Problème de l'arrêt">Problème de l'arrêt</a></li> <li><a href="/wiki/R%C3%A9cursivement_%C3%A9num%C3%A9rable" title="Récursivement énumérable">Ensemble récursivement énumérable</a></li> <li><a href="/wiki/Machine_de_Turing" title="Machine de Turing">Machine de Turing</a></li> <li><a href="/wiki/Th%C3%A8se_de_Church" title="Thèse de Church">Thèse de Church</a></li> <li><a href="/wiki/Automate_cellulaire" title="Automate cellulaire">Automate cellulaire</a></li> <li><a href="/wiki/R%C3%A9seau_de_neurones_artificiels" title="Réseau de neurones artificiels">Réseau de neurones artificiels</a></li> <li><a href="/wiki/R%C3%A9duction_polynomiale" title="Réduction polynomiale">Réduction polynomiale</a></li> <li><a href="/wiki/Cat%C3%A9gorie:Probl%C3%A8me_NP-complet" title="Catégorie:Problème NP-complet">Problème NP-complet</a></li> <li><a href="/wiki/Principe_de_Church-Turing-Deutsch" title="Principe de Church-Turing-Deutsch">Principe de Church-Turing-Deutsch</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Algorithmique" title="Algorithmique">Algorithmique</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Algorithmique" title="Algorithmique">Algorithmique</a></li> <li><a href="/wiki/Algorithme_glouton" title="Algorithme glouton">Algorithme glouton</a></li> <li><a href="/wiki/Algorithme_probabiliste" title="Algorithme probabiliste">Algorithme probabiliste</a></li> <li><a href="/wiki/Algorithme_g%C3%A9n%C3%A9tique" title="Algorithme génétique">Algorithme génétique</a></li> <li><a href="/wiki/Th%C3%A9orie_de_la_complexit%C3%A9_(informatique_th%C3%A9orique)" title="Théorie de la complexité (informatique théorique)">Complexité algorithmique</a></li> <li><a href="/wiki/Analyse_de_la_complexit%C3%A9_des_algorithmes" title="Analyse de la complexité des algorithmes">Analyse d'algorithme</a></li> <li><a href="/wiki/Diviser_pour_r%C3%A9gner_(informatique)" title="Diviser pour régner (informatique)">Diviser pour régner</a></li> <li><a href="/wiki/Heuristique_(math%C3%A9matiques)" title="Heuristique (mathématiques)">Heuristique</a></li> <li><a href="/wiki/Programmation_dynamique" title="Programmation dynamique">Programmation dynamique</a></li> <li><a href="/wiki/G%C3%A9om%C3%A9trie_algorithmique" title="Géométrie algorithmique">Géométrie algorithmique</a></li> <li><a href="/wiki/Algorithme_de_tri" title="Algorithme de tri">Algorithmes de tri</a></li> <li><a href="/wiki/Algorithmique_du_texte" title="Algorithmique du texte">Algorithmique du texte</a></li> <li><a href="/wiki/Exploration_de_donn%C3%A9es" title="Exploration de données">Exploration de données</a></li> <li><a href="/wiki/Science_des_donn%C3%A9es" title="Science des données">Science des données</a></li> <li><a href="/wiki/Apprentissage_profond" title="Apprentissage profond">Apprentissage profond</a></li> <li><a href="/wiki/Test_de_primalit%C3%A9" title="Test de primalité">Test de primalité</a></li> <li><a href="/wiki/Structure_de_donn%C3%A9es" title="Structure de données">Structure de données</a></li> <li><a href="/wiki/Arbre_enracin%C3%A9" title="Arbre enraciné">Arbre enraciné</a></li> <li><a href="/wiki/Programmation_concurrente" title="Programmation concurrente">Concurrence</a></li> <li><a href="/wiki/Parall%C3%A9lisme_(informatique)" title="Parallélisme (informatique)">Parallélisme</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Syntaxe</th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/R%C3%A9%C3%A9criture_(informatique)" title="Réécriture (informatique)">Réécriture</a></li> <li><a href="/wiki/Compilateur" title="Compilateur">Compilation</a></li> <li><a href="/wiki/Expression_r%C3%A9guli%C3%A8re" title="Expression régulière">Expression régulière</a></li> <li><a href="/wiki/Grammaire_formelle" title="Grammaire formelle">Grammaire formelle</a></li> <li><a href="/wiki/Langage_rationnel" title="Langage rationnel">Langage rationnel</a></li> <li><a href="/wiki/Ensemble_rationnel" title="Ensemble rationnel">Ensemble rationnel</a></li> <li><a href="/wiki/Langage_formel" title="Langage formel">Théorie des langages</a></li> <li><a href="/wiki/Th%C3%A9orie_des_automates" title="Théorie des automates">Théorie des automates</a></li> <li><a href="/wiki/Automate_fini" title="Automate fini">Automate fini</a></li> <li><a href="/wiki/Automate_sur_les_mots_infinis" title="Automate sur les mots infinis">Automate sur les mots infinis</a></li> <li><a href="/wiki/Automate_d%27arbres" title="Automate d'arbres">Automate d'arbres</a></li> <li><a href="/wiki/Automate_%C3%A0_pile" title="Automate à pile">Automate à pile</a></li> <li><a href="/wiki/Hi%C3%A9rarchie_de_Chomsky" title="Hiérarchie de Chomsky">Hiérarchie de Chomsky</a></li> <li><a href="/wiki/Linguistique_informatique" title="Linguistique informatique">Linguistique informatique</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Sémantique</th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Interpr%C3%A9tation_abstraite" title="Interprétation abstraite">Interprétation abstraite</a></li> <li><a href="/wiki/M%C3%A9thode_formelle_(informatique)" title="Méthode formelle (informatique)">Méthodes formelles</a></li> <li><a href="/wiki/V%C3%A9rification_de_mod%C3%A8les" title="Vérification de modèles">Vérification de modèles</a></li> <li><a href="/wiki/S%C3%A9mantique_des_langages_de_programmation" title="Sémantique des langages de programmation">Sémantique des langages de programmation</a></li> <li><a href="/wiki/S%C3%A9mantique_d%C3%A9notationnelle" title="Sémantique dénotationnelle">Sémantique dénotationnelle</a></li> <li><a href="/wiki/S%C3%A9mantique_axiomatique" title="Sémantique axiomatique">Sémantique axiomatique</a></li> <li><a href="/wiki/S%C3%A9mantique_op%C3%A9rationnelle" title="Sémantique opérationnelle">Sémantique opérationnelle</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Logique_math%C3%A9matique" title="Logique mathématique">Logique mathématique</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Assistant_de_preuve" title="Assistant de preuve">Assistant de preuve</a></li> <li><a class="mw-selflink selflink">Calcul des prédicats</a></li> <li><a href="/wiki/Correspondance_de_Curry-Howard" title="Correspondance de Curry-Howard">Correspondance de Curry-Howard</a></li> <li><a href="/wiki/Fonction_r%C3%A9cursive" title="Fonction récursive">Fonction récursive</a></li> <li><a href="/wiki/Lambda-calcul" title="Lambda-calcul">Lambda-calcul</a></li> <li><a href="/wiki/Th%C3%A9or%C3%A8mes_d%27incompl%C3%A9tude_de_G%C3%B6del" title="Théorèmes d'incomplétude de Gödel">Théorèmes d'incomplétude de Gödel</a></li> <li><a href="/wiki/Th%C3%A9orie_des_types" title="Théorie des types">Théorie des types</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Math%C3%A9matiques_discr%C3%A8tes" title="Mathématiques discrètes">Mathématiques discrètes</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Combinatoire" title="Combinatoire">Combinatoire</a></li> <li><a href="/wiki/Algorithme_du_simplexe" title="Algorithme du simplexe">Algorithme du simplexe</a></li> <li><a href="/wiki/Optimisation_combinatoire" title="Optimisation combinatoire">Optimisation combinatoire</a></li> <li><a href="/wiki/Th%C3%A9orie_des_graphes" title="Théorie des graphes">Théorie des graphes</a></li> <li><a href="/wiki/Liste_des_algorithmes_de_la_th%C3%A9orie_des_graphes" title="Liste des algorithmes de la théorie des graphes">Algorithmes de la théorie des graphes</a></li> <li><a href="/wiki/Recherche_op%C3%A9rationnelle" title="Recherche opérationnelle">Recherche opérationnelle</a></li> <li><a href="/wiki/Th%C3%A9orie_de_la_d%C3%A9cision" title="Théorie de la décision">Théorie de la décision</a></li> <li><a href="/wiki/Analyse_num%C3%A9rique" title="Analyse numérique">Analyse numérique</a></li></ul> </div></td> </tr> </tbody></table> </div> <ul id="bandeau-portail" class="bandeau-portail"><li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer skin-invert-image" typeof="mw:File"><a href="/wiki/Portail:Logique" title="Portail de la logique"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/e/e7/Logic.svg/48px-Logic.svg.png" decoding="async" width="48" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/e/e7/Logic.svg/72px-Logic.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/e/e7/Logic.svg/96px-Logic.svg.png 2x" data-file-width="85" data-file-height="28" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:Logique" title="Portail:Logique">Portail de la logique</a></span> </span></li> <li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer skin-invert-image" typeof="mw:File"><a href="/wiki/Portail:Informatique_th%C3%A9orique" title="Portail de l'informatique théorique"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/30px-Max-cut.svg.png" decoding="async" width="30" height="24" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/45px-Max-cut.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/60px-Max-cut.svg.png 2x" data-file-width="200" data-file-height="160" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:Informatique_th%C3%A9orique" title="Portail:Informatique théorique">Portail de l'informatique théorique</a></span> </span></li> </ul>    </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="">Ce document provient de « <a dir="ltr" href="https://fr.wikipedia.org/w/index.php?title=Calcul_des_prédicats&oldid=218203062">https://fr.wikipedia.org/w/index.php?title=Calcul_des_prédicats&oldid=218203062</a> ».</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Cat%C3%A9gorie:Accueil" title="Catégorie:Accueil">Catégories</a> : <ul><li><a href="/wiki/Cat%C3%A9gorie:Logique" title="Catégorie:Logique">Logique</a></li><li><a href="/wiki/Cat%C3%A9gorie:Logique_math%C3%A9matique" title="Catégorie:Logique mathématique">Logique mathématique</a></li><li><a href="/wiki/Cat%C3%A9gorie:Mod%C3%A8le_conceptuel" title="Catégorie:Modèle conceptuel">Modèle conceptuel</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Catégories cachées : <ul><li><a href="/wiki/Cat%C3%A9gorie:Article_%C3%A0_r%C3%A9f%C3%A9rence_n%C3%A9cessaire" title="Catégorie:Article à référence nécessaire">Article à référence nécessaire</a></li><li><a href="/wiki/Cat%C3%A9gorie:Article_%C3%A0_r%C3%A9f%C3%A9rence_souhait%C3%A9e" title="Catégorie:Article à référence souhaitée">Article à référence souhaitée</a></li><li><a href="/wiki/Cat%C3%A9gorie:Article_avec_une_section_vide_ou_incompl%C3%A8te" title="Catégorie:Article avec une section vide ou incomplète">Article avec une section vide ou incomplète</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Logique/Articles_li%C3%A9s" title="Catégorie:Portail:Logique/Articles liés">Portail:Logique/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Projet:Math%C3%A9matiques/Articles" title="Catégorie:Projet:Mathématiques/Articles">Projet:Mathématiques/Articles</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Sciences/Articles_li%C3%A9s" title="Catégorie:Portail:Sciences/Articles liés">Portail:Sciences/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Informatique_th%C3%A9orique/Articles_li%C3%A9s" title="Catégorie:Portail:Informatique théorique/Articles liés">Portail:Informatique théorique/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Informatique/Articles_li%C3%A9s" title="Catégorie:Portail:Informatique/Articles liés">Portail:Informatique/Articles liés</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"> La dernière modification de cette page a été faite le 31 août 2024 à 00:11.</li> <li id="footer-info-copyright"><span style="white-space: normal"><a href="/wiki/Wikip%C3%A9dia:Citation_et_r%C3%A9utilisation_du_contenu_de_Wikip%C3%A9dia" title="Wikipédia:Citation et réutilisation du contenu de Wikipédia">Droit d'auteur</a> : les textes sont disponibles sous <a rel="nofollow" class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.fr">licence Creative Commons attribution, partage dans les mêmes conditions</a> ; d’autres conditions peuvent s’appliquer. Voyez les <a class="external text" href="https://foundation.wikimedia.org/wiki/Policy:Terms_of_Use/fr">conditions d’utilisation</a> pour plus de détails, ainsi que les <a href="/wiki/Wikip%C3%A9dia:Cr%C3%A9dits_graphiques" title="Wikipédia:Crédits graphiques">crédits graphiques</a>. En cas de réutilisation des textes de cette page, voyez <a href="/wiki/Sp%C3%A9cial:Citer/Calcul_des_pr%C3%A9dicats" title="Spécial:Citer/Calcul des prédicats">comment citer les auteurs et mentionner la licence</a>.<br /> Wikipedia® est une marque déposée de la <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, organisation de bienfaisance régie par le paragraphe <a href="/wiki/501c" title="501c">501(c)(3)</a> du code fiscal des États-Unis.</span><br /></li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy/fr">Politique de confidentialité</a></li> <li id="footer-places-about"><a href="/wiki/Wikip%C3%A9dia:%C3%80_propos_de_Wikip%C3%A9dia">À propos de Wikipédia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikip%C3%A9dia:Avertissements_g%C3%A9n%C3%A9raux">Avertissements</a></li> <li id="footer-places-contact"><a href="//fr.wikipedia.org/wiki/Wikipédia:Contact">Contact</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code de conduite</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Développeurs</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/fr.wikipedia.org">Statistiques</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Déclaration sur les témoins (cookies)</a></li> <li id="footer-places-mobileview"><a href="//fr.m.wikipedia.org/w/index.php?title=Calcul_des_pr%C3%A9dicats&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Version mobile</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-2fxxf","wgBackendResponseTime":166,"wgPageParseReport":{"limitreport":{"cputime":"0.299","walltime":"0.533","ppvisitednodes":{"value":3802,"limit":1000000},"postexpandincludesize":{"value":132809,"limit":2097152},"templateargumentsize":{"value":32821,"limit":2097152},"expansiondepth":{"value":14,"limit":100},"expensivefunctioncount":{"value":0,"limit":500},"unstrip-depth":{"value":0,"limit":20},"unstrip-size":{"value":10190,"limit":5000000},"entityaccesscount":{"value":1,"limit":400},"timingprofile":["100.00% 270.857 1 -total"," 31.25% 84.655 1 Modèle:Portail"," 21.20% 57.430 1 Modèle:Catégorisation_badges"," 16.21% 43.893 2 Modèle:Références"," 11.96% 32.395 1 Modèle:Palette"," 10.83% 29.325 7 Modèle:Référence_nécessaire"," 9.68% 26.226 3 Modèle:Ouvrage"," 8.21% 22.239 5 Modèle:Article_détaillé"," 7.89% 21.376 6 Modèle:Méta_bandeau_de_section"," 7.02% 19.011 3 Modèle:Méta_palette_de_navigation"]},"scribunto":{"limitreport-timeusage":{"value":"0.066","limit":"10.000"},"limitreport-memusage":{"value":3875638,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-f69cdc8f6-9dtxv","timestamp":"20241125024334","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Calcul des pr\u00e9dicats","url":"https:\/\/fr.wikipedia.org\/wiki\/Calcul_des_pr%C3%A9dicats","sameAs":"http:\/\/www.wikidata.org\/entity\/Q4055684","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q4055684","author":{"@type":"Organization","name":"Contributeurs aux projets Wikimedia"},"publisher":{"@type":"Organization","name":"Fondation Wikimedia, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2004-08-19T13:47:57Z","dateModified":"2024-08-30T23:11:32Z","headline":"m\u00e9thode formelle, utilise des variables sur des objets non logiques et permet l'usage de phrases qui contiennent des variables; seules les variables sont quantifi\u00e9es"}</script> </body> </html>