L'étude formelle des propriétés des systèmes logiques considérés comme objets d'étude : leur syntaxe, leur sémantique, les transformations de preuves, la décidabilité, la complétude, la compacité et autres théorèmes métalogiques formulés au niveau des systèmes entiers plutôt qu'au niveau des formules isolées.

Principe

Traiter les calculs logiques comme des objets formels et énoncer des règles et limites générales sur les relations de conséquence, la dérivabilité, la théorie des modèles et les rapports entre caractérisations syntaxiques et sémantiques.

Démonstration

Prouver le théorème de complétude pour la logique du premier ordre (montrer que toute formule valide sémantiquement est dérivable syntaxiquement) et établir l'indécidabilité de la validité en logique du premier ordre constituent des démonstrations métalogiques typiques.

Mauvaise application

Confondre une assertion au niveau objet avec une affirmation métalogique (par exemple interpréter un métathéorème quantifiant sur les théories comme s'il était une preuve à l'intérieur d'une théorie fixe) ou appliquer un résultat modèle-théorique à une dérivation syntaxique sans vérifier la représentabilité.

Conséquence

Éclaire ce qui peut ou ne peut pas être prouvé dans des systèmes donnés, permet le transfert de résultats entre logiques et produit des limites principled (indécidabilité, incomplétude, complétude) qui guident la conception et l'utilisation des systèmes formels.

Inversion

Au lieu de raisonner sur les logiques comme objets, considérer une logique uniquement comme un calcul au niveau objet dont les faits pertinents sont seulement les dérivations de formules individuelles et les évaluations sémantiques dans un modèle fixé.

Limite

Se concentre sur les propriétés formelles des systèmes logiques et exclut les comptes rendus empiriques, psychologiques ou philosophiques informels du raisonnement ; s'applique principalement à des calculs formellement spécifiés et à leurs sémantiques, non à l'argumentation informelle.

Tension sémantique

Une tension apparaît entre approches syntaxiques (théorie des preuves) et sémantiques (théorie des modèles) : certains résultats sont perspectivistes (démontrabilité vs validité) et leur traduction exige des hypothèses de représentation et de correction.

Synthèse

La métalogique unit de manière cohérente l'étude de la syntaxe, de la sémantique et des règles de transformation pour produire des théorèmes généraux sur des systèmes logiques entiers, révélant à la fois des capacités (complétude, décidabilité) et des limites (indécidabilité, incomplétude).