Métathéorème - Metatheorem
En logique , un métathéorème est une déclaration sur un système formel éprouvé dans un métalangage . Contrairement aux théorèmes prouvés dans un système formel donné, un métathéorème est prouvé dans une métathéorie , et peut faire référence à des concepts qui sont présents dans la métathéorie mais pas dans la théorie des objets .
Un système formel est déterminé par un langage formel et un système déductif ( axiomes et règles d'inférence ). Le système formel peut être utilisé pour prouver des phrases particulières du langage formel avec ce système. Les métathéorèmes, cependant, sont prouvés à l'extérieur du système en question, dans sa métathéorie. Les métathéories courantes utilisées en logique sont la théorie des ensembles (en particulier en théorie des modèles ) et l'arithmétique récursive primitive (en particulier en théorie de la preuve ). Plutôt que de démontrer que des phrases particulières sont prouvables, les métathéorèmes peuvent montrer que chacune d'une large classe de phrases peut être prouvée, ou montrer que certaines phrases ne peuvent pas être prouvées.
Exemples
Des exemples de métathéorèmes comprennent:
- Le théorème de la déduction pour la logique du premier ordre dit qu'une phrase de la forme φ → ψ est prouvable à partir d' un ensemble d'axiomes A si et seulement si la ψ phrase est prouvable du système dont les axiomes se composent de φ et tous les axiomes de A .
- Le théorème d'existence de classe de la théorie des ensembles de von Neumann – Bernays – Gödel stipule que pour toute formule dont les quantificateurs ne s'étendent que sur des ensembles, il existe une classe constituée des ensembles satisfaisant la formule.
- Preuves de cohérence de systèmes tels que l'arithmétique Peano .
Voir également
Les références
- Geoffrey Hunter (1969), Metalogic .
- Alasdair Urquhart (2002), «Metatheory», Un compagnon de la logique philosophique , Dale Jacquette (éd.), P. 307
Liens externes
- Méta-théorème à l'Encyclopaedia of Mathematics
- Barile, Margherita. "Metatheorem" . MathWorld .