Métalologique - Metalogic
La métalogique est l'étude de la métathéorie de la logique . Alors que la logique étudie comment les systèmes logiques peuvent être utilisés pour construire des arguments valides et solides , la métalogique étudie les propriétés des systèmes logiques. La logique concerne les vérités qui peuvent être déduites à l'aide d'un système logique ; métalogique concerne les vérités qui peuvent être dérivées sur les langues et les systèmes qui sont utilisés pour exprimer des vérités.
Les objets de base de l'étude métalogique sont les langages formels, les systèmes formels et leurs interprétations . L'étude de l'interprétation des systèmes formels est la branche de la logique mathématique connue sous le nom de théorie des modèles , et l'étude des systèmes déductifs est la branche connue sous le nom de théorie de la preuve .
Aperçu
Langue formelle
Un langage formel est un ensemble organisé de symboles , dont les symboles le définissent précisément par forme et par lieu. Une telle langue peut donc être définie sans référence au sens de ses expressions ; il peut exister avant qu'on ne lui donne une interprétation, c'est-à-dire avant qu'il n'ait un sens. La logique du premier ordre est exprimée dans un langage formel. Une grammaire formelle détermine quels symboles et ensembles de symboles sont des formules dans un langage formel.
Un langage formel peut être formellement défini comme un ensemble A de chaînes (suites finies) sur un alphabet fixe . Certains auteurs, dont Rudolf Carnap , définissent le langage comme la paire ordonnée <α, A >. Carnap exige également que chaque élément de α apparaisse dans au moins une chaîne de A .
Règles de formation
Les règles de formation (également appelées grammaire formelle ) sont une description précise des formules bien formées d'un langage formel. Ils sont synonymes 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
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.
Un système formel peut être formellement défini comme un triplet ordonné <α, , d>, où d est la relation de dérivabilité directe. Cette relation est comprise dans un sens compréhensif tel que les phrases primitives du système formel sont prises comme directement dérivables de l' ensemble vide de phrases. La dérivabilité directe est une relation entre une phrase et un ensemble fini, éventuellement vide de phrases. Les axiomes sont choisis de telle sorte que chaque premier membre de d est un membre de et chaque deuxième membre est un sous-ensemble fini de .
Un système formel peut aussi être défini avec la seule relation d. Ainsi peuvent être omis et dans les définitions de langage formel interprété , et système formel interprété . Cependant, cette méthode peut être plus difficile à comprendre et à utiliser.
Preuves formelles
Une preuve formelle est une séquence de formules bien formées d'un langage formel, dont la dernière est un théorème d'un système formel. Le théorème est une conséquence syntaxique de toutes les formules bien formées qui le précèdent dans le système de preuve. Pour qu'une formule bien formée soit considérée comme faisant partie d'une preuve, elle doit résulter 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.
Interprétations
Une interprétation d'un système formel est l'attribution de significations aux symboles et de valeurs de vérité aux phrases du système formel. L'étude des interprétations s'appelle la sémantique formelle . Donner une interprétation est synonyme de construire un modèle .
Distinctions importantes
Métalangage-langage objet
En métalogique, les langages formels sont parfois appelés langages objets . Le langage utilisé pour faire des déclarations sur un langage objet est appelé un métalangage . Cette distinction est une différence clé entre la logique et la métalogique. Alors que la logique traite des preuves dans un système formel , exprimées dans un langage formel, la métalogique traite des preuves concernant un système formel qui sont exprimées dans un métalangage concernant un langage objet.
Syntaxe–sémantique
En métalogique, la « syntaxe » concerne les langages formels ou les systèmes formels sans égard à leur interprétation, tandis que la « sémantique » concerne les interprétations des langages formels. Le terme « syntaxique » a une portée légèrement plus large que « la théorie de la preuve », puisqu'il peut être appliqué aux propriétés des langages formels sans aucun système déductif, ainsi qu'aux systèmes formels. « Sémantique » est synonyme de « théorie des modèles ».
Utilisation–mention
En métalogique, les mots « utiliser » et « mentionner », à la fois sous leur forme nominale et verbale, prennent un sens technique afin d'identifier une distinction importante. La distinction utilisation-mention (parfois appelée distinction mots-comme-mots ) est la distinction entre l' utilisation d' un mot (ou d'une phrase) et sa mention . Habituellement, il est indiqué qu'une expression est mentionnée plutôt qu'utilisée en la mettant entre guillemets, en l'imprimant en italique ou en définissant l'expression seule sur une ligne. La mise entre guillemets d'une expression nous donne le nom d'une expression, par exemple :
- 'Metalogic' est le nom de cet article.
- Cet article concerne la métalogique.
Type–jeton
La distinction type-token est une distinction en métalogique, qui sépare un concept abstrait des objets qui sont des instances particulières du concept. Par exemple, le vélo particulier dans votre garage est un jeton du type de chose connu sous le nom de « le vélo ». Alors que le vélo dans votre garage est dans un endroit particulier à un moment particulier, ce n'est pas le cas de "le vélo" tel qu'il est utilisé dans la phrase : " Le vélo est devenu plus populaire récemment". Cette distinction est utilisée pour clarifier le sens des symboles des langages formels .
Histoire
Des questions métalogiques ont été posées depuis l'époque d' Aristote . Cependant, ce n'est qu'avec l'essor des langages formels à la fin du XIXe et au début du XXe siècle que les recherches sur les fondements de la logique ont commencé à fleurir. En 1904, David Hilbert a observé qu'en étudiant les fondements des mathématiques , les notions logiques sont présupposées, et donc un compte rendu simultané des principes métalogiques et métamathématiques était nécessaire. Aujourd'hui, métalogique et métamathématiques sont largement synonymes l'un de l'autre, et les deux ont été substantiellement subsumés par la logique mathématique dans le milieu universitaire. Un modèle alternatif possible, moins mathématique, peut être trouvé dans les écrits de Charles Sanders Peirce et d'autres sémioticiens .
Résultats
Les résultats en métalogique consistent en des choses telles que des preuves formelles démontrant la cohérence , l' exhaustivité et la décidabilité de systèmes formels particuliers .
Les principaux résultats en métalogique comprennent :
- Preuve de l' indénombrable de l' ensemble de puissance des nombres naturels ( théorème de Cantor 1891)
- Théorème de Löwenheim-Skolem ( Leopold Löwenheim 1915 et Thoralf Skolem 1919)
- Preuve de la cohérence de la logique propositionnelle vérité-fonctionnelle ( Emil Post 1920)
- Preuve de la complétude sémantique de la logique propositionnelle vérité-fonctionnelle ( Paul Bernays 1918), (Emil Post 1920)
- Preuve de la complétude syntaxique de la logique propositionnelle vérité-fonctionnelle (Emil Post 1920)
- Preuve de la décidabilité de la logique propositionnelle vérité-fonctionnelle (Emil Post 1920)
- Preuve de la cohérence de la logique des prédicats monadiques du premier ordre ( Leopold Löwenheim 1915)
- Preuve de la complétude sémantique de la logique des prédicats monadiques du premier ordre (Leopold Löwenheim 1915)
- Preuve de la décidabilité de la logique des prédicats monadiques du premier ordre (Leopold Löwenheim 1915)
- Preuve de la cohérence de la logique des prédicats du premier ordre ( David Hilbert et Wilhelm Ackermann 1928)
- Preuve de la complétude sémantique de la logique des prédicats du premier ordre ( théorème de complétude de Gödel 1930)
- Preuve du théorème d'élimination des coupures pour le calcul des séquences ( Gentzen 's Hauptsatz 1934)
- Preuve de l'indécidabilité de la logique des prédicats du premier ordre ( théorème de Church 1936)
- Le premier théorème d'incomplétude de Gödel 1931
- Deuxième théorème d'incomplétude de Gödel 1931
- Le théorème d'indéfinissabilité de Tarski (Gödel et Tarski dans les années 1930)
Voir également
Les références
- ^ Harry Gensler, Introduction à la logique , Routledge, 2001, p. 336.
- ^ A b c d e Hunter, Geoffrey , Metalogic: Introduction à la Métatheorie de la norme du premier ordre logique , University of California Press, 1973
- ^ un b Rudolf Carnap (1958) Introduction à la logique symbolique et ses applications , p. 102.
- ^ Hao Wang, Réflexions sur Kurt Gödel
Liens externes
- Médias liés à Metalogic sur Wikimedia Commons
- Dragalin, AG (2001) [1994], "Méta-logique" , Encyclopédie des mathématiques , EMS Press