Logique et métalogique
Dans un sens, la logique doit être identifiée avec le calcul des prédicats du premier ordre, le calcul dans lequel les variables sont confinées aux individus d'un domaine fixe - bien qu'elle puisse également inclure la logique de l'identité, symbolisée «=», qui prend les propriétés ordinaires de l'identité dans le cadre de la logique. En ce sens, Gottlob Frege a réalisé un calcul formel de la logique dès 1879. Cependant, la logique est parfois interprétée comme incluant également des calculs de prédicat d'ordre supérieur, qui admettent des variables de types supérieurs, comme celles qui s'étendent sur des prédicats (ou des classes et des relations).) etc. Mais alors c'est un petit pas vers l'inclusion de la théorie des ensembles, et, en fait, la théorie des ensembles axiomatique est souvent considérée comme faisant partie de la logique. Aux fins de cet article, cependant, il est plus approprié de limiter la discussion à la logique au premier sens.
Il est difficile de séparer les découvertes significatives en logique de celles en métalogique, car tous les théorèmes intéressant les logiciens concernent la logique et appartiennent donc à la métalogique. Si p est un théorème mathématique - en particulier, un sur la logique - et P est la conjonction des axiomes mathématiques utilisés pour prouver p, alors chaque p peut être transformé en théorème, "non-P ou p", en logique. Cependant, les mathématiques ne se font pas en effectuant explicitement toutes les étapes formalisées en logique; la sélection et la compréhension intuitive des axiomes sont importantes à la fois pour les mathématiques et pour la métamathématique. Les dérivations réelles de la logique, telles que celles effectuées juste avant la Première Guerre mondiale par Alfred North Whitehead et Bertrand Russell, présentent peu d'intérêt intrinsèque pour les logiciens. Il pourrait donc sembler superflu d'introduire le terme métalogique. Dans la présente classification, cependant, la metalogic est conçue comme traitant non seulement des résultats concernant les calculs logiques, mais aussi des études des systèmes formels et des langages formels en général.
Un système formel ordinaire diffère d'un calcul logique en ce que le système a généralement une interprétation voulue, tandis que le calcul logique laisse délibérément les interprétations possibles ouvertes. Ainsi, on parle, par exemple, de la vérité ou de la fausseté des phrases dans un système formel, mais en ce qui concerne un calcul logique, on parle de validité (c'est-à-dire d'être vrai dans toutes les interprétations ou dans tous les mondes possibles) et de satisfiabilité (ou avoir un modèle, c'est-à-dire être vrai dans une interprétation particulière). Par conséquent, l'exhaustivité d'un calcul logique a une signification tout à fait différente de celle d'un système formel: un calcul logique permet de nombreuses phrases telles que ni la phrase ni sa négation n'est un théorème parce qu'elle est vraie dans certaines interprétations et fausse dans d'autres, et il requiert seulement que chaque phrase valide soit un théorème.
