Schéma d'axiomes

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

En logique mathématique, un schéma d’axiomes généralise la notion d'axiome.

Définition formelle[modifier | modifier le code]

Un schéma d’axiomes est une formule exprimée dans le métalangage d'un système axiomatique, dans lequel une ou plusieurs métavariables apparaissent. 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.

Axiomatisation finie[modifier | modifier le code]

La quantité de sous-formules possibles ou terme qui peuvent donner leur valeur à une métavariable est infinie dénombrable, un schéma d’axiome représente par conséquent 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 plus élégantes, même si elles sont moins pratiques pour un travail déductif.[réf. nécessaire]

Exemples[modifier | modifier le code]

Deux exemples très bien connus de schémas d’axiomes sont les suivants :

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 axiomatiques des théories des mathématiques, de la philosophie, de la linguistique, etc.

Théories finiment axiomatisables[modifier | modifier le code]

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

Dans les logiques d’ordres supérieurs[modifier | modifier le code]

Les métavariables de logique du premier ordre sont généralement trivialement éliminables en logique d’ordre supérieur, car une métavariable est souvent un espace dédié à toute propriété ou relation sur les éléments de la théorie. C'est le cas des schémas d'Induction et de Remplacement mentionnés ci-dessus. La logique d’ordre supérieur permet aux variables quantifiées d’avoir pour domaine l'ensemble des propriétés ou des relations.

Voir aussi[modifier | modifier le code]

Notes et références[modifier | modifier le code]

  • Entrée « Schéma » dans la Stanford Encyclopedia of Philosophy
  • Corcoran, J. 2006. Schémas: le Concept de Schéma dans l'Histoire de la Logique. Bulletin de la Logique Symbolique 12: 219-40.
  • Mendelson, Elliot, 1997. Introduction à la Logique Mathématique, 4e ed. Chapman & Hall.
  • Potter, Michael, 2004. La Théorie des ensembles et de sa Philosophie. Oxford Univ. Appuyez sur la touche.
  • (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Axiom schema » (voir la liste des auteurs).