Logique mathématique
Image manquante
Fairytale_info.png
lettre i
La logique mathématique est une discipline des mathématiques, étudiant les systèmes formels en relation de la manière qu'elles encodent des concepts intuitifs de preuve et traitement de l'information. Pour l'histoire elle fut développée pour comprendre et présenter les travaux de Kurt Gödel sur les bases des mathématiques.
L'étendue de la logique mathématique
Bien que le candide peut penser que la logique mathématique est la logique des mathématiques, la vérité est plutôt qu'elle ressemble plus aux mathématiques de la logique. Elle comprend ces parties de la logique qui peuvent être modelée mathématiquement. Des intitulés antérieurs furent la logique symbolique (en opposition à la logique philosophique); et les métamathématiques, qui est désormais restreinte comme nom à certains aspects de la théorie de la preuve.
Le nom fut donné par Giuseppe Peano. Pour l'essentiel c'est encore la logique d'Aristote mais écrit comme une branche de l'algèbre abstraite.
Des essais de traiter les opérations de la logique formelle est d'une façon analogue a été fait assez fréquemment par certains des mathématiciens les plus philosophes, comme Leibniz et Lambert; mais leurs recherches restaient peu connues, et ce fut George Boole et Auguste De Morgan, vers le milieu du XIXe siècle, pour laquelle une mathématique -- bien que non-quantitatif -- façon de regarder la logique devait être fait. Par cela, non seulement la doctrine traditionelle ou aristotélicienne de la logique fut réformée et complétée, mais de cela ils ont développés un instrument qui traite d'une manière certaine avec la tâche d'enqueter les concepts fondamentaux des mathématiques -- une tâche que les philosophes ont constamment examinés, et pour laquelle ils ont aussi souvent échoués -- bien que ce soit trompeur de dire que les controverses qui avaient lieu dans la période 1900-1925 avaient toutes été résolues. (voir aussi mathématiques)
Bien que le développement traditionnel de la logique (voir liste des sujets en logique place une forte emphase sur la forme des arguments, l'attitude de la logique mathématique courante peut être résumée comme l'étude combinatoire du contenu. Ceci couvre à la fois le syntactique (par exemple, envoyer une chaîne de caractères d'une langue naturelle à un compilateur pour écrire comme une séquence d'instructions d'ordinateur) et la sémantique (construction des modèles spécifiques ou de leurs ensembles complets, dans la théorie du modèle.
La plus grande partie de la matière dépend de l'existence d'algorithmes efficaces pour vérifier les preuves. Cela n'est pas souligné dans les traitements traditionels: cela pourrait changer comme les programmes progressent et l'exposition commence à rattraper.
Les résultats d'instauration
Quelques résultats importants, tous découvert pendant les années 1930, sont:
- des preuves putatives de la validité universelle des formules du premier ordre peuvent être vérifiées rapidement pour la validité, par algorithme. En langage technique, l'ensemble des preuves est une primitive récursive. Essentiellement, c'est le théorème d'incomplétude de Gödel, bien que ce théorème soit habituellement présenté d'une manière qui ne rend pas évident qu'il ait quelque chose à voir avec les algorithmes.
- l'ensemble des formules du premier ordre n'est pas calculable, càd, qu'il n'y a pas d'algorithmes pour vérifier une validité universelle. Il y a, cependant, un algorithme qui se comporte de cette façon: donnant une formule du premier ordre en entrée, l'algorithme éventuellent s'interrompt si la formule est universellement valide, et continue pour toujours autrement. Si l'algorithme est utilisé depuis des milliards d'années la réponse reste inconnue. En d'autres mots, cet ensemble est « récursivement énumérable » ou comme c'est quequefois dit plus suggestivement « semi-décidable ».
- L'ensemble de toutes les formules universellement valides de second ordre n'est pas énumérable même récursivement. Ceci est une conséquence du théorème de l'incomplétude.