Définissons: "non A"  comme  signifiant  que   A   ne se  trouve pas  dans  la théorie. Définissons: "A et B" comme signifiant que  A est dans la théorie,  B aussi. Enfin, de façon provisoire et pour traduire l'idée d'une règle de passage, définissons :  "A permet B"  comme signifiant que, si  A  est  dans la théorie, alors nous sommes surs que  B  y est aussi.

Si: "A et B" est dans la théorie, la définition mème de: "A et B" nous assure que A est dans la théorie.
Donc: A et B permet A
Pour la mème raison, si: A et B est dans la théorie, B y est aussi.
Donc: A et B permet B

Si  A est dans la théorie, alors B  conduit à: A et B, ce que l'on peut exprimer par :  B permet A et B.  Donc  A   a conduit à  cette dernière écriture, et donc finalement :  A permet [B permet A et B]]

( Remarquons que, si la théorie contient: P et: P permet Q, elle contient alors nécessairement  Q. Car elle contient P, et nous sommes surs que, si elle contient P elle contient Q.  Donc elle contient Q ).

La théorie, lorsqu'elle contient non B, ne contient pas B: c'est la définition mème de non B. Donc il est impossible que cette théorie contienne à la fois B et non B, ou si on préfère contienne: B et non B. Maintenant, regardons le cas ou: A permet [B et non B]. Si A appartenait à la théorie, alors B et non B lui appartiendrait aussi, ce qui serait un échec absolu de toute la démarche. Donc, dans ce cas, A est absent de la théorie. Ainsi:
[A permet [B et non B]] permet [non A]

Si la théorie contient non[nonA], elle ne contient pas [non A]. Or, si elle ne contenait pas A, elle contiendrait non A. Donc elle contient A. Nous sommes donc surs que, contenant non[non A], elle contient A, et donc:
non[non A] permet A

Lorsque le dictionnaire définit un oiseau comme "un animal qui vole", nous savons que cette définition ne change rien sur le fond, car toute vérité comportant le mot: oiseau pourrait ètre réécrite en le remplaçant par sa définition, et réciproquement. Nous constatons là ce que démontre aussi la Logique du premier ordre, à savoir qu'une définition n'est qu'une écriture abrégée et qu'elle ne change pas la vérité. C'est la raison de notre choix initial, consistant à nous appuyer uniquement sur des définitions. Cependant, il est préférable de se fixer un mécanisme unique pour celles-ci. Nous accepterons uniquement les définitions de la forme:
A signifie B.
Donc: Il est permis d'écrire [A signifie B]

Les effets d'une telle écriture sont les suivants: A et B étant à nos yeux une seule et mème chose, on peut remplacer l'une par l'autre et réciproquement. Soit:
[A signifie B] permet [A permet B]
[A signifie B] permet [B permet A]

Enfin, toute définition peut ètre supposée générale: ayant été écrite avec la lettre x, elle reste valable avec la lettre y. Donc, si nous adoptons la notation: A[y/x] pour désigner l'affirmation A dans laquelle on a remplacé x par y (nous l'appellerons: " A dans lequel y remplace x"), alors le seul fait d'avoir écrit: A signifie B nous conduit aussi à: A[y/x) signifie B[y/x].
Donc: [A signifie B] permet [A[y/x] signifie B[y/x]]

( Si nous écrivons sur une page dite page principale ce que nous savons déjà de la théorie, si  sur  une  autre page  dite  page annexe  nous  écrivons  une affirmation A et toute affirmation pouvant ètre obtenue à partir de A ou à partir de la page principale, et si nous obtenons par cette méthode  B  sur  la  page annexe, alors nous pouvons en déduire que:  A permet B.   Car,  si  A  faisait partie de la théorie, alors la page annexe serait pleinement valable et pourrait ètre confondue avec la page principale, et  B  serait donc dans la théorie).

*

Les affirmations obtenues ci-dessus, ainsi que les deux remarques entre parenthèses, constituent  un système  totalement  formalisé  pour progresser dans la théorie. Un ordinateur peut les appliquer sans intervention humaine.

*

Pour montrer la valeur de la méthode décrite ci-dessus, nous allons démontrer grace à elle tous les résultats connus en mathématiques, ou au moins les premiers d'entre eux.
Voici deux définitions très utiles:
(A) signifie A
A => B signifie non (A et non B)

THEOREME: (A permet B) permet (A => B)
(A => B) permet (A permet B)

Démonstration: Faisons l'hypothèse: (A permet B), c'est à dire écrivons cette affirmation sur la première page annexe. Faisons à nouveau une hypothèse, à savoir: (A et non B), c'est à dire que nous écrivons cette nouvelle affirmation sur une deuxième page annexe. Comme les parenthèses peuvent ètre retirées, car: (A et non B) signifie A et non B, on a donc sur la deuxième page annexe: A et non B, puis A (car: A et non B permet A), puis aussi : A permet B copié depuis la première page annexe, et donc B, conséquence de ces deux dernières affirmations. Mais on a aussi sur la deuxième page annexe non B, conséquence de: A et non B. Finalement, cette page comporte B et non B, donc (première page annexe): (A et non B) permet (B et non B), et il s'ensuit: non (A et non B). La première ligne du théorème est démontrée.

Maintenant, faisons l'hypothèse: A => B (première page annexe), puis A (deuxième page annexe), puis: non B (troisième page annexe). Sur la troisième page annexe, on a donc: A recopié, non B, puis: A et non B, puis (A et non B), mais aussi A => B recopié, et donc: non(A et non B). Finalement la troisième page contient: (A et non B) et non (A et non B). Il s'ensuit que la seconde page peut contenir: non B permet (A et non B) et non (A et non B), donc non(non B), donc B. Ainsi la première page peut contenir: A permet B, et la page principale contient: A => B permet (A permet B). La seconde ligne du théorème est démontrée.

THEOREME: (A => B) => (non B => non A)

Notons d'abord que, compte tenu du théorème précédent, il revient au mème de démontrer (U => V) ou de démontrer: U permet V, puisque l'une de ces affirmations permet l'autre. De mème, pour démontrer U => (V => W), il suffit de démontrer: U permet (V permet W), puisque par ailleurs on sait que: (V permet W) permet (V => W), et que la combinaison de ces deux affirmations conduit à: U permet (V => W), donc ): U => (V => W). (NB: La combinaison de: A permet B et de: B permet C conduit à: A permet C pour la raison suivante. Si les deux premières affirmations se trouvent sur la page principale, écrivons sur la page annexe: A, puis: A permet B recopié, puis: B, puis: B permet C recopié, puis: C. On peut donc écrire sur la page principale: A permet C).
Voici maintenant la démonstration. Première page annexe: (A permet B). Deuxième page annexe: non B. Troisième page annexe: A, puis: A permet B recopié, puis B, puis non B recopié, et enfin: B et non B. Donc (deuxième page annexe): A permet (B et non B), puis non A. Finalement, sur la première page annexe: non B permet non A, et enfin (page principale): (A permet B) permet (non B permet non A). Le théorème est démontré.

THEOREME : ((A => B) et ((nonA) => B)) => B

L'intèrèt de ce théorème est que, pour démontrer B, il suffit donc de démontrer B successivement dans le cas ou A est vrai et dans le cas ou non A est vrai. Voici la démonstration du théorème. Supposons (première page annexe): ((A => B) et ((nonA) => B). Alors A => B, donc : non B => non A. Mais aussi : (nonA) => B, donc : non B => non(nonA) (en application du théorème précédent). Ecrivons alors non B sur la deuxième page annexe (ce qui revient à supposer non B). Recopions : non B => non A et non B => non(non A). Combinées avec non B, elles donnent (non A)et non(nonA) donc sur la première page annexe : non B => ((nonA) et non(nonA)), qui conduit à non(nonB), puis à B (puisque non(nonB) permet B). Ainsi le théorème peut ètre énoncé sur la page principale.

THEOREMES : (A et B) => (B et A)
((A et B) et C) => (A et (B et C))

On fait l'hypothèse (A et B) (prem.page annexe). On isole A, puis B. Et comme: B permet(A permet (B et A)), on peut écrire B et A, puis (B et A). Le théorème est démontré. La méthode est identique pour le second théorème.

Définitions : (A ou B) signifie non(nonA et nonB)
(A<=>B) signifie (A=>B) et (B=>A)

THEOREMES : A => ( A ou B)
((A ou B) et non A) => B

En effet, si A (pr. p. ann.) et si ( non A et non B) (deux. p.ann.), cette deuxième hypothèse permet d'écrire : non A, de recopier A, puis d'écrire : A et non A. Donc (pr.p.ann.) non (non A et non B), puis A ou B .
Si (pr.p.ann.): ((A ou B) et non A), et si (deux.p.ann.): non B, alors (deux.p.ann.): non A, puis (non A et non B), mais aussi (A ou B), donc non(non A et non B), d'ou la contradiction qui conduit à non(non B), puis à B.

[ Nous ne poursuivrons pas, dans ce site, cet exposé . Le principe en est le suivant : l'ètre humain déjà intelligent cherche à dire ce que contient la théorie T, totalement inconnue ( à ceci près qu'elle contient toutes les définitions possibles ). Dans une version plus formalisée, l'intelligence préalable est remplacée par la théorie ZF (théorie de Zermelo- Frankel), et on démontre que tout objet T qui contient ses définitions contient les mathématiques ].