Métathéorie

Une métathéorie, ou méta-théorie, est une théorie dont l'objet est une théorie, comme cela est illustré par la citation de Stephen Hawking^[1] :

« Les études méta-théoriques font généralement partie de la philosophie des sciences. De plus, une métathéorie est un objet de préoccupation pour la zone dans laquelle la théorie individuelle est conçue. »

En logique mathématique

Dans un sens plus restreint et spécifique, en logique mathématique, une métathéorie est une théorie mathématique qui a pour objet une autre théorie mathématique. Le paradoxe de Richard a pour origine la confusion entre la théorie (la théorie des ensembles en l'occurrence) et la métathéorie à un moment où cette distinction n'était pas claire en logique mathématique.

En mathématiques

Le concept de métathéorie émerge au XX^e siècle à la suite des travaux du mathématicien allemand David Hilbert qui, en 1905, a publié^[2] un programme de recherche visant à démontrer la cohérence et la complétude des mathématiques, créant ainsi le domaine de la métamathématique. Kurt Gödel, a montré en 1931 que ce programme est irréalisable (voir Théorèmes d'incomplétude de Gödel). Depuis le terme de métamathématique est moins utilisé.

En informatique

En général les concepts d'un langage de programmation comme sa grammaire, sa traduction, sa compilation font partie de la métathéorie du langage. Cependant certains langages de programmation permettent d'intégrer ces concepts dans le langage lui-même, autrement dit d'intégrer la métathéorie dans le langage. Dans ce cas, on parle de réflexion. D'ailleurs, la réflexion est un concept connu des linguistes, car une langue naturelle permet de parler d'elle-même.

Les systèmes de preuve interactive (ainsi Coq) sont réflexifs. Sans la réflexion, la démonstration mécanisée du théorème de Feit-Thompson n'aurait pas été possible.