JAN ARRETE
(1) On a au rer stade : À 00.. 0, I, 2...n ; au 2° : À 10..0, n + 1... 2n À A o1o..0, 2n + 1.. 3n A...
THÉORÈME D’'HERBRAND 135 or, on démontre (1) que :
ÎL = RER Li Nr NA AT. Xiy XN-ntre. XN) Xot tN FRS D Il rat AU Ve Z1-..2n
Pa. Vp Pe.2,
La proposition initiale serait donc contradictoire contrairement à l'hypothèse.
Le raisonnement perd toute signification dans le cas d’un formalisme véritable. Mais les opérations successives de satisfaction dans un champ sont rigoureusement finies : on peut les considérer comme un traitement formel applicable à toute proposition non contradictoire. D'où l’idée d'HER- BRAND d'en faire un critère de non contradiction en démontrant la réciproque — évidente pour le système intuitif de L&ŒWENHEIM —: si une proposition est contradictoire, elle ne peut être «satisfaite dans un champ » ; ou : toute identité logique possède la propriété formelle : sa négation est impossible à satisfaire dans un champ. La preuve ne peut être faite que par induction complète sur la démonstration de la proposition : d’où la nécessité de transformer le traitement de satisfaction qui ne s’applique qu'aux propositions sous forme prénexe (quantificateurs groupés en tête). On le définit ainsi : la proposition étant supposée écrite de façon qu'il n’y ait pas de négation portant sur un quantificateur (ce qui on l’a vu n’exige pas l'application d’une règle mais
(1) Par induction complète :
II > UV1:.Vr Zu. 2n à > UXo..Xo Xy.An (évident)
CASA AA LL À n EUR AV... Vkzy.2nA Uxo..AXoX3...%n A UXoX1...XoXn+1...Xan Pas ik 1 Va Ÿn ÉD Æov*sin
A AU His. sn) >
en > (Uro...%o AgeAn À... À Uri, xs.stn À Axis Xe Astnti.# Stan).
or #s+ on
Cf. GôDeL (1), p. 353-355.
136 THÉORÈME D'HERBRAND
est simple convention d’écriture) on remplace toutes les variables générales par des fonctions d'indices des variables restreintes dans l’étendue desquelles elles se trouvent — ou par un individu choisi une fois pour toutes s’il n’y a pas de telles variables restreintes —, les variables libres par des individus fixes. Chaque étape de l’opération correspond à une répartition des individus construits entre toutes les variables restreintes ; les fonctions d’indices ou fonctions mathématiques dont les arguments sont ainsi individualisés, sont remplacées chacune par un nouvel individu (différent pour chaque fonction et chaque argument). Enfin dans la proposition initiale — d’où les II ont disparu — on substitue à chaque proposition partielle commençant par un x une disjonction toutes les individualisations de la proposition partielle (il y a par rapport au procédé LŒWENHEIM échange des Il et des >, des disjonctions et des conjonctions puisqu'il s’agit de la satisfaction de la négation de la proposition). S'il y a plusieurs ? consécutifs (c.-à-d. tels que les derniers soient dans l'étendue des premiers) on superposera autant de disjonctions que de >: on obtient donc à chaque étape une proposition individualisée, sans quantificateur, la réduite. Lorsque la proposition initiale est une identité logique on doit arriver au bout d’un nombre fini d'étapes à une identité du calcul des propositions. En effet : 19 l’axiome (1) possède cette propriété : les règles précédentes le transforment en :
