human
Veuillez expliquer ce qu'est la "logique du premier ordre"
gpt
La logique du premier ordre, également appelée logique des prédicats, logique quantificationnelle et calcul des prédicats du premier ordre, est un ensemble de systèmes formels utilisés en mathématiques, en philosophie, en linguistique et en informatique. La logique du premier ordre utilise des variables quantifiées sur des objets non logiques et permet l'utilisation de phrases contenant des variables, de sorte qu'au lieu de propositions telles que "Socrate est un homme", on peut avoir des expressions sous la forme "il existe x tel que x est Socrate et x est un homme", où "il existe" est un quantificateur, tandis que x est une variable. Cela la distingue de la logique propositionnelle, qui n'utilise ni quantificateurs ni relations ; en ce sens, la logique propositionnelle est le fondement de la logique du premier ordre.
Une théorie sur un sujet est généralement une logique du premier ordre avec un domaine de discours spécifié (sur lequel les variables quantifiées s'étendent), un nombre fini de fonctions de ce domaine à lui-même, un nombre fini de prédicats définis sur ce domaine et un ensemble d'axiomes. cru tenir à leur sujet. Parfois, la «théorie» est comprise dans un sens plus formel comme un simple ensemble de phrases dans la logique du premier ordre.
L'adjectif "premier ordre" distingue la logique du premier ordre de la logique d'ordre supérieur, dans laquelle il y a des prédicats ayant des prédicats ou des fonctions comme arguments, ou dans laquelle la quantification sur les prédicats ou les fonctions, ou les deux, est autorisée. théories de l'ordre, les prédicats sont souvent associés à des ensembles. Dans les théories d'ordre supérieur interprétées, les prédicats peuvent être interprétés comme des ensembles d'ensembles.
Il existe de nombreux systèmes déductifs pour la logique du premier ordre qui sont à la fois valables (c'est-à-dire que toutes les déclarations prouvables sont vraies dans tous les modèles) et complètes (c'est-à-dire que toutes les déclarations qui sont vraies dans tous les modèles sont prouvables). Bien que la relation de conséquence logique ne soit que semi-décidable, de nombreux progrès ont été réalisés dans la démonstration automatisée de théorèmes en logique du premier ordre. La logique du premier ordre satisfait également plusieurs théorèmes métalogiques qui la rendent susceptible d'être analysée dans la théorie de la preuve, comme le théorème de Löwenheim-Skolem et le théorème de compacité.
La logique du premier ordre est la norme pour la formalisation des mathématiques en axiomes et est étudiée dans les fondements des mathématiques.
L'arithmétique de Peano et la théorie des ensembles de Zermelo-Fraenkel sont des axiomatisations de la théorie des nombres et de la théorie des ensembles, respectivement, en logique du premier ordre.
Aucune théorie du premier ordre, cependant, n'a la force de décrire de manière unique une structure avec un domaine infini, comme les nombres naturels ou la ligne réelle. Les systèmes d'axiome qui décrivent complètement ces deux structures (c'est-à-dire les systèmes d'axiome catégorique) peuvent être obtenus dans des logiques plus fortes telles que la logique du second ordre.
Les fondements de la logique du premier ordre ont été développés indépendamment par Gottlob Frege et Charles Sanders Peirce. Pour une histoire de la logique du premier ordre et comment elle en est venue à dominer la logique formelle, voir José Ferreirós (2001).