Logique d'ordre supérieur
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

Les logiques d'ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d'utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats.

D'un point (Graphie) de vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) sémantique, cela revient à dire que l'on considère les fonctions et prédicats comme des objets à part entière, au même titre que, par exemple, un nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) entier. On s'autorisera ainsi, d'une part, à quantifier les prédicats et fonctions et, d'autre part, à donner des fonctions ou des prédicats en arguments d'autres fonctions et prédicats. Néanmoins, on pourra se doter d'un système de typage qui restreindra le genre d'objet (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et qui peut être désigné par une étiquette verbale. Il...) qui pourra être donné en tant que tel ou tel argument de tel ou tel prédicat (Les prédicats d’une théorie sont les formules qui contiennent des variables libres.) ou telle ou telle fonction.

Un prédicat d'ordre supérieur est un prédicat qui prend comme argument un ou plusieurs autres prédicats. De manière générale, un prédicat d'ordre n prend comme argument un ou plusieurs prédicats d'ordre n-1, avec n > 1. La même chose est valable pour les fonctions d'ordre supérieur.

Les lambda-calculs typés, comme le calcul des constructions, s'inspirent de telles logiques dans ce qu'on appelle le paradigme fonctionnel. Un lien fort est tissé entre les mathématiques (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels...) et l'informatique (L´informatique - contraction d´information et automatique - est le domaine d'activité scientifique, technique et industriel en rapport avec le traitement...) grâce à l'isomorphisme de Curry-Howard qui associe un lambda-calcul (Le lambda-calcul (ou λ-calcul) est un langage de programmation théorique inventé par Alonzo Church dans les années 1930. Ce langage a été le premier utilisé pour définir et caractériser les fonctions récursives et il a eu une...) à une logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans une première approche...). C'est de ce domaine que sont issus les langages de programmation fonctionnelle (Un langage fonctionnel est un langage de programmation dont la syntaxe et les caractéristiques encouragent la programmation fonctionnelle. Le langage fonctionnel le plus ancien est le Lisp,...).

Logique du second ordre

La logique du second ordre étend celle du premier ordre par l'ajout de variables fonctionnelles, qui peuvent donc être quantifiées. Par exemple, \forall P\exists x/ P(x).

La logique monadique du second ordre se restreint aux variables fonctionnelles unaires, qui sont en fait les ensembles. Elle permet d'avoir des résultats de décidabilité plus intéressants qu'au premier ordre : par exemple, la théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur l’observation ou...) monadique d'un ordinal dénombrable est décidable (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.).

Logique du troisième ordre

Elle utilise des objets de troisième type, comme les filtres ou ultrafiltres, mais est rarement mentionnée en tant que telle.

Page générée en 0.048 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique