1.11. Quantificateurs universels du second ordre

La logique du premier ordre autorisera l'utilisation de symboles de structures variables comme abréviations d'expressions fixes définissant ces structures, mais ainsi ne peut les lier que sur certains domaines restreints respectivement déterminés par ces expressions (voir 1.B).
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. Cela peut être conçu soit comme l'ensemble de toutes les expressions définissables (avec toutes les expressions de définition possibles, dont les variables libres peuvent inclure toute liste de paramètres au-delà des arguments donnés), soit comme leur ensemble complet (de toutes les opérations de ce type existant dans l'univers, reliant les types interprétés donnés). 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é puis pour la théorie des ensembles (en 2.1 et 2.2), une théorie peut d’abord être 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. (Les règles de preuve ci-dessous visent seulement à être correctes, la logique du second ordre n'admettant aucune théorie de la démonstration correcte et complète).
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 du 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 du 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 du second ordre après l’introduction universelle du 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.

Un nouveau symbole liant B utilisable en logique du premier ordre, peut être défini via la logique du second ordre, par une expression abrégée ici par F(A) car utilisant le symbole variable A de la structure unaire dont l'argument sera lié par B:

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

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, il définit (Bx, A(x)) comme un symbole de structure, par l'expression F(A) dont les variables libres disponibles sont les paramètres de F plus ceux de A.

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 à entendre comme un schéma d'axiomes par élimination universelle du second ordre du prédicat unaire variable A:
  1. x, x = x (réflexivité)
  2. A,∀x,∀y, (x = yA(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 cas utilisant uniquement d'autres variables libres a, b, 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 = yy = x
4. ∀x, ∀y, ∀z, (x = yy = z) ⇒ x = z
5. ∀f, ∀x, ∀y, x = yf(x) = f(y)
6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x, ∀y, ∀z, (x = yz = y) ⇒ z = x
Nom
Symétrie
Transitivité
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.
La formule (x = yy = z) sera abrégée en x = y = z.
Remarque. (1.∧7.) ⇒ 3., puis 3. ⇒ (4. ⇔ 7) donc (1.∧7.) ⇔ (1.∧3.∧4.).

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).
L'introduction d'une variable x définie par un terme t en écrivant (x = t ⇒ ...), autrement dit en posant l'axiome x = t, peut être considérée comme justifiée par les règles ainsi:

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

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. 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