Logique (mathématiques)/Logiques d'ordre supérieur
Une logique est au premier ordre lorsque les quantificateurs portent seulement sur les variables d’objet. Les symboles des prédicats et des opérateurs fondamentaux sont considérés comme des constantes. Si on introduit des variables de prédicat ou d’opérateur et si on quantifie sur ces variables, on obtient une logique du deuxième ordre.
Les prédicats et les opérateurs peuvent eux-mêmes être considérés comme des objets. On peut alors introduire des prédicats de type 2, les précédents étant de type 1. On obtient une formule atomique en appliquant un prédicat unaire de type 2 à un prédicat de type 1, par exemple. Il faut distinguer les types des prédicats si l’on veut conserver les règles de grammaire qui postulent qu’un prédicat ne peut pas être appliqué à lui-même. Mais cette règle n’est pas nécessaire.
On peut aussi introduire des prédicats de type supérieur à deux. On obtient alors une hiérarchie de prédicats semblable à la hiérarchie des ensembles dans la théorie des types de Whitehead et Russell.
On peut aussi introduire divers types d’opérateurs, des opérateurs de type 2a qui portent sur les opérateurs de type 1, des opérateurs de type 2b qui portent sur les prédicats de type 1… Rien n’interdit d’imaginer tout ce qu’on veut.
Dès qu’on quantifie sur tous ces nouveaux êtres on obtient des logiques d’ordre supérieur. Ces logiques sont des théories des ensembles et des fonctions, parce que les prédicats peuvent être identifiés à des ensembles et les opérateurs à des fonctions. Elles conduisent aux mêmes difficultés que les autres formulations des théories des ensembles.
La logique du premier ordre peut être utilisée pour développer des théories des ensembles. Cela permet de séparer nettement les principes purement logiques, ceux du calcul des prédicats au premier ordre, et les principes ensemblistes. Les propriétés particulières aux ensembles et aux fonctions sont énoncées dans des axiomes. Toutes les déductions sont faites en prenant ces axiomes comme prémisses mais sans faire usage des logiques d’ordre supérieur. Même pour les théories des ensembles, la logique du premier ordre est suffisante pour formaliser toutes les preuves.
