Complétude (logique)En logique mathématique et métalogique, un système formel est dit complet par rapport à une propriété particulière si chaque formule possédant cette propriété peut être prouvée par une démonstration formelle à l'aide de ce système, c'est-à-dire par l'un de ses théorèmes ; autrement, le système est dit incomplet. Le terme « complet » est également utilisé sans qualification, avec des significations différentes selon le contexte, la plupart du temps se référant à la propriété de la validité sémantique.
Calcul des prédicatsEn logique mathématique, le calcul des prédicats du premier ordre, ou calcul des relations, logique quantificationnelle, ou tout simplement calcul des prédicats, est un système formel utilisé pour raisonner et décrire des énoncés en mathématiques, informatique, intelligence artificielle, philosophie et linguistique. Il a été proposé par Gottlob Frege une formalisation du langage des mathématiques entre la fin du et le début du .
Second-order logicIn logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).
Logique d'ordre supérieurLes logiques d'ordre supérieur (en anglais, higher-order logic ou HOL) sont des logiques formelles permettant d'utiliser des variables qui réfèrent à des fonctions ou à des prédicats. Elles étendent le calcul des prédicats. Cela revient à dire que l'on considère les fonctions et prédicats comme des objets de base à part entière, au même titre que, par exemple, un nombre entier. On s'autorisera ainsi, d'une part, à quantifier les prédicats et les fonctions et, d'autre part, à donner des fonctions ou des prédicats en arguments à d'autres fonctions ou prédicats.
Théorème de complétude de GödelEn logique mathématique, le théorème de complétude du calcul des prédicats du premier ordre dresse une correspondance entre la sémantique et les démonstrations d'un système de déduction en logique du premier ordre. En termes intuitifs le théorème de complétude construit un pont entre vérité et démontrabilité formelle : tout énoncé vrai est démontrable.
