Preuve formelle - Formal proof

En logique et en mathématiques , une preuve formelle ou une dérivation est une séquence finie de phrases (appelées formules bien formées dans le cas d'un langage formel ), dont chacune est un axiome , une hypothèse, ou découle des phrases précédentes dans la séquence par une règle d'inférence . Il diffère d'un argument en langage naturel en ce qu'il est rigoureux, sans ambiguïté et vérifiable mécaniquement. Si l'ensemble des hypothèses est vide, alors la dernière phrase d'une preuve formelle est appelée un théorème du système formel . La notion de théorème n'est pas en général efficace , donc il peut n'y avoir aucune méthode par laquelle nous pouvons toujours trouver une preuve d'une phrase donnée ou déterminer qu'il n'en existe aucune. Les concepts de preuve à la Fitch , de calcul des séquences et de déduction naturelle sont des généralisations du concept de preuve.

Le théorème est une conséquence syntaxique de toutes les formules bien formées qui le précèdent dans la preuve. Pour qu'une formule bien formée soit considérée comme faisant partie d'une preuve, elle doit être le résultat de l'application d'une règle de l' appareil déductif (d'un système formel) aux formules bien formées précédentes dans la séquence de preuve.

Les preuves formelles sont souvent construites à l'aide d'ordinateurs dans la preuve interactive de théorèmes (par exemple, grâce à l'utilisation d'un vérificateur de preuves et d' un prouveur de théorème automatisé ). De manière significative, ces preuves peuvent être vérifiées automatiquement , également par ordinateur. La vérification des preuves formelles est généralement simple, tandis que le problème de la recherche de preuves ( prouvant un théorème automatisé ) est généralement insoluble en termes de calcul et/ou seulement semi-décidable , selon le système formel utilisé.

Contexte

Langue formelle

Article principal : Langage formel

Un langage formel est un ensemble de séquences finies de symboles . Un tel langage peut être défini sans référence à aucune signification de l'une de ses expressions ; il peut exister avant qu'une interprétation lui soit assignée, c'est-à-dire avant qu'il n'ait un sens. Les preuves formelles sont exprimées dans certains langages formels.

Grammaire formelle

Articles détaillés : Grammaire formelle et règle de formation

Une grammaire formelle (également appelée règles de formation ) est une description précise des formules bien formées d'un langage formel. Il est synonyme de l'ensemble des chaînes sur l' alphabet du langage formel qui constituent des formules bien formées. Cependant, il ne décrit pas leur sémantique (c'est-à-dire ce qu'ils signifient).

Systèmes formels

Article principal: système formel

Un système formel (également appelé calcul logique ou système logique ) se compose d'un langage formel et d'un appareil déductif (également appelé système déductif ). L'appareil déductif peut consister en un ensemble de règles de transformation (également appelées règles d'inférence ) ou un ensemble d' axiomes , ou avoir les deux. Un système formel est utilisé pour dériver une expression d'une ou plusieurs autres expressions.

Interprétations

Articles principaux: Sémantique formelle (logique) et Interprétation (logique)

Une interprétation d'un système formel est l'attribution de significations aux symboles et de valeurs de vérité aux phrases d'un système formel. L'étude des interprétations est appelée sémantique formelle . Donner une interprétation est synonyme de construire un modèle .

Voir également

Les références

Liens externes