Logique mathématique - Définition

Introduction

La logique mathématique, ou logique formelle, est une discipline des mathématiques qui définit et étudie les représentations formelles du langage mathématique. Les objets fondamentaux de la logique mathématiques sont les formules modélisant les énoncés mathématiques, les dérivations modélisant les raisonnements mathématiques et les sémantiques établissant les liens entre ces modèles et les objets qu'ils sont censés représenter.

Sous-domaines de la logique mathématique

Au cours du XX^e siècle, la logique mathématique s'est ramifiée en de nombreux sous-domaines :

• la théorie des ensembles ;
• la théorie de la démonstration ;
• la théorie des modèles ;
• la théorie de la calculabilité.

Cette classification en quatre grands axes, généralement admise, est celle proposée par Jon Barwise éditeur de l'ouvrage collectif Handbook of Mathematical Logic. Depuis, un cinquième grand axe semble se dessiner avec les travaux sur la théorie des types.

Quelques résultats fondamentaux

Quelques résultats importants ont été établis pendant la décennie 1930 :

• Le théorème de complétude du calcul des prédicats du premier ordre que Gödel a montré dans sa thèse de doctorat, un an avant son célèbre théorème d'incomplétude. Ce théorème énonce que toute démonstration mathématique peut être représentée dans le formalisme du calcul des prédicats (qui est donc complet).

• L'ensemble des théorèmes du calcul des prédicats n'est pas calculable, c'est-à-dire qu'aucun algorithme ne permet de vérifier si un énoncé donné est prouvable ou non. Il existe, cependant, un semi-algorithme : celui-ci prend en entrée une formule du premier ordre ; il s'interrompt en répondant «oui» si la formule est universellement valide, et continue indéfiniment sinon. Même si ce semi-algorithme s'exécute pendant des milliards d'années, il peut ne pas conclure qu'une proposition n'est pas universellement valide. En d'autres termes, l'ensemble des formules du premier ordre universellement valide est « récursivement énumérable » ; on dit qu'il est « semi-décidable ».

• La cohérence (non contradiction) d'un système d'axiomes (par exemple : les axiomes de Peano pour l'arithmétique) n'est pas une conséquence de ces seuls axiomes sauf dans des cas triviaux (notamment lorsque les axiomes sont contradictoires entre eux). C'est le fameux second théorème d'incomplétude de Gödel.

• L'ensemble de toutes les formules universellement valides du second ordre n'est pas énumérable, même récursivement. Ceci est une conséquence du théorème d'incomplétude.

• Tout théorème purement logique peut être démontré en n'utilisant à tout moment que des propositions qui sont des sous-formules de son énoncé. Connu sous le nom de théorème de la sous-formule, il est une conséquence du théorème d'élimination des coupures en calcul des séquents de Gerhard Gentzen.
  • Accessoirement, ce théorème de la sous-formule fournit un théorème de cohérence pour la logique, car il interdit la dérivation de la formule vide (identifiée à l'absurdité).

D'autres résultats importants ont été établis pendant la deuxième partie du XX^e siècle.

• L'indépendance de l'hypothèse du continu par rapport aux autres axiomes de la théorie des ensembles (ZF) est achevée en 1963 par Paul Cohen.
• La théorie de la calculabilité se développe.
• Au tournant de la décennie 1980, la correspondance de Curry-Howard identifie la simplification des démonstrations et les programmes, créant ainsi un pont entre mathématiques et informatique.
• En 1990, cette correspondance est étendue à la logique classique.