Logique du premier ordre
La logique du premier ordre (également appelée logique des prédicats 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 s contenant des variables. Ainsi, au lieu de propositions telles que Socrates est un homme, on peut avoir des expressions sous la forme "il existe x tel que x Socrate et x est un homme » et il existe un quantificateur wh ile x est une variable. Cela la distingue de la logique propositionnelle, qui n'utilise pas de quantificateurs ni de relations ; En ce sens, la logique propositionnelle est le fondement de la logique du premier ordre.
Une théorie sur une image est généralement une logique de premier ordre avec un domaine de discours spécifié sur lequel les variables quantifiées se situent, un nombre infini de fonctions allant de ce domaine à lui-même, un grand nombre de prédicats définis sur ce domaine et un ensemble d'axiomes dits tenir pour ces choses. Parfois, la "théorie" est comprise dans un sens plus formel, qui n’est qu’un 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 existe des prédicats ayant des prédicats ou des fonctions en tant qu'arguments, ou dans lesquels un ou les deux des quantificateurs de prédicats ou de quantificateurs de fonctions sont autorisés. Dans les théories de premier ordre, les prédicats sont souvent associés à des ensembles. Dans les théories interprétées d'ordre supérieur, les prédicats peuvent être interprétés comme des ensembles d'ensembles.
Il existe de nombreux systèmes déductifs pour la logique de premier ordre qui sont à la fois sains (toutes les déclarations prouvables sont vraies dans tous les modèles) et complètes (toutes les déclarations qui sont vraies dans tous les modèles sont prouvables). Bien t - il conséquence logique relation est seulement semidecidable, beaucoup de progrès ont été ma de dans le théorème automatisé prouver dans la logique du premier ordre. Le journal de premier ordre répond également à plusieurs métalogiques théorèmes qui le rendent favorable à l’analyse en théorie de la preuve, comme th e théorème Löwenheim-Skolem et le théorème de compacité.
La logique du premier ordre est la norme pour formaliser les 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 respectivement une axiomatisation de la théorie des nombres et de la théorie des ensembles dans la logique du premier ordre. Cependant, aucune théorie de premier ordre n'a la force de décrire de manière unique une structure de domaine infini, telle que les nombres naturels ou la ligne réelle. Les systèmes axiomes qui décrivent complètement ces deux structures (c'est-à-dire les systèmes axiomes catégoriques) peuvent être obtenus dans une logique plus forte telle 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 de premier ordre et de la manière dont elle est parvenue à dominer la logique formelle, voir José Ferreirós (2001).
