Logique mathématique

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 etre 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 Augustus 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 etre résumée comme l'étude combinatoire du contenu. Ceci couvre à  la fois le syntactique (par exemple, envoyé 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. Celà  n'est pas souligné dans les traitements traditionels: celà  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 etre 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 quelquechose à  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.