-
Notifications
You must be signed in to change notification settings - Fork 2
/
Bourbaki.tex
171 lines (146 loc) · 7.44 KB
/
Bourbaki.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
\documentclass{article}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\newcommand{\C}{\mathcal{C}}
\newcommand{\Pp}{\mathcal{P}^+}
\newcommand{\Pm}{\mathcal{P}^-}
\begin{document}
\noindent
Bourbaki, \emph{Livre I Th\'eorie des ensembles Chap.IV (\'etat 7?)
Structures}, p. 2--6.
\url{http://sites.mathdoc.fr/archives-bourbaki/PDF/180_nbr_083.pdf}
\section*{Echelons.}
Nous nous proposons, dans ce chapitre, de d\'ecrire une fois pour
toutes, et d'une fa{\c c}on aussi g\'en\'erale que possible, un
certain nombre de constructions formatives et de d\'emonstrations, que
interviennent constamment dans toutes les th\'eories math\'ematiques.
Les crit\'eres que nous obtiendrons, comme ceux du chap.I, serviront
\`a abr\'eger notablement les raisonnements du type envisag\'e, et
fourniront en outre un principe de classification pour les diverses
th\'eories math\'ematiques usuelles.
Bien entendu, la justification de ces crit\`eres appartient \`a la
m\'etamath\'ematique.
Pour la description que nous avons en vue, il nous sera commode
d'introduire des assemblages que \emph{ne sont pas} des termes ou
relations de th\'eories math\'ematiques. Consid\'erons, d'une part,
des lettres distinctes $x_1, x_2, \dots, x_n$, et d'autre part trois
nouveaux signes $\Pp$, $\Pm$ et $X$.
Une \emph{construction d'\'echelons sur les lettres} $x_1, \dots, x_n$
est une suite d'assemblages form\'es avec ces lettres et les trois
signes pr\'ec\'edents, chacun de ces assemblages \'etant appel\'e,
soit \emph{\'echelon covariant}, soit \emph{\'echelon contravariant}
(sur les lettres $x_1, \dots, x_n$), de sorte que, pour chaque
assemblage $A$ de la suite, l'une des conditions suivantes soit
v\'erifi\'ee:
\begin{enumerate}
\item[a)] $A$ est une des lettres $x_1, \dots, x_n$, et est alors covariant.
\item[b)] Il y a dans la suite un assemblage $B$ pr\'ec\'edant $A$ et
tel que $A$ soit $\Pp B$ (resp. $\Pm B$); si $B$ est contravariant,
$A$ est contravariant (resp. covariant); si $B$ est covariant, $A$
est covariant (resp. contra-variant).
\item[c)] Il y a dans la suite deux assemblages $B$, $C$ pr\'ec\'edant
$A$, \emph{tous deux} contravariants ou \emph{tous deux} covariants,
tels que $A$ soit $X B C$; si $B$ et $C$ sont tous deux
contravariants (resp. covariants) $A$ est contravariant (resp
covariant).
\end{enumerate}
La m\'ethode d\'evelopp\'ee dans l'Appendice du chap.I premet de
reconnaitre si un assemblage donn\'e des lettres $x_1, \dots, x_n$ et
des trois signes $\Pp$, $\Pm$ et $X$, est ou non un \'echelon et s'il
est contravariant ou covariant.
Il est imm\'ediat que tout \'echelon sur \emph{certaines} des lettres
$x_1, \dots, x_n$ et aussi un \'echelon sur $x_1, \dots, x_n$.
\section*{Esp\`eces de structures et structures.}
On dit qu'on a d\'efini dans une th\'eorie $\C$ plus forte que la
th\'eorie des ensembles une \emph{esp\`ece de structure}, lorsqu'on
s'est donn\'e:
\begin{enumerate}
\item Un certain nombre de lettres distinctes $x_1, \dots, x_n, s_1,
\dots, s_p$ autres que les constantes de $\C$.
\item Des \'echelons $T_1, T_2, \dots, T_p$ d'une construction
d'\'echelons (1) sur les $n$ lettres $x_1, \dots, x_n$, en nombre
\'egal \`a celui des lettres $s_j$, distincts ou non.
\item Une relation $R\{x_1, \dots, x_n, s_1, \dots, s_p\}$ de la
th\'eorie $\C$, de la forme
\begin{multline*}
s_1 \subset T_1(x_1, \dots, x_n) \text{ et } s_2 \subset T_2(x_1,
\dots, x_n) \text{ et \dots et } \\
s_p \subset T_p(x_1, \dots, x_n) \text{ et } R'\{x_1, \dots, x_n,
s_1, \dots, s_p\}
\end{multline*}
de fa{\c c}on que la relation suivante soit un th\'eor\`eme de $\C$:
(IS) $(R\{x_1, \dots, x_n, s_1, \dots, s_p\}$ et $f_1$ est une
bijection de $x_1$ sur $y_1$ et \dots et $f_n$ est une bijection de
$x_n$ sur $y_n) \implies R\{y_1, \dots, y_n, s_1', \dots s_p'\}$ ou
$y_1, \dots, y_n$ sont des lettres distinctes des constantes de $\C$
et de toutes les lettres figurant dans $R\{x_1, \dots, x_n, s_1,
\dots, s_p\}$, et ou on a pos\'e \[ s_j' = T_j\langle f_1, \dots,
f_n\rangle \langle s_j \rangle \] pour $1 \leq j \leq p$.
\end{enumerate}
La d\'efinition des termes $T_j\langle f_1, \dots, f_n\rangle$ se fait
bien entendu dahs la th\'eorie obtenue en adjoignant \`a $\C$, d'une
part l'axiome ``$f_1$ est une bijection de $x_1$ sur $y_1$ et \dots et
$f_n$ est une bijection de $x_n$ sur $y_n$'', et d'autre part l'axiome
``$s_1 \subset T_1(x_1, \dots, x_n)$ et \dots et $s_p \subset T_p(x_1,
\dots, x_n)$''.
\section*{Echelons.}
We propose, in this chapter, to describe once and for all, and as
generally as possible, a certain number of formative constructions and
proofs, that constantly intervene in all mathematical theories. The
criteria we obtain, such as in chap.I, will be used to notably shorten
the reasoning of the type envisaged, and also provide a classification
principle for various usual mathematical theories.
Of course, the justification for these criteria belongs to
metamathematics.
For the description we have in mind, it will be convenient to
introduce assemblies that \emph{are not} terms or relations of
mathematical theories. Consider, first, the distinct letters $x_1,
x_2, \dots, x_n$, and on the other hand three new symbols $\Pp$, $\Pm$,
and $X$.
An \emph{echelon construction on the letters} $x_1, \dots, x_n$ is a
sequence of assemblies formed with the letters and the three preceding
symbols, each of the assemblies being called either a \emph{covariant
echelon} or a \emph{contravariant echelon} (on the letters $x_1,
\dots, x_n$), so that, for each assembly $A$ in the sequence, one of
the following conditions holds:
\begin{enumerate}
\item[a)] $A$ is one of the letters $x_1, \dots, x_n$ and is covariant.
\item[b)] There is in the sequence an assembly $B$ preceding $A$ such
that $A$ is $\Pp B$ (resp. $\Pm B$); if $B$ is contravariant,
$A$ is contravariant (resp. covariant); if $B$ is covariant, $A$
is covariant (resp. contravariant).
\item[c)] There is in the sequence two assembies $B$, $C$ preceding
$A$, both contravariant or both covariant, such that $A$ is $XBC$;
if $B$ and $C$ are both contravariant (resp. covariant) $A$ is
contravariant (resp. covariant).
\end{enumerate}
\section*{Species of structures and structures.}
We say that we have defined, in a theory
$\C$ at least as strong as set theory, a \emph{species of structure}
when we have:
\begin{enumerate}
\item A certain number of distinct variables $x_1, \dots, x_n, s_1,
\dots, s_p$ besides the constants of $\C$.
\item The \emph{echelons} $T_1, T_2, \dots, T_p$ of an \emph{echelon
construction} on $n$ letters $x_1, \dots, x_n$, equal in number to
the letters $s_j$, distinct or not.
\item A relation $R\{x_1, \dots, x_n, s_1, \dots, s_p\}$ of the theory
$\C$, of the form
\begin{multline*}
s_1 \subset T_1(x_1, \dots, x_n) \text{ and } s_2 \subset T_2(x_1,
\dots, x_n) \text{ and \dots and } \\
s_p \subset T_p(x_1, \dots, x_n) \text{ and } R'\{x_1, \dots, x_n,
s_1, \dots, s_p\}
\end{multline*}
so that the following relationship is a theorem of $\C$:
(IS) $(R\{x_1, \dots, x_n, s_1, \dots, s_p\}$ and $f_1$ is a
bijection of $x_1$ onto $y_1$ and \dots and $f_n$ is a bijection of
$x_n$ onto $y_n) \implies R\{y_1, \dots, y_n, s_1', \dots s_p'\}$, where
$y_1, \dots, y_n$ are variables distinct from the constants of $\C$
and from all the variables appearing in $R\{x_1, \dots, x_n, s_1,
\dots, s_p\}$, and where we set \[ s_j' = T_j\langle f_1, \dots,
f_n\rangle \langle s_j \rangle \] for $1 \leq j \leq p$.
\end{enumerate}
\end{document}