Schéma d'axiomes

Un schéma d’axiomes est une formule exprimée dans le métalangage d'un système axiomatique dans laquelle apparaît au moins une métavariable. Ces variables, qui sont des constructions métalinguistiques, représentent n'importe quel terme ou sous-formule du système logique, qui peut être (ou ne pas être) tenu de satisfaire certaines conditions. Souvent, de telles conditions exigent que certaines des variables soient libres, ou que certaines variables n'apparaissent pas dans la sous-formule ou le terme.

La quantité de sous-formules possibles ou terme qui peuvent donner leur valeur à une métavariable étant infinie dénombrable, un schéma d’axiome représente en général un ensemble infini dénombrable d'axiomes. Cet ensemble peut généralement être défini de manière récursive. Une théorie qui peut être axiomatisée sans schéma est dite finiment axiomatisable. Ces dernières sont considérées méta-mathematiquement comme plus élégantes, même si elles sont moins pratiques pour un travail déductif.^{[réf. nécessaire]}

Les schémas d’axiomes suivants sont d'usage fréquent :

• le schéma d'induction, qui fait partie des axiomes de Peano pour l'arithmétique des nombres naturels ;
• le schéma d’axiomes de remplacement, qui fait partie de l'axiomatisation standard ZFC de la théorie des ensembles.

Il a été prouvé (d'abord par Richard Montague) que ces schémas ne peuvent pas être éliminés. L'arithmétique de Peano et de ZFC ne sont donc pas finiment axiomatisables. C'est également le cas pour bien d'autres théories axiomatiques en mathématiques, linguistique, etc.

Tous les théorèmes de la ZFC sont également des théorèmes de la théorie des ensembles de von Neumann-Bernays-Gödel, mais cette dernière est, paradoxalement, finiment axiomatisée. La théorie des Nouvelles Fondations est, elle aussi, finiment axiomatisable, mais seulement avec une certaine perte d’élégance.