Démonstration formelle
# Démonstration formelle

Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une. Le concept de déduction naturelle est une généralisation de la notion de démonstration.

Le théorème est une conséquence syntaxique de toutes les formules bien formées qui la précèdent dans la démonstration. Pour qu'une formule bien formée soit présente dans le cadre d'une démonstration, elle doit être le résultat de l'application d'une règle de l'appareil déductif.

Les démonstration formelles sont souvent construits à l'aide d'ordinateurs en tant qu'assistants de preuve. De manière significative, ces preuves peuvent être vérifiées automatiquement, également par ordinateur. La vérification des démonstrations formelles est généralement simple, alors que trouver des démonstrations (démonstration automatique de théorèmes) est généralement informatiquement intraitable et/ou seulement semi-décidable, selon le système formel utilisé.

## Contexte

### Langage formel

Un langage formel est un ensemble de suites finies de symboles. Un tel langage peut être défini sans référence à des significations de l'une de ses expressions; il peut exister avant qu'une interprétation lui soit attribué – c'est-à-dire, une signification. Les démonstrations formelles sont exprimées dans un langage formel.

### Grammaire formelle

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

### Système formel

Un système formel (également appelé un calcul logique ou un système logique) se compose d'un langage formel conjointement avec un système déductif. Le système déductif peut être constitué d'un ensemble de règles de transformation (également appelées règles d'inférence) ou d'un ensemble d'axiomes, ou les deux. Un système formel est utilisé pour dériver une expression d'une ou plusieurs autres expressions.

### Interprétations

Une interprétation d'un système formel est l'attribution de signification aux symboles, et des valeurs aux suites d'un système formel. L'étude des interprétations est appelée la sémantique formelle. Donner une interprétation est synonyme de construction d'une structure.

