Si vous ne gardez du calcul des prédicats classique (que j'appellerai Lω) que les formules qui ne font intervenir, tant en occurences libres que liées, que les n premières variables, vous obtenez le langage Ln. Avant de poursuivre, et de façon un peu cavalière, je vous invite à résoudre l'exercice suivant:

Exercice 1. Dans le langage comprenant seulement un symbole de relation binaire, caractériser à isomorphisme près la chaîne à n éléments au moyen d'un seul énoncé de L2.

Vous avez vu que Ln a plus de possibilités d'expression que vous ne l'aviez d'abord pensé, qu'il est ennemi de la forme prénexe, que sa force au contraire réside dans l'utilisation d'une même variable en différentes places d'une formule.

Ces langages ont été étudiés par Léon Henkin dans [1]; il y remarque que L1 est très pauvre: c'est le “calcul des classes”, on y peut seulement exprimer que des combinaisons booléennes de formules atomiques sont vides ou non, et nous n'en parlerons plus; il montre ensuite que tout théorème de L2est prouvable par une suite de déductions (d'un système classique) qui ne fait intervenir que des énoncés de L3. Dans [2], Donald Monk construit pour tout n un théorème de L3 dont toute preuve utilise des énoncés avec au moins n variables. Dans [3], Dana Scott prouve que L2 est décidable; ce résultat est précisé par Michael Mortimer dans [4], qui montre que tout énoncé consistant f de L2 a un modèle fini, de cardinal borné effectivement en fonction de f. Pour n supérieur ou égal à 3, Ln n'est plus décidable car il a même pouvoir d'expression que Lω, comme il est montré dans l'exercice suivant.