LE TIERS EXCLU INOFFENSIF

pour les égalités numériques (qui sont des espèces d’identités) ; lorsque est Y une telle équation on a donc

AN

(on sait qu’en logique intuitionniste seule l'implication A+ — — À vaut). GÔDEL démontre par récurrence sur la construction de la proposition (c’est-à-dire en appliquant règle de généralisation et règle de passage) que l’implication vaut pour toutes les propositions de l’arithmétique définie par les axiomes de HERBRAND. Les moyens de démonstration y sont donc exactement les mêmes, que l’on prenne la logique classique ou la logique intuitionniste : les deux arithmétiques se recouvrent exactement. La raison en est simple : les individus sur lesquels portent les propositions arithmétiques sont toujours calculables effectivement (par un nombre fini de démarches ; ce sont les valeurs de fonctions récurrentes de schéma quelconque mais toujours de type 1 — c’est-à-dire ne faisant pas intervenir la référence à des collections infinies). Dès lors la proscription intuitionniste des affirmations non constructives d’existence n’a pour effet qu'un changement d'écriture : au lieu de > X (x) on mettra — I — YX (x) ; mais on aura exactement k |

LA

le même nombre d’affirmations, « puisqu'on a le droit d’appliquer le prédicat de l’absurdité aux propositions générales » (:). La séparation entre mathématique intuitionniste et mathématique classique n'apparaît qu'avec l’analyse et les définitions non prédicatives (c'est-à-dire prenant leur départ de systèmes infinis ; le tiers exclu ne joue là encore aucun rôle).

SKOLEM (?) avait d’ailleurs obtenu un résultat un peu plus étendu grâce à la considération des champs : nile tiers exclu, ni la fonction « (pour variables de type 1) ne peuvent appor-

(1) GÔDEL, 1bid.

(2) SkoLEM (IV), p. 30.