Système formel - Formal system

Un système formel est une structure abstraite utilisée pour déduire des théorèmes à partir d'axiomes selon un ensemble de règles. Ces règles, qui sont utilisées pour effectuer l'inférence de théorèmes à partir d'axiomes, sont le calcul logique du système formel. Un système formel est essentiellement un « système axiomatique ».

En 1921, David Hilbert a proposé d'utiliser un tel système comme fondement de la connaissance en mathématiques . Un système formel peut représenter un système bien défini de pensée abstraite .

Le terme formalisme est parfois synonyme rude pour système formel , mais il fait également référence à un style donné de notation , par exemple, Paul Dirac de notation Ket de soutien - gorge .

Fond

Chaque système formel utilise des symboles primitifs (qui forment collectivement un alphabet ) pour construire de manière finie un langage formel à partir d'un ensemble d' axiomes grâce à des règles de formation inférentielles .

Le système est donc constitué de formules valides construites à partir de combinaisons finies des symboles primitifs, combinaisons formées à partir des axiomes conformément aux règles énoncées.

Plus formellement, cela peut être exprimé comme suit :

  1. Un ensemble fini de symboles, connu sous le nom d'alphabet, qui concatène des formules, de sorte qu'une formule n'est qu'une chaîne finie de symboles tirés de l'alphabet.
  2. Une grammaire composée de règles pour former des formules à partir de formules plus simples. Une formule est dite bien formée si elle peut être formée en utilisant les règles de la grammaire formelle. Il est souvent nécessaire qu'il y ait une procédure de décision pour décider si une formule est bien formée.
  3. Un ensemble d'axiomes, ou schémas d'axiomes , constitué de formules bien formées.
  4. Un ensemble de règles d'inférence . Une formule bien formée qui peut être déduite des axiomes est connue sous le nom de théorème du système formel.

Récursif

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 semi- décidables .

Inférence et implication

L' implication du système par son fondement logique est ce qui distingue un système formel d'autres qui peuvent avoir une base dans un modèle abstrait. Souvent, le système formel sera la base ou même identifié avec une théorie ou un domaine plus large (par exemple la géométrie euclidienne ) compatible avec l'usage des mathématiques modernes telles que la théorie des modèles .

Langue formelle

Un langage formel est un langage défini par un système formel. Comme les langues en linguistique , les langues formelles ont généralement deux aspects :

  • la syntaxe d'une langue est à quoi ressemble la langue (plus formellement : l'ensemble des expressions possibles qui sont des énoncés valides dans la langue) étudiée en théorie formelle des langues
  • la sémantique d'une langue est ce que signifient les énoncés de la langue (qui se formalise de diverses manières, selon le type de langue en question)

En informatique et en linguistique, seule la syntaxe d'un langage formel est généralement considérée via la notion de grammaire formelle . Une grammaire formelle est une description précise de la syntaxe d'un langage formel : un ensemble de chaînes . Les deux principales catégories de grammaire formelle sont celles des grammaires génératives , qui sont des ensembles de règles permettant de générer des chaînes dans une langue, et celle des grammaires analytiques (ou grammaire réductrice) qui sont des ensembles de règles sur la façon dont une chaîne peut être analysé pour déterminer s'il fait partie de la langue. En bref, une grammaire analytique décrit comment reconnaître lorsque des chaînes sont membres de l'ensemble, tandis qu'une grammaire générative décrit comment écrire uniquement ces chaînes dans l'ensemble.

En mathématiques , une langue formelle n'est généralement pas décrite par une grammaire formelle mais par (a) une langue naturelle, comme l'anglais. Les systèmes logiques sont définis à la fois par un système déductif et par un langage naturel. Les systèmes déductifs à leur tour ne sont définis que par le langage naturel (voir ci-dessous).

Système déductif

Un système déductif , également appelé appareil déductif ou logique , se compose des axiomes (ou schémas d'axiomes ) et des règles d'inférence qui peuvent être utilisées pour dériver des théorèmes du système.

De tels systèmes déductifs préservent les qualités déductives dans les formules qui sont exprimées dans le système. Habituellement, la qualité qui nous intéresse est la vérité par opposition au mensonge. Cependant, d'autres modalités , telles que la justification ou la croyance peuvent être préservées à la place.

Afin de maintenir son intégrité déductive, un appareil déductif doit être définissable sans référence à une quelconque interprétation prévue de la langue. Le but est de s'assurer que chaque ligne d'une dérivation n'est qu'une conséquence syntaxique des lignes qui la précèdent. Il ne devrait y avoir aucun élément d' interprétation du langage qui soit impliqué dans la nature déductive du système.

Un exemple de système déductif est la logique des prédicats du premier ordre .

Système logique

Un système ou langage logique (à ne pas confondre avec le type de « langage formel » discuté ci-dessus qui est décrit par une grammaire formelle), est un système déductif (voir la section ci-dessus ; le plus souvent la logique des prédicats du premier ordre ) avec d'autres (non- logique) des axiomes et une sémantique . Selon l' interprétation de la théorie des modèles , la sémantique d'un système logique décrit si une formule bien formée est satisfaite par une structure donnée. Une structure qui satisfait à tous les axiomes du système formel est appelée modèle du système logique. Un système logique est solide si chaque formule bien formée qui peut être déduite des axiomes est satisfaite par chaque modèle du système logique. Inversement, un système logique est complet si chaque formule bien formée qui est satisfaite par chaque modèle du système logique peut être déduite des axiomes.

Un exemple de système logique est l'arithmétique de Peano .

Histoire

Les premiers systèmes logiques comprennent la logique indienne de Pāṇini , la logique syllogistique d'Aristote, la logique propositionnelle du stoïcisme et la logique chinoise de Gongsun Long (vers 325-250 avant notre ère). Plus récemment, les contributeurs incluent George Boole , Augustus De Morgan et Gottlob Frege . La logique mathématique s'est développée dans l' Europe du XIXe siècle .

Formalisme

Le programme d'Hilbert

David Hilbert a initié un mouvement formaliste qui a finalement été tempéré par les théorèmes d'incomplétude de Gödel .

Manifeste QED

Le manifeste QED représentait un effort ultérieur, encore infructueux, de formalisation des mathématiques connues.

Exemples

Voici des exemples de systèmes formels :

Variantes

Les systèmes suivants sont des variantes des systèmes formels.

Système de preuve

Les preuves formelles sont des séquences de formules bien formées (ou wff en abrégé). Pour qu'un wff soit considéré comme faisant partie d'une preuve, il peut s'agir d'un axiome ou du produit de l'application d'une règle d'inférence sur les wff précédents dans la séquence de preuve. Le dernier wff de la séquence est reconnu comme un théorème .

Le point de vue selon lequel générer des preuves formelles est tout ce qu'il y a aux mathématiques est souvent appelé formalisme . David Hilbert a fondé les métamathématiques comme discipline pour discuter des systèmes formels. Tout langage que l'on utilise pour parler d'un système formel est appelé métalangage . Le métalangage peut être un langage naturel, ou il peut être lui-même partiellement formalisé, mais il est généralement moins complètement formalisé que la composante langage formel du système formel examiné, qui est alors appelé langage objet , c'est-à-dire l'objet du débat en question.

Une fois qu'un système formel est donné, on peut définir l'ensemble des théorèmes qui peuvent être prouvés à l'intérieur du système formel. Cet ensemble se compose de tous les wffs pour lesquels il existe une preuve. Ainsi, tous les axiomes sont considérés comme des théorèmes. Contrairement à la grammaire pour wffs, il n'y a aucune garantie qu'il y aura une procédure de décision pour décider si un wff donné est un théorème ou non. La notion de théorème qui vient d'être définie ne doit pas être confondue avec les théorèmes sur le système formel , qui, afin d'éviter toute confusion, sont généralement appelés métathéorèmes .

Voir également

Les références

Lectures complémentaires

Liens externes