Chapitre
Le type associé sera obtenu en enlevant successivement toutes les variables des lignes d'ordre 1, puis toutes celles de ce qui restera des lignes d'ordre 2, puis des lignes d’ordre 3, et ainsi de suite jusqu’à l’ordre p.
Les égalités associées seront obtenues en égalant chaque variable restreinte à la variable générale, ou à la fonction de variable générale, correspondant à l'élément qui lui est attaché. On voit qu’une variable restreinte est toujours égalée à une générale, ou à une fonction des variables générales de lignes dont l’ordre est inférieur au sien; et donc que ces égalités fournissent des égalités associées compatibles avec le type considéré.
Il suffit de voir que la disjonction ainsi obtenue est une identité; or, il est évident qu’elle résulte de la deuxième disjonction d'ordre p associée à P (3.4), en remplaçant chaque élément des champs, par la variable générale, ou la fonction de variable générale correspondante (chaque ligne du schème correspond à un terme de cette identité).
Corollaire. Une proposition de propriété B est vraie.
Car on a vu: 1) Que la propriété B équivaut à la propriété C (3.31).
2) Qu'une proposition de propriété À est vraie (2.3).
Ceci démontre la première partie du théorème.
5.2. Pour démontrer la deuxième partie du théorème, nous procédons par récurrence sur la démonstration de la proposition.
19, Si PvP a la propriété B, il en est de même de P (d’après la définition de 3.22).
22 Si dx a la propriété B, (x). x l’a aussi. En effet, pour fabriquer les réduites de x et (x). x, il faut précisément remplacer ces propositions par: (y:y»..y,x). dx, si Yiy>...y, sont les variables réelles de (x). x, comme on a vu en 3.2.
Lemme 2. La propriété C se conserve dans l'emploi de la deuxième règle de généralisation (sous la forme de Ch. 3, 1.4).
t étant un individu dépendant de variables réelles, on passe de -.®Dr à —.(4x). D x.
Prenons la propriété C sous la forme donnée en 3.4.
Nous savons (3.221) qu'aux variables réelles vont correspondre des éléments fixes de C:; alors l’élément correspondant à { sera dans C, (avec k> 2); appelons le à..
— 115 — Chapitre 5. 5.2.
Supposons que la première proposition ait la propriété C d'ordre p. Considérons la deuxième disjonction associée (voir 3.4) d'ordre p-k—1 pour la deuxième. Ne considérons dans cette disjonction que les termes où x est remplacé par a: On voit immédiatement que leur disjonction est une dre disjonction d'ordre p associée à la proposition ® #, le premier champ étant C;; donc c’est une identité propositionnelle: et il en est donc de même de la disjonction primitive.
5.3. Lemme 3.:°S; P ef PDQ ont la propriété C d'ordre p, il en est de même de Q.
P.P)Q a aussi la propriété C d'ordre p d’après 3.53. Mettons P et Q sous forme normale (Ch. 2, 3.101); ils s’écrivent respectivement:
(CE yi EyreEy,).Myiyasy,kixs...x, (CEzitz...Ez).Nzz...z,x1x5...x
et
en mettant en évidence toutes les variables réelles (certaines pourront être fictives (Ch. 5, 3.52) dans P ou Q). P.P )Q peut
s’écrire, en le transformant par les règles de passage:
VE Y, Pit es 2)"
0 ,,0 0 dei 1 MyT See ÿ9 Xi kocee Xpe MY Var Ve Ai Kate: Xn D)NzegoesZqees Kiss ne
Dans cette proposition, les o, valent O ou 1 suivant que y, est restreinte ou générale dans P. Nous nous arrangeons comme on voit, pour que de deux symboles (y?) et (y!) qui se suivent, le premier soit toujours symbole de variable restreinte, le deuxième symbole de variable générale (car si y? est restreinte, y} est générale, et inversement d’après Ch. 2, 3.102). Prenons la propriété C pour cette proposition sous la forme donnée en 3.4. On a donc des champs C; Coeee Corse Chip engendrés par les fonctions descriptives et d'indice de cette proposition; nous les transformons en des champs C;C;'...C}...C;:,11, comme suit: C, et C;’ sont identiques; on obtient en général les C, à partir des C,, de la manière suivante: appelons f, la fonc-