Worldlex Wiki En 1921, David Hilbert proposa d'utiliser les systèmes formels comme fondement de la connaissance en mathématiques . Cependant, en 1931, Kurt Gödel démontra qu'aucun système formel cohérent , suffisamment puissant pour exprimer l'arithmétique élémentaire, ne peut prouver sa propre complétude . Ceci montra concrètement que le programme de Hilbert, tel qu'énoncé, était impossible.
Le terme formalisme est parfois un synonyme approximatif de système formel , mais il fait également référence à un style de notation donné , par exemple la notation bra-ket de Paul Dirac .
Un système formel comporte au minimum les composants suivants :
- Le langage formel est un ensemble de formules bien formées , qui sont des chaînes de symboles d'un alphabet , formées par une grammaire formelle (constituée de règles de production ou de règles de formation ).
- Système déductif, appareil déductif ou système de preuve , qui comporte des règles d'inférence prenant des axiomes et inférant des théorèmes , tous deux faisant partie du langage formel.
- Dans certains cas, un système inductif est utilisé pour établir une preuve en commençant par un cas simple, puis en le généralisant.
Un système formel est dit récursif (c’est-à-dire effectif) ou récursivement énumérable si l’ensemble des axiomes et l’ensemble des règles d’inférence sont respectivement des ensembles décidables ou des ensembles semi-décidables .
langage formel
- La syntaxe, c'est ce à quoi ressemble le langage (plus formellement : l'ensemble des expressions possibles qui constituent des énoncés valides dans le langage).
- La sémantique désigne la signification des énoncés de la langue (qui est formalisée de diverses manières, selon le type de langue en question).
En général, seule la syntaxe d'un langage formel est considérée à travers la notion de grammaire formelle . Les deux principales catégories de grammaires formelles sont les grammaires génératives , qui sont des ensembles de règles sur la façon dont les chaînes de caractères d'un langage peuvent être écrites, et les grammaires analytiques (ou grammaires réductives ), qui sont des ensembles de règles sur la façon dont une chaîne de caractères peut être analysée pour déterminer si elle appartient au langage.
Système déductif
Pour préserver son intégrité déductive, un appareil déductif doit pouvoir être défini sans faire référence à une quelconque interprétation du langage. L'objectif est de garantir que chaque ligne d'une dérivation soit simplement une conséquence logique des lignes qui la précèdent. Aucun élément d' interprétation du langage ne doit interférer avec la nature déductive du système.
La conséquence logique (ou l'implication) du système découlant de son fondement logique est ce qui distingue un système formel d'autres systèmes pouvant reposer sur un modèle abstrait. Souvent, le système formel constitue le fondement d'une théorie ou d'un domaine plus vaste (par exemple, la géométrie euclidienne ), voire s'y identifie, conformément à l'usage en mathématiques modernes, notamment en théorie des modèles .les axiomes concernant l'égalité utilisés en logique du premier ordre .
Les deux principaux types de systèmes déductifs sont les systèmes de preuve et la sémantique formelle.
Système de preuve
Une fois un système formel défini, on peut déterminer l'ensemble des théorèmes démontrables au sein de ce système. Cet ensemble comprend toutes les formules bien formées (FBF) ayant une démonstration. Ainsi, tous les axiomes sont considérés comme des théorèmes. Contrairement à la grammaire des FBF, il n'existe aucune garantie qu'une procédure de décision permette de déterminer si une FBF donnée est un théorème ou non.
L'idée que les mathématiques se résument à la production de démonstrations formelles est souvent appelée formalisme . David Hilbert a fondé la métamathématique , une discipline permettant d'étudier les systèmes formels. Tout langage utilisé pour parler d'un système formel est appelé métalangage . Le métalangage peut être un langage naturel ou être partiellement formalisé, mais il est généralement moins formalisé que le langage formel du système formel étudié, appelé alors langage objet , c'est-à-dire l'objet de la discussion. La notion de théorème que nous venons de définir ne doit pas être confondue avec les théorèmes portant sur le système formel , qui, pour éviter toute confusion, sont généralement appelés métathéorèmes .
Sémantique formelle d'un système logique
Un système logique est :
- Le système est correct si chaque formule bien formée qui peut être déduite des axiomes est satisfaite par chaque modèle du système logique.
- Sémantiquement complet , si chaque formule bien formée satisfaite par chaque modèle du système logique peut être déduite des axiomes.
L'arithmétique de Peano est un exemple de système logique . Le modèle standard de l'arithmétique définit le domaine de discours comme étant les entiers non négatifs et attribue aux symboles leur signification usuelle. Il existe également des modèles non standard de l'arithmétique .
Histoire
David Hilbert a initié un mouvement formaliste appelé le programme de Hilbert comme solution proposée à la crise des fondements des mathématiques , qui a finalement été tempéré par les théorèmes d'incomplétude de Gödel . Le manifeste QED représentait un effort ultérieur, jusqu'alors infructueux, de formalisation des mathématiques connues.