On gén´´eralise un théorème de Hilbert et Bernays relatif aux k-transformées d'une formule du calcul des prédicats.

On étudie certaines propriétés d'une hiérarchie de sytèmes formels, NFo, NF1,..., NFn,..., NF(t), le premier étant le système NF de Quine et les autres systèmes inconsistants, mais apparemment non trviaux.