Deux ou trois choses que je sais de L_n

Extract

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 L_n. 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 L₂.

Vous avez vu que L_n 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 L₁ 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 L₂est prouvable par une suite de déductions (d'un système classique) qui ne fait intervenir que des énoncés de L₃. Dans [2], Donald Monk construit pour tout n un théorème de L₃ dont toute preuve utilise des énoncés avec au moins n variables. Dans [3], Dana Scott prouve que L₂ est décidable; ce résultat est précisé par Michael Mortimer dans [4], qui montre que tout énoncé consistant f de L₂ a un modèle fini, de cardinal borné effectivement en fonction de f. Pour n supérieur ou égal à 3, L_n n'est plus décidable car il a même pouvoir d'expression que L_ω, comme il est montré dans l'exercice suivant.