logique (suite)

Herbrand

Jacques Herbrand, mort à vingt-trois ans en 1931 dans un accident de montagne, a eu néanmoins le temps d’apporter au développement de la logique mathématique une contribution de tout premier ordre. Celle-ci concerne essentiellement la théorie de la démonstration hilbertienne et la métathéorie du calcul des prédicats du premier ordre. Herbrand a découvert en 1929 un théorème dont Bernays a écrit qu’il était le « théorème central de la logique des prédicats », et qui comporte de nombreuses applications, notamment aux problèmes de décision, de réduction et de consistance. La méthode de Herbrand, qui est contenue en germe dans un certain nombre de mémoires de Löwenheim et de Skolem, consiste à établir une certaine relation entre le problème de la validité d’une formule dans le calcul des prédicats et le problème de la validité (au sens du calcul propositionnel) d’une formule sans quantificateur qui peut être construite à partir d’elle selon des règles déterminées. C’est chez Herbrand que l’on voit apparaître pour la première fois le théorème de la déduction (que Tarski déclare cependant avoir connu et utilisé dès 1921), et c’est lui qui a suggéré à Gödel l’interprétation que celui-ci a proposée en 1934 pour la notion de récursivité (le concept de fonction récursive générale est désigné fréquemment comme le concept de Herbrand-Gödel-Kleene).

Gentzen

De Gehrard Karl Erich Gentzen (1909-1945), il a déjà été question à propos de la théorie de la démonstration. Dans un mémoire de 1934, Gentzen a établi un verschärfter Hauptsatz (théorème principal renforcé) qui est en relation très étroite avec le théorème de Herbrand. Croyant à tort que le théorème de Herbrand ne s’applique qu’à des formules prénexes, Gentzen le considère comme un simple cas particulier du sien. Une meilleure connaissance de l’œuvre de Herbrand permet au contraire de se rendre compte aujourd’hui que c’est le verschärfter Hauptsatz de Gentzen qui est en réalité un cas particulier du théorème fondamental de Herbrand. Les recherches de Gentzen dans le domaine de la déduction logique ont porté sur la construction d’un « formalisme qui reflète le plus exactement possible les raisonnements logiques qui sont réellement utilisés dans les démonstrations mathématiques ». Les méthodes dites « de déduction naturelle » mises au point par Gentzen se distinguent fondamentalement de celles qui sont utilisées dans les logiques que l’on peut appeler axiomatiques en ce qu’elles adoptent comme concept central le concept de déduction sous hypothèses et enchaînent non pas directement des propositions, mais bien des raisonnements ou inférences logiques présentés sous forme d’« énoncés de conséquence » (Sequenzen). La logique naturelle de Gentzen a donné naissance, par l’intermédiaire de la méthode des « tableaux sémantiques » d’E. W. Beth (1955), à une méthode de démonstration particulièrement élégante et efficace connue et utilisée aujourd’hui largement sous le nom de méthode des tableaux analytiques ou méthode des arbres (cf. R. M. Smullyan, First-Order Logic, 1968).

Gödel

Kurt Gödel a démontré en 1930 la complétude du calcul des prédicats du premier ordre et a provoqué en 1931 une véritable révolution dans l’univers de la logique en établissant l’incomplétude nécessaire de tout système formel suffisamment fort pour exprimer l’arithmétique élémentaire et l’impossibilité d’établir la non-contradiction d’un tel système sans recourir à des moyens plus puissants que ceux dont dispose le système lui-même. Cette découverte capitale a représenté naturellement un coup d’arrêt sérieux pour les entreprises de type formaliste et a ruiné tout espoir de réaliser le programme de Hilbert sous sa forme primitive. Gödel a démontré également en 1940 que, si une certaine axiomatisation de la théorie des ensembles sans l’axiome du choix est consistante, elle le reste lorsqu’on ajoute aux axiomes l’axiome du choix ou l’hypothèse du continu généralisée ou les deux.

Ce résultat a trouvé en quelque sorte son complément dans la démonstration de l’indépendance de l’hypothèse du continu qui a été donnée en 1963 par Paul J. Cohen.

Quelques aperçus sur des développements récents

La première démonstration d’indécidabilité pour le calcul des prédicats du premier ordre a été donnée en 1936 par Alonzo Church (né en 1903). Le problème de la décision a néanmoins été résolu pour toute une série de cas spéciaux dont certains présentent un intérêt considérable. En plus des contributions déjà évoquées antérieurement, il faut indiquer notamment celles de H. Behmann (1922), Bernays et Schönfinkel (1928), Ackermann (1928, 1933), Herbrand (1931), Gödel (1932, 1933), L. Kalmár (1933), K. Schütte (1934), Quine (1944, 1945). Pour un exposé d’ensemble, voir W. Ackermann, Solvable Cases of the Decision Problem (1954). D’importants résultats ont été obtenus pendant les dernières décennies sur les problèmes de décidabilité et de réduction dans les domaines les plus divers (Tarski, A. Mostowski et R. M. Robinson [Undecidable Theories, 1953], L. Kalmár, J. Suranyi, L. McKinsey, E. M. Post. A. A. Markov, M. Hall, P. S. Novikov, M. O. Rabin, etc.)

L’idée simple de définition récursive d’une fonction telle qu’on la trouve originairement chez Dedekind, Peano et Skolem a été progressivement généralisée et précisée jusqu’à ce que l’on parvienne à un concept susceptible de constituer un équivalent exact pour la notion relativement vague d’« effectivité » ou de « constructivité » en mathématiques. Les travaux décisifs sur cette question ont été effectués essentiellement pendant la période 1930-1940 et sont dus à Gödel, S. C. Kleene, A. Church, A. M. Turing (1912-1954) et Post. (A. A. Markov a fourni en 1951 avec sa théorie des algorithmes une solution nouvelle et équivalente du problème.) En 1936, Church a proposé d’identifier la notion intuitive de « fonction effectivement calculable » avec celle de « fonction récursive générale » au sens défini par Kleene (General Recursive Functions of Natural Numbers, 1936). On a pu démontrer qu’un certain nombre d’autres substituts formels proposés pour la notion de calculabilité (comme, par exemple, la λ-définissabilité de Church) étaient équivalents à la notion de récursivité générale. La suggestion de Church (connue sous le nom de thèse de Church) a reçu par le fait une certaine confirmation ; mais elle a été attaquée récemment (1957) par Kalmár, et elle est considérée par certains comme peu plausible.