Quantificateurs du second ordre

1.11. Quantificateurs universels du second ordre

La logique du premier ordre peut être développée pour autoriser l'utilisation de symboles de structures variables comme abréviations d'expressions fixes définissant ces structures avec paramètres variables, mais ainsi ne peut les lier que sur des domaines restreints dépendant des expressions choisies (plus de commentaires en 1.D).
Appelons quantificateur du second ordre, un quantificateur liant un symbole de structure variable sur l'ensemble de toutes les structures de son type de symbole. Ceci peut être conçu soit comme l'ensemble de toutes les expressions définissables (par toutes les expressions avec n'importe quel nombre de paramètres), soit comme l'ensemble complet de toutes ces opérations (reliant les types interprétés donnés) qui existent... dans l'univers. Utiliser des quantificateurs du second ordre signifie travailler dans un cadre logique élargi, notamment une version de la logique de second ordre (décrite dans la partie 5), suivant les détails.

Comme on fera pour les axiomes de l’égalité (ci-dessous) puis pour la théorie des ensembles (en 2.1 et 2.2), une théorie peut être d’abord exprimée en logique du second ordre pour des raisons intuitives, avant d’interpréter cela formellement comme un outil commode de niveau méta pour abréger une formalisation du premier ordre, comme suit.

Soit T une théorie du premier ordre, T' son extension par un symbole de structure s (sans axiome supplémentaire) et F un énoncé de T' (en logique du premier ordre) également noté F(s) lorsque vu comme une formule de T utilisant le symbole de structure variable s en logique du second ordre.

Introduction universelle de second ordre. Si T'⊢F alors T implique l'énoncé du second ordre (∀s, F(s)).

Ceci est valable pour tout modèle et le domaine ensembliste complet de s, indépendamment de l'univers dans lequel les modèles et les structures s sont recherchés.

Élimination universelle de second ordre. Une fois accepté un énoncé de second ordre (∀s, F(s)) dans une théorie T, il se manifeste en logique du premier ordre sous la forme d'un schéma d'énoncés (axiomes ou théorèmes), c'est-à-dire une liste infinie d'énoncés de la forme (∀parameters, F(s)) pour chaque remplacement possible de s par une expression définissante avec des paramètres.

Appliquer l’élimination universelle de second ordre après l’introduction universelle de second ordre signifie déduire de T un schéma de théorèmes, chacun déductible en logique du premier ordre en remplaçant s par sa définition respective dans la preuve originale.

Incomplétude de la logique du second ordre

Les règles de preuve ci-dessus, qui suffiront à nos besoins, sont clairement correctes, mais contrairement à la logique du premier ordre, la logique du second ordre n'admet aucune théorie de la démonstration correcte et complète. Dans ce qui précède, la seule règle de preuve complète est que l'élimination universelle de second ordre formalise complètement les conséquences de ∀ entendu comme portant sur les seules structures définissables. Aucune règle ne peut épuiser les conséquences de l'application de ∀ au domaine de "toutes les structures" (y compris celles indéfinissables) pour la raison suivante dont les détails seront développés ultérieurement.

Une théorie est dite complète si elle détermine essentiellement son modèle. La définition exacte est que tous les modèles sont isomorphes entre eux (3.3); retenons-en qu'elle détermine toutes les propriétés de son modèle (valeurs des énoncés du premier ordre) et exclut les modèles non standard.
L'arithmétique (la théorie décrivant le système ℕ des entiers naturels avec quatre symboles 0, 1, +, ⋅) peut être formalisée comme théorie complète en logique du second ordre (axiomes listés en 4.4 et 4.5). La seule composante de cette formalisation au-delà de la logique du premier ordre est l'axiome d'induction, utilisant un ∀ s'étendant sur "tous les prédicats unaires" (y compris ceux indéfinissables). Cependant, le théorème d'incomplétude (1.C) réfutera la possibilité pour tout algorithme de donner les valeurs correctes de tous les énoncés arithmétiques du premier ordre.

Mais l'ensemble des seules structures définissables d'un type donné ne peut pas non plus être complètement défini pour la même raison, car décrire l'ensemble infini exact de toutes les expressions de définitions possibles revient à décrire ℕ.

Axiomes de l'égalité

En logique du premier ordre avec des types et un langage donnés, certains énoncés utilisant = sont valides (toujours vrais) pour le domaine d'interprétations conservant = en tant que prédicat = de la théorie des ensembles, mais non plus pour le domaine plus large d'interprétations l'interprétant comme tout autre prédicat. Une liste possible d'axiomes de l'égalité est une liste de certains de ces énoncés qui suffisent à impliquer tous les autres dans ce contexte.
Une de ces listes comprend les 2 axiomes suivants par type, le dernier étant à lire comme un schéma d'axiomes par élimination universelle de second ordre du prédicat unaire variable A:

∀x, x = x (réflexivité)
∀A,∀x,y, (x = y ∧ A(y)) ⇒ A(x).

Les variables x et y peuvent également servir parmi les paramètres de la définition de A. Ceci peut être compris en réordonnant les quantificateurs en (∀x, ∀y, ∀A), ou comme déduit de l'usage d'un A de paramètres a, b, en adaptant un énoncé logiquement valide de 1.10 :

∀a,b, (∀x,y, R(a, b, x,y)) ⇒ R(a, b, a,b)

Diverses définitions de A donnent divers énoncés (en supposant la réflexivité):

Enoncé
3. ∀x,y, x = y ⇒ y = x
4. ∀x,y,z, (x = y ∧ y = z) ⇒ x = z
5. ∀f, ∀x,y, x = y ⇒ f(x) = f(y)
6. ∀A, ∀x,y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x,y,z, (x = y ∧ z = y) ⇒ z = x

Qualité de =
Symétrique
Transitive

Euclidienne à gauche

A(u) utilisé
y = u
u = z
f(u) = f(y)
¬A(u)
z = u

5. est un schéma d'énoncés avec f parcourant les foncteurs entre deux types quelconques.
6. peut aussi se déduire par symétrie.

Remarque. (1.∧7.) ⇒ 3., puis 3. ⇒ (4. ⇔ 7) donc (1.∧7.) ⇔ (1.∧3.∧4.).
La formule (x = y ∧ y = z) sera abrégée en x = y = z.

Une autre liste possible d'axiomes de l'égalité consiste en les énoncés 1. à 5. où f et A parcourent les seuls symboles du langage, pris chacun une fois par argument: le schéma complet de 2. est impliqué par déductions successives pour chaque occurrence de symbole dans A. Ceci sera plus précisément justifié en 2.11 (relations d’équivalence).

Définir de nouveaux symboles liants

Un nouveau symbole de variable libre x défini par un terme t peut être introduit, soit déclarée par une ligne de preuve distincte (x = t) servant d'axiome, soit dans une ligne comme (x = t ⇒ ...). On peut le justifier par les règles comme

(∀x, x = x) ∴ t = t ∴ ∃x, (x = t ∴ ...).

En liant un paramètre, la définition d'un symbole de foncteur f par un terme ici abrégé t de variable x (qui justifiera la notation abrégée de t comme symbole de foncteur), est déclarée par l'axiome

∀x, f(x) = t(x).

De même, les symboles d'opérateur peuvent être définis en liant plusieurs paramètres, et les classes et autres prédicats peuvent être définis de même en remplaçant = par ⇔.
Enfin, un nouveau symbole liant B utilisable dans une théorie du premier ordre T (à savoir en théorie des ensembles formalisée avec sa traduction en théorie du premier ordre) peut être défini par une expression ici abrégée par F(A) car utilisant, au-delà du langage de T, un symbole A de structure unaire variable (dont l'argument sera lié par B). Une telle définition peut être déclarée par cet axiome de second ordre:

∀A, (Bx, A(x)) = F(A)

où = devient ⇔ si les valeurs sont booléennes. Par élimination universelle du second ordre, cela donne un schéma de définitions en logique du premier ordre: pour chaque expression définissant A, l'expression (Bx, A(x)) se définit comme un symbole de structure, par l'expression définissant F(A), obtenue en remplaçant A par sa définition dans l'expression F. Ses variables libres disponibles sont donc les paramètres de F plus ceux de A.

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques 1.1. Introduction au fondement des mathématiques 1.2. Variables, ensembles, fonctions et opérations 1.3. Forme des théories 1.4. Structures mathématiques 1.5. Expressions et structures définissables 1.6. Connecteurs 1.7. Classes en théorie des ensembles 1.8. Symboles liants	1.9. Axiomes et preuves 1.10. Quantificateurs ⇦ 1.11. Quantificateurs du 2e ordre
	Aspects philosophiques ⇨1.A. Temps en théorie des modèles 1.B. Indéfinissabilité de la vérité 1.C. Théorèmes d'incomplétude 1.D. Le cadre ensembliste unifié
2. Théorie des ensembles - 3. Algèbre

Other languages:
EN : 1. First foundations of mathematics : 1.11. Second-order quantifiers