Metalogic , l'étude et l'analyse de la sémantique (relations entre expressions et significations) et syntaxe (relations entre expressions) des langages formels et des systèmes formels. Il est lié, mais n'inclut pas, le traitement formel des langues naturelles. (Pour une discussion sur la syntaxe et la sémantique des langages naturels, voir linguistique et sémantique.)
Nature, origines et influences de la métalogique
Syntaxe et sémantique
Un langage formel nécessite généralement un ensemble de règles de formation, c'est-à-dire une spécification complète des types d'expressions qui compteront comme des formules bien formées (phrases ou expressions significatives), applicables mécaniquement, dans le sens où une machine pourrait vérifier si un candidat répond aux exigences. Cette spécification contient généralement trois parties: (1) une liste de symboles primitifs (unités de base) donnés mécaniquement, (2) certaines combinaisons de ces symboles, distinguées mécaniquement comme formant les phrases simples (atomiques), et (3) un ensemble de clauses inductives - inductives dans la mesure où elles stipulent que des combinaisons naturelles de phrases données formées par des connecteurs logiques tels que la disjonction «ou», qui est symbolisée par «∨»; «Non», symbolisé «∼»; et «pour tous», symbolisé «(∀)», sont à nouveau des phrases. [«(∀)» est appelé un quantificateur,comme aussi «il y en a», symbolisé «(∃)».] Puisque ces spécifications ne concernent que les symboles et leurs combinaisons et non les significations, elles n'impliquent que la syntaxe du langage.
Une interprétation d'un langage formel est déterminée en formulant une interprétation des phrases atomiques du langage par rapport à un domaine d'objets - c'est-à-dire en stipulant quels objets du domaine sont désignés par quelles constantes du langage et quelles relations et fonctions sont dénoté par quelles lettres de prédicat et symboles de fonction. La valeur de vérité (qu'elle soit «vraie» ou «fausse») de chaque phrase est ainsi déterminée selon l'interprétation standard des connecteurs logiques. Par exemple, p · q est vrai si et seulement si p et qsont vrai. (Ici, le point signifie la conjonction «et» et non l'opération de multiplication «temps».) Ainsi, étant donné toute interprétation d'un langage formel, un concept formel de vérité est obtenu. La vérité, le sens et la dénotation sont des concepts sémantiques.
Si, en plus, un système formel dans un langage formel est introduit, certains concepts syntaxiques apparaissent, à savoir les axiomes, les règles d'inférence et les théorèmes. Certaines phrases sont désignées comme axiomes. Ce sont des théorèmes (de base). Chaque règle d'inférence est une clause inductive, indiquant que, si certaines phrases sont des théorèmes, alors une autre phrase qui leur est liée de manière appropriée est également un théorème. Si p et «soit non- p soit q » (∼ p ∨ q ) sont des théorèmes, par exemple, alors q est un théorème. En général, un théorème est soit un axiome, soit la conclusion d'une règle d'inférence dont les prémisses sont des théorèmes.
En 1931, Kurt Gödel a fait la découverte fondamentale que, dans la plupart des systèmes formels intéressants (ou significatifs), toutes les phrases vraies ne sont pas des théorèmes. Il résulte de cette constatation que la sémantique ne peut être réduite à la syntaxe; ainsi la syntaxe, qui est étroitement liée à la théorie de la preuve, doit souvent être distinguée de la sémantique, qui est étroitement liée à la théorie des modèles. En gros, la syntaxe - telle qu'elle est conçue dans la philosophie des mathématiques - est une branche de la théorie des nombres, et la sémantique est une branche de la théorie des ensembles, qui traite de la nature et des relations des agrégats.
Historiquement, au fur et à mesure que les systèmes logiques et axiomatiques devenaient de plus en plus précis, il est apparu, en réponse à un désir de plus grande lucidité, une tendance à accorder plus d'attention aux caractéristiques syntaxiques des langages employés plutôt qu'à se concentrer exclusivement sur les significations intuitives. De cette manière, la logique, la méthode axiomatique (telle que celle employée en géométrie), et la sémiotique (la science générale des signes) ont convergé vers la métalogique.
La méthode axiomatique
Le système axiomatique le plus connu est celui d'Euclid pour la géométrie. D'une manière similaire à celle d'Euclide, chaque théorie scientifique implique un ensemble de concepts significatifs et une collection d'assertions vraies ou croyantes. La signification d'un concept peut souvent être expliquée ou définie en termes d'autres concepts et, de même, la véracité d'une assertion ou la raison de la croire peut généralement être clarifiée en indiquant qu'elle peut être déduite de certaines autres assertions déjà acceptées. La méthode axiomatique se déroule en une séquence d'étapes, en commençant par un ensemble de concepts et de propositions primitifs, puis en définissant ou en déduisant tous les autres concepts et propositions de la théorie.
La prise de conscience qui a surgi au 19ème siècle qu'il existe différentes géométries possibles a conduit à un désir de séparer les mathématiques abstraites de l'intuition spatiale; en conséquence, de nombreux axiomes cachés ont été découverts dans la géométrie d'Euclide. Ces découvertes ont été organisées en un système axiomatique plus rigoureux par David Hilbert dans son Grundlagen der Geometrie (1899; The Foundations of Geometry ). Dans ce système et dans les systèmes connexes, cependant, les connecteurs logiques et leurs propriétés sont tenus pour acquis et restent implicites. Si la logique impliquée est considérée comme celle du calcul des prédicats, le logicien peut alors arriver à des systèmes formels tels que ceux décrits ci-dessus.
Une fois ces systèmes formels obtenus, il est possible de transformer certains problèmes sémantiques en problèmes syntaxiques plus précis. On a affirmé, par exemple, que les géométries non euclidiennes doivent être des systèmes auto-cohérents parce qu'elles ont des modèles (ou interprétations) en géométrie euclidienne, qui à son tour a un modèle dans la théorie des nombres réels. On peut alors se demander comment on sait que la théorie des nombres réels est cohérente en ce sens qu'aucune contradiction ne peut être dérivée en son sein. Évidemment, la modélisation ne peut établir qu'une cohérence relative et doit s'arrêter quelque part. Arrivé à un système formel (disons de nombres réels), cependant, le problème de cohérence a alors le focus plus net d'un problème syntaxique:celui de considérer toutes les preuves possibles (comme des objets syntaxiques) et de se demander si l'une d'elles a jamais (disons) 0 = 1 comme dernière phrase.
Comme autre exemple, la question de savoir si un système est catégorique - c'est-à-dire s'il détermine essentiellement une interprétation unique en ce sens que deux interprétations quelconques sont isomorphes - peut être explorée. Cette question sémantique peut dans une certaine mesure être remplacée par une question syntaxique connexe, celle de l'exhaustivité: s'il y a dans le système une phrase ayant une valeur de vérité définie dans l'interprétation voulue de telle sorte que ni cette phrase ni sa négation ne soient un théorème. Même si l'on sait maintenant que les concepts sémantique et syntaxique sont différents, l'exigence vague qu'un système soit «adéquat» est clarifiée par les deux concepts. L'étude de questions syntaxiques aussi pointues que celles de la cohérence et de l'exhaustivité, qui a été soulignée par Hilbert, a été nommée «métamathématique» (ou «théorie de la preuve») par lui vers 1920.
