É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 […]
