MÉTALOGIQUE

Étude des propriétés des systèmes logiques. Une fois construit comme système, un formalisme peut lui-même devenir objet d'étude. Les propriétés les plus importantes des systèmes formels sont les suivantes : tout d'abord, dans l'ensemble des formules constructibles dans un système, il en est qui ne sont pas démontrables et le système est dit cohérent ; au cas où ce système comporte l'opérateur de négation, il est dit non contradictoire. Ensuite, un système est dit décidable ou résoluble s'il existe un procédé effectif (c'est-à-dire réalisable en un nombre fini d'étapes) par lequel on peut déterminer, « décider », pour toute formule du système si elle est ou non démontrable. Enfin, un système est dit saturé syntaxiquement s'il devient contradictoire lorsqu'on ajoute à ses axiomes une formule non démontrable dans le système ; il est dit saturé sémantiquement (lorsqu'on envisage le système eu égard à ses interprétations) s'il permet de démontrer toutes les formules correspondant aux théorèmes du modèle envisagé.

La logique des propositions est saturée du point de vue syntaxique et sémantique ; elle est décidable et non contradictoire. La logique des prédicats du premier ordre est non contradictoire, décidable pour les prédicats absolus et certaines classes d'expressions de la logique des relations. En ce qui concerne la logique des prédicats d'ordre supérieur, les tentatives pour montrer leur caractère non contradictoire (ou celui d'un système assez puissant pour formaliser les mathématiques) ont échoué. Gödel a démontré, en 1931, la nécessité de cet échec ; ses deux théorèmes peuvent être ainsi transcrits dans la langue ordinaire :

Si un système non contradictoire est assez puissant pour formaliser l'arithmétique récursive, il contient nécessairement des énoncés indécidables, c'est-à-dire dont on ne peut pas dire s'ils sont ou non démontrables dans le formalisme du système en question.

Si un système est assez puissant pour formaliser l'arithmétique, il est impossible de démontrer sa non-contradiction avec les seules ressources de ce système : il faut recourir à des procédés extérieurs de démonstration. Dans son ouvrage, Les Limitations internes des formalismes (1957), Jean Ladrière montre qu'il ne s'agit pas d'un échec du formalisme, mais de la limitation de son champ d'application.

— Françoise ARMENGAUD