]> AND Private Git Repository - cours-maths-dis.git/blob - logique/CalculPredicats2.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
relations 13 fini
[cours-maths-dis.git] / logique / CalculPredicats2.tex
1 \section{Introduction}
2
3
4
5 % %\subsection{Insuffisances de la formalisation en calcul
6 % %  propositionnel} 
7
8 % La logique des propositions ne s'occupe que des liens
9 % entre propositions réalisés à l'aide des connecteurs logiques:
10 % %Autrement dit, 
11 % une fois qu'une proposition \og complexe\fg{} a été
12 % analysée suivant ces connecteurs, il subsiste des \og atomes\fg{} (non
13 % sécables en calcul propositionnel) et l'analyse ne peut pas être
14 % poussée plus profondément, alors qu'il existe potentiellement encore des
15 % \og relations\fg{} entre ces atomes.
16
17
18
19  \subsection{Introduction aux \og prédicats\fg{}} 
20
21 En logique des propositions,
22 \og Pierre est le père de Marc\fg{} ne comporte aucun
23 connecteur logique: elle ne peut se formaliser que par une variable 
24 propositionnelle: $A$.
25 La proposition \og Jean est le père de Sylvie\fg{}
26 qui entretient des rapports évidents avec la précédente, elle ne peut être
27 formalisée en logique des propositions que par une
28 variable propositionnelle, $B$. 
29 Après la formalisation, donc, on se retrouve avec deux variables
30 propositionnelles $A$ et $B$, sans lien aucun entre elles, alors qu'il
31 est évident que ces deux propositions évoquent un même lien de parenté
32 entre des individus différents. 
33
34
35
36 Il apparaît primordial 
37 %Ce premier exemple suggère la nécessité, pour poursuivre l'analyse des
38 % propositions, de la création d'
39 de créer 
40 un langage qui permettrait de décrire
41 des propriétés accordées %(ou non) 
42 à des individus: c'est ce à quoi s'intéresse la 
43 \emph{logique des prédicats}. 
44 %Cette préoccupation est aussi celle des mathématiciens, qui
45 %s'occupent, par exemple, de décrire les propriétés des entiers
46 %naturels. 
47
48
49 % Il faudra donc envisager des \og variables\fg{} , dans un certain
50 % domaine, et, pour certaines \og valeurs\fg{} de ces variables,
51 % certaines propriétés seront \og vraies\fg{} ou \og fausses\fg{}. 
52
53  \subsection{Introduction à l'\og univers du discours\fg{}}
54
55 % Soit la proposition \og 7 n'a pas de racine carrée\fg{}.
56 % En calcul propositionnel, elle ne peut être formalisée que par une
57 % variable propositionnelle. 
58 % De plus, il semble même difficile de lui accorder une \og valeur de
59 % vérité\fg{} ; en effet, si l'on se place dans l'ensemble des entiers
60 % naturels, cette proposition est \og vraie\fg{}, alors que si l'on se 
61 % place dans l'ensemble des nombres réels, elle est évidemment fausse. 
62
63 La valeur de l'expression \og $x$ possède une racine carrée \fg{}
64 dépend de $x$ et de l'\emph{univers} dans lequel on fait évoluer 
65 $x$.
66 Cette expression est 
67 \begin{itemize}
68 \item toujours vraie si l'univers du discours est l'ensemble des réels
69   positifs;
70 \item toujours fausse si l'univers du discours est l'ensemble des réels
71   strictement négatifs;
72 \item vraie pour certaines valeurs si l'univers du discours est l'ensemble des 
73   entiers naturels.
74 \end{itemize}
75
76
77
78 % Dans cet exemple, comme dans celui de la section précédente, la
79 % proposition évoque 
80 % une propriété, accordée ou refusée, à un objet bien précis (7).
81 % Bien entendu, la valeur de vérité dépend de la valeur de cet objet,
82 % mais aussi de l'ensemble dans lequel ces valeurs peuvent être
83 % choisies. 
84
85
86 % On pourra envisager de formaliser (partiellement) une telle
87 % proposition par une expression du type \og $x$ a une racine
88 % carrée\fg{}, et la valeur de vérité de la proposition obtenue en \og
89 % donnant à $x$ une valeur\fg{} dépend, non seulement de cette valeur,
90 % mais aussi de l'ensemble dans lequel cette valeur peut être prise. 
91
92
93 % D'une manière générale, et avant de donner une définition précise de
94 % ces 
95 % concepts, on dira qu'une \og propriété\fg{} possédée (ou non) par un objet est un prédicat.
96 % La valeur de vérité de la proposition obtenue en appliquant ce
97 % prédicat à un (ou plusieurs) objets dépend de l'univers du discours,
98 % c'est à dire de l'ensemble des valeurs reconnues comme possibles (par
99 % exemple, dans l'exemple précédent, $\N$ ou $\R$), et aussi, bien
100 % entendu, de cette valeur elle-même. 
101
102
103  \subsection{Introduction à la \og quantification\fg{}}
104
105 Considérons les propositions \og Tous les étudiants sont sérieux\fg{}
106 et \og certains étudiants sont sérieux\fg{}. 
107
108 La généralisation du calcul propositionnel peut paraître encore
109 plus grand que dans les exemples précédents, puisque la propriété
110 évoquée (\og être sérieux\fg{} ) est accordée, par ces propositions,
111 non pas seulement à un individu bien précis, mais à certains
112 individus, considérés dans leur ensemble, ou même à toute une
113 catégorie d'individus, sans qu'aucun ne soit nommément désigné. 
114 Ce troisième exemple suggère la notion de \emph{quantification} d'une
115 variable (tous les\ldots, certains\ldots). 
116
117
118 % L'objet du calcul des prédicats est d'étudier et de formaliser les
119 % notions qui viennent d'être brièvement évoquées, et que le calcul
120 % propositionnel ne permet pas de faire apparaître.
121
122
123
124 %\subsection{Sujets et individus}
125
126 \section{Définitions}
127
128
129
130 \subsection{Termes}
131
132 Le calcul des prédicats fait intervenir des variables, qui prennent
133 des valeurs dans un certain ensemble appelé univers du
134 discours qui par la suite sera souvent noté $U$.
135
136 % Les éléments de cet univers sont appelés \emph{sujets}. Un sujet distingué ou
137 % \emph{individu} est une instance de l'univers du discours qui peut prendre la
138 % place du sujet.
139
140 % \begin{Ex}
141 %  Le symbole 7 est un individu, ou un sujet distingué, dans l'univers
142 %  du discours des entiers naturels. 
143 % \end{Ex}
144
145
146
147 % Il existe deux manières de distinguer un sujet de l'univers du
148 % discours. 
149
150 % \begin{itemize}
151
152 % \item le nommer (donner explicitement son nom, ou le symbole qui le
153 %   représente), comme dans l'exemple précédent, pour l'entier 7. 
154
155 % \item le désigner indirectement par une \og propriété\fg{}
156 %   caractéristique (qu'il doit donc être le seul à posséder, de manière 
157 %   à ce qu'il soit identifié sans aucune ambiguïté). 
158 % Par exemple, si \textit{Pierre} est le père de \textit{Jean}, il est possible de
159 % distinguer \textit{Pierre} sans le nommer explicitement par la locution \og
160 % \textit{le père de Jean}\fg{}. 
161 % \end{itemize}
162
163
164
165 %De manière tout à fait précise :
166 \begin{Def}[Symbole fonctionnel]
167 \index{Symbole fonctionnel}
168 Soit $f$ une fonction du produit d'univers $U_1\times U_2\times\ldots\times U_n$
169 dans $U'$. Le symbole fonctionnel $f$ est dit d'\emph{arité} $n$ et on note $f_n$.
170 \end{Def}
171
172 % \begin{Ex}
173 % Le groupe opératoire à 1 place $\textit{pere}(x)$ désigne sans
174 % ambiguïté un et un seul individu dans l'univers des êtres humains, dès
175 % que la variable $x$ a été remplacée par un sujet distingué. 
176 % Si \textit{Jean} est bien un nom d'individu (c'est à dire, désigne 
177 % bien un individu unique), s'il en est de même de \textit{Pierre}, et 
178 % si \textit{Pierre} est le père de \textit{Jean}, alors 
179 % $\textit{pere}(\textit{Jean})$ distingue l'individu \textit{Pierre}.
180 % \end{Ex}
181
182 Lorsque l'expression $f(x_1, \ldots, x_n)$ ne dépend pas de $x_1,
183 \ldots, x_n$, on peut la remplacer par une constante $c$ de l'univers.
184
185
186
187
188 \begin{Def}[Terme]
189 \noindent 
190 Un \emph{terme} est défini de manière récursive par:
191
192 \begin{itemize}
193
194 \item une variable,
195
196 \item une  constante,
197
198 \item l'expression $f(t_1,t_2,\ldots,t_n)$ si $t_1,t_2,\ldots,t_n$ sont des
199   termes et $f$ un symbole  fonctionnel d'arité $n$  
200 \end{itemize}
201 \end{Def}
202
203
204
205
206
207 \subsection{Prédicats et atomes}
208
209 On cherche à formaliser les relations qui peuvent lier des
210 individus de l'univers du discours. 
211 Par exemple, \og 22 est le double de 11\fg{}, \og 46 est le double de
212 45\fg{} sont 
213 des propositions (vraies ou fausses!) qui évoquent la relation \og
214 être le double de\fg{} . 
215
216
217 \begin{Def}[Symbole prédicatif]
218 Soit $p$ une fonction du produit d'univers $U_1\times U_2\times\ldots\times U_n$
219 dans $\{\textit{vrai},\textit{faux}\}$.
220 Le symbole prédicatif $p$ d'\emph{arité} $n$ (notée $p_n$) est aussi nommé
221 \emph{prédicat $p$}.
222 \end{Def}
223
224 \begin{Def}[Atome]
225 Un atome est de la forme $p(t_1, . . . , t_n)$, où $p$ est un
226 symbole de prédicat d'arité $n$ et $t_1$,\ldots, $t_n$ sont des termes.
227 \end{Def}
228
229
230 \section{Quantificateurs}
231
232 \subsection{Quantificateur universel}
233
234 Considérons la proposition \og Tous les étudiants travaillent les
235 mathématiques\fg{} pour l'analyser du point de vue du calcul 
236 des prédicats.
237 %Aucun connecteur logique n'apparaît. 
238 On peut exprimer ceci à l'aide un prédicat binaire qui peut être formalisé
239 par $\textit{travaille}(x,y)$, et qui signifie qu'un individu $x$ travaille une
240 certaine matière $y$. 
241
242
243 % Il faut préciser l'univers du discours, il s'agit ici d'un ensemble
244 % produit cartésien de deux ensembles : 
245 % \begin{itemize}
246 %  \item le premier est l'ensemble des étudiants,
247 %  \item le second un ensemble de noms de matières (celles qui sont
248 %    susceptibles d'être enseignées). 
249 % \end{itemize}
250  
251 % Il est bien clair qu'il s'agit d'une proposition. Or, si la seconde
252 % variable ($y$) est bien remplacée par un symbole d'individu ($maths$),
253 % aucun nom, explicite ou implicite, n'est donné pour désigner un
254 % étudiant particulier : on a \og $\textit{travaille}(x,maths)$\fg{} sans que
255 % l'on sache \og qui est $x$\fg{} . 
256
257 % Il s'agit d'une construction particulière, qui permet d'obtenir des
258 % propositions à partir de prédicats sans qu'une variable soit
259 % distinguée, et qui porte le nom de quantification : le sujet $x$ n'est
260 % pas distingué, il est \emph{quantifié}. 
261
262
263 La notation utilisée pour cette quantification est \og $\qqs$ \fg{} qui
264 représente un A à l'envers (pour \emph{All}).
265 Ainsi on représente la proposition ci dessus par 
266 $$ \qqs x\, . \, \textit{travaille}(x,\textit{maths}).$$
267
268
269
270 \begin{Def}[Quantificateur universel]
271 $\qqs$ est un symbole de quantificateur, appelé le
272 \emph{quantificateur universel}\index{quantificateur!universel}. On
273 dit alors que $\qqs x$ est le quantificateur universel de la variable
274 $x$. 
275 \end{Def}
276
277 \begin{Rem} La présence du symbole de quantification est indispensable
278   pour donner du sens aux formules avec variables.
279 \begin{itemize}
280 \item $\forall x \, . \, \textit{travaille}(x,\textit{maths})$ est une
281   proposition. La variable $x$ est dite \emph{liée} au quatificateur $\forall$;
282  \item $\textit{travaille}(x,\textit{maths})$ n'est pas une
283 proposition: on ne peut pas lui attribuer une valeur de
284 vérité. Il est nécessaire de substituer $x$ par un terme distinguant
285 un individu pour que cela le devienne 
286 (i.e. 
287 $\textit{travaille}(Jean,\textit{maths})$ ou bien  
288 $\textit{travaille}(\textit{fils}(\textit{Pierre}),\textit{maths})$).
289 Dans cette expression, la
290 variable $x$ est dite \emph{libre}. 
291 \end{itemize}
292 \end{Rem}
293
294 \begin{Exo}
295   Pour chacune des formules $A$ suivantes, 
296   préciser 
297   l'ensemble $\textit{Var}(A)$ des variables de A, 
298   l'ensemble $\textit{Varliees}(A)$ des occurences liées de $\textit{Var}(A)$, 
299   l'ensemble $\textit{Varlibres}(A)$ des occurences libres de $\textit{Var}(A)$.
300 \begin{enumerate}
301 \item  $ A \equiv P (f (x, y)) \lor \forall z\, .\, Q(a, z)$
302 \item  $A \equiv (\forall x \,.\,  P(x, y, z)) \lor (\forall z\,.\, Q(z)
303   \imp R(z))$
304 \item  
305   $A \equiv \forall x\,.\, (\forall y\,.\, P (x, y) \imp \forall z\,.\, 
306   Q(x, y, z))$
307 \end{enumerate}
308 \end{Exo}
309
310
311 \subsection{Quantificateur existentiel}
312
313
314 Dans la proposition \og Tous les étudiants travaillent au moins une 
315 matière\fg{}, intervient le même prédicat binaire 
316 $\textit{travaille}(x,y)$; on remarque qu'aucun étudiant n'est 
317 explicitement nommé, pas plus que la matière qu'il travaille. Si le 
318 \og Tous \fg{} induit une quantification universelle, le \og au moins 
319 une matière \fg{} signifie qu'il existe une matière travaillée par 
320 cet étudiant. Il suffit alors d'introduire le quantificateur 
321 existentiel, représenté par un E (première lettre de \emph{Exists}) retourné
322 ($\exi$).
323
324
325 Cet exemple se traduit alors par  
326 $$\qqs x\, . \, \exi y\, . \, \ \textit{travaille}(x,y)$$
327 où la variable
328 $x$ est liée par le quantificateur universel $\qqs x$ et la variable
329 $y$ est liée par le quantificateur existentiel $\exi y$. 
330
331 % AG : ce ne sont pas des quantificateurs, mais des modalités.
332 % \begin{Rem}
333 % Dans d'autres logiques (modales, temporelles\ldots), on fait
334 % intervenir d'autres symboles de quantificateurs. 
335 % Ces autres logiques se situent en dehors du cadre de notre étude.
336 % \end{Rem}
337
338 \begin{Exo}
339 Formalisez les affirmations suivantes, en utilisant uniquement les
340 prédicats indiqués, les connecteurs logiques et les quantificateurs.
341  \begin{enumerate}
342 \item  Personne n'est parfait ($p(x)$ représente que $x$
343   est parfait)  
344 \item   0 est multiple de chaque nombre entier 
345 ($e(x)$ et $m(x,y)$ signifient respectivement que $x$ est un entier
346 et que $x$ est un multiple de $y$).
347 \item  les absents n'ont pas tous tort 
348 ($a(x)$ et $t(x)$  signifient respectivement que $x$ est absent 
349 et que $x$ a tort)
350 \end{enumerate}
351 % Réponses :
352 % \opt{prof}{
353 %  \begin{enumerate}
354 % \item  $\forall x \,. \, \non p(x)$
355 % \item  $ \forall x \,.\, e(x) \imp m(0,x)$
356 % \item  $\exists x \, . \, a(x) \et \non t(x)$
357 %  \end{enumerate}
358 % }
359 % \opt{etud}{
360 % \vspace{10cm}
361 % } 
362 \end{Exo}
363
364 \begin{Exo}
365 Soit les prédicats 
366 $\textit{curé}(x)$ ($x$ est un curé),
367 $\textit{vélo}(y)$ ($y$ est un vélo) et 
368 $\textit{possède}(x,y)$ ($x$ possède $y$).
369
370 Traduisez en langage courant les formules quantifiées suivantes :
371 \begin{enumerate}
372 \item $\forall x\, . \textit{vélo}(x) \imp 
373 (\exists z \, . \, \textit{curé}(z) \land \textit{possède}(z,x))$.
374 \item $\forall x\, . \textit{curé}(x) \imp 
375 (\forall y,z \, . \, (\textit{velo}(y) \land \textit{velo}(z) \land y
376 \neq z ) \imp 
377 (\neg \textit{possède}(x,y) \lor \neg \textit{possède}(x,z)))$
378 \item $\exists x \, . \, \textit{curé}(x) \land 
379 (\forall y \, . \, \textit{vélo}(y) \imp \neg
380 \textit{possède}(x,y))$. 
381 \end{enumerate}
382 \end{Exo}
383
384
385
386
387 \subsection{Alternance de quantificateurs}
388
389 Attention : \emph{Il est interdit d'intervertir des quantificateurs 
390 de symboles différents} (si l'on désire que la formule conserve le 
391 même sens, bien entendu).
392
393 \begin{Ex} $ $
394
395 \begin{itemize}
396 \item $\qqs x\, . \, \exi  y \, .\, \textit{travaille}(x,y)$ signifie que
397 tout étudiant travaille une matière (au moins).
398 Autrement dit, la matière travaillée  dépend de cet étudiant, elle
399 n'est éventuellement pas la même pour tous les étudiants. 
400
401 \item La formule $\exi y\, . \, \qqs x\, .\, \ 
402 \textit{travaille}(x,y)$ signifie qu'il y a une matière que tous les 
403 étudiants travaillent. La différence fondamentale avec le cas 
404 précédent est que, dans cette dernière affirmation, on affirme que 
405 tous les étudiants travaillent la même matière.
406 \end{itemize}
407 \end{Ex}
408
409 % AG : cet exemple n'est pas très satisfaisant, car donne vrai dans
410 % les deux cas.
411 % \begin{Ex}
412 % Un autre exemple, plus mathématique :
413 % \begin{itemize}
414 % \item $\qqs x\exi y\,(x+y=x)$, soit: \og pour tout $x$, on peut
415 %   trouver un $y$, tel que $x+y=x$\fg{} . Si l'univers du discours est
416 %   une algèbre de Boole, il est clair que la formule est vraie : il
417 %   suffit pour s'en convaincre de choisir $y=x$, et on a bien, en
418 %   algèbre de Boole, $x+x=x$: la valeur de $y$ dépend bien de celle de
419 %   $x$ (c'est la même). 
420
421 % \item $\exi y \qqs x\,(x+y=x)$, soit: \og il existe une valeur de $y$
422 %   telle que, pour tout $x$, $x+y=x$\fg{} . Si l'univers du discours
423 %   est une algèbre de Boole, il est clair que la formule est vraie :
424 %   la valeur 0 pour $y$ convient, et, si $y=0$, on a bien, quelle que
425 %   soit la valeur de $x$, $x+0=x$. 
426 % \end{itemize}
427 % \end{Ex}
428
429
430
431
432 % \begin{Ex}
433 % En supposant que $(a,b,c)$ prenne ses valeurs dans un univers du
434 % discours qui est une partie de $\R^3$ telle que $b^2-4ac>0$, la
435 % formule : 
436
437 % \begin{itemize}
438
439 % \item $\qqs a\,.\, \qqs b \, . \,   \qqs c \, .\,   \exi x\, .\, \
440 %   ax^2+bx+c=0$ est une formule vraie (une équation du second
441 %   degré dont le discriminant est positif admet des racines réelles, et
442 %   tout le monde sait que les valeurs de ces racines dépendent de
443 %   celles de $a$, de $b$ et de $c$). 
444
445 % \item $\exists x\,.\,\qqs a\,.\,\qqs b\,.\,\qqs c\,.\, ax^2+bx+c=0$ est
446 %   une formule fausse : il n'y a pas de réel qui soit solution de
447 %   n'importe quelle équation du second degré ! 
448 % \end{itemize}
449 % \end{Ex}
450
451 \begin{Exo}
452 Dans cet exercice, nous considérons qu'aimer est une relation binaire 
453 (non nécessairement symétrique). On note $\textit{aime}(x, y)$ 
454 si la personne $x$ aime la personne $y$.
455
456 \begin{enumerate}
457 \item Représentez, à l'aide de propositions logiques, les phrases suivantes :
458 \begin{enumerate}
459 \item  Quelqu'un aime Valentine.
460 \item Personne n'aime Quentin.
461 \item Toute personne aime quelqu'un.
462 \item Quelqu'un est aimé de tous.
463 \item Toute personne s'aime.
464 \item  Il n'y a personne qui ne s'aime pas lui-même.
465 \end{enumerate}
466 \item Les deux propositions suivantes sont-elles \'equivalentes ?
467 $$(\exists x\, .\, \textit{aime}(x,\textit{caroline}) )\land  
468 (\exists x\, .\, \textit{aime}(\textit{caroline}, x) )$$ 
469 et 
470 $$\exists x \, . \,  \textit{aime}(x,\textit{caroline}) 
471 \land  \textit{aime}(\textit{caroline}, x)$$
472 \end{enumerate}
473 \end{Exo}
474
475 \begin{Exo}
476 Formaliser les propositions suivantes dans le calcul des prédicats.
477 \begin{enumerate}
478 \item \og Il existe une planète plus petite que toutes les autres;\fg{}
479 \item \og Il y a une planète plus grande que tout objet du système solaire;\fg{}
480 \item \og Toute planète a une planète plus proche du soleil qu'elle;\fg{}
481 \item \og Certaines planètes sont plus petites que Neptune, d'autres pas;\fg{}
482 \item \og Il n'y a pas de planète qui soit plus grande qu'une autre tout en 
483   étant plus proche du soleil qu'elle;\fg{}
484 \item \og Tout ce qui tourne autours de la Terre est plus petit que toutes 
485   les planètes;\fg{}
486 \item \og Certaines planètes sont plus grosses que Neptune, mais aucune n'est 
487   plus éloignée du soleil qu'elle;\fg{}
488 \item \og Certaines planètes sont plus grosses que Neptune tout en étant  
489   plus éloignées du soleil qu'elle.\fg{}
490 \end{enumerate}
491 \end{Exo}
492
493 % \begin{Exo}
494 % Traduire les affirmations suivantes en formules au moyen de prédicats
495 % et de quantificateurs.
496 % \begin{enumerate}
497 % \item \og la somme des angles d'un triangle vaut 180 degrés \fg{}
498 % \item \og deux droites perpendiculaires a une même troisième sont
499 %   parallèles entre elles\fg{}
500 % \item \og un nombre complexe égal à son conjugué est un nombre réel
501 %   \fg{}
502 % \item \og après 4, tout entier pair est la somme de deux nombres
503 %   premiers\fg{} 
504 % \item \og un polynome de degré $n$ ne peut pas s'annuler plus de $n$
505 %   fois \fg{}
506 % \end{enumerate} 
507 % \end{Exo}
508
509 % \begin{Exo}
510 % Imaginer une façon d'exprimer l'affirmation suivante 
511 % \og
512 % $\epsilon + \epsilon + \epsilon + \ldots +\epsilon$ finit toujours par
513 % faire beaucoup, même si $\epsilon$ est très petit \fg{} au moyen d'un
514 % prédicat d'arité 3 et de trois quantificateurs.
515 % \end{Exo}
516
517 \subsection{Portée d'un quantificateur}
518
519 \begin{Def}[Portée d'un quantificateur] La \emph{portée d'un 
520 quantificateur}\index{portée d'un 
521 quantificateur}\index{quantificateur!portée} dans une formule du 
522 calcul des prédicats est la partie de cette formule couverte par ce 
523 quantificateur.
524 \end{Def}
525
526
527 Par convention, dans l'écriture d'une formule, un quantificateur est
528 prioritaire sur tout connecteur logique. Sa portée est donc
529 généralement clairement délimitée par une paire de parenthèses, avant
530 le quantificateur jusqu'après la formule elle-même. 
531
532
533 \begin{Exo}
534 Dans cet exercice $f_n$ signifie que le symbole $f$ (propositionnel ou
535 prédicatif)  est d'arité $n$.
536 On considère un langage 
537 $\mathcal{L}=\{f_1, g_1, h_2, R_1,S_2,T_2,=_2\}$ et les expressions
538 suivantes:
539 \begin{itemize}
540 \item 
541 $ \varphi_1  : 
542 \exists x \,. \, 
543 (
544 (\forall y \, . \, 
545 (\exists z \,.\,
546 R(x)))) \lor
547 (\exists y \, .\, 
548 (\neg 
549 (\forall z \, . \, 
550 (S(h(x,z),x)))))
551 $
552
553 \item 
554 $ \varphi_2  : 
555 (\forall x \, .\, 
556 (T(f(x),y)) 
557 \imp
558 (\neg 
559 (\exists x \, .\, (f(x,y)))))$
560
561 \item 
562 $ \varphi_3  :
563 (\forall z \, .\,
564 T(x,y) \imp
565 (\exists y \,.\,
566 ((\forall x' \, . \,\neg (f(x) = y))) \lor T(y,z)))$
567
568 \item 
569 $ \varphi_4  : 
570 (\forall x \,.\,
571 (\exists y  \,.\,
572 (( g(y) = x) \lor 
573 (\neg T(y,y)))))
574 \imp 
575 (\exists y \,.\,
576 (\forall x \,.\,
577 (T(y,g(x)))))$
578 \end{itemize}
579
580 \begin{enumerate}
581 \item Parmi ces expressions, lesquelles sont des formules de
582 $\mathcal{L}$ ?
583 \item Pour celles qui sont des formules, supprimer les parenthèses
584   inutiles.
585 \item Déterminer les occurrences liées des variables dans les formules.
586 \end{enumerate}
587 \end{Exo}
588
589
590 \begin{Exo}
591 Classer les huit propositions suivantes dans les deux premières
592 colonnes libres du tableau ci-dessous de 
593 manière à ce que les relations annoncées soient vérifiées.
594
595 Compléter le tableau avec les formules correspondantes.
596
597 \begin{enumerate}
598 \item Dans cette assemblée, tout le monde parle l'anglais et le français.
599 \item Dans cette assemblée, tout le monde parle l'anglais ou le français.
600 \item Dans cette assemblée, tout le monde parle l'anglais et tout le monde 
601   parle le français.
602 \item Dans cette assemblée, tout le monde parle l'anglais ou tout le monde 
603   parle le français.
604 \item Un accompagnateur au moins parlera le russe et un accompagnateur  
605   au moins parlera le chinois.
606 \item Un accompagnateur au moins parlera le russe ou un accompagnateur  
607   au moins parlera le chinois.
608 \item Un accompagnateur au moins parlera le russe et le chinois.
609 \item Un accompagnateur au moins parlera le russe ou le chinois.
610 \end{enumerate}
611 \begin{center}
612 \begin{tabular}{|c|c|c|c|c|c|}
613   \hline
614   \multirow{2}{0.5cm}{\ldots} & $\Rightarrow$ & 
615   \multirow{2}{0.5cm}{\ldots} &
616   \multirow{2}{3.5cm}{$\forall x\,. \, P(x) \ldots Q(x)$} & 
617   \multirow{2}{0.5cm}{$\approx$} & 
618   \multirow{2}{3.5cm}{$\forall x\,. \, P(x) \ldots \forall y\,. \, Q(y)$}\\
619   \cline{2-2}
620   & $\Leftarrow$ & & & & \\
621   \hline
622   \multirow{2}{0.5cm}{\ldots} & $\Rightarrow$ & 
623   \multirow{2}{0.5cm}{\ldots} &
624   \multirow{2}{3.5cm}{\ldots} & 
625   \multirow{2}{0.5cm}{$\not \approx$} & 
626   \multirow{2}{3.5cm}{\ldots}\\
627   \cline{2-2}
628   & $\not \Leftarrow$ & & & & \\
629   \hline
630   \multirow{2}{0.5cm}{\ldots} & $\Rightarrow$ & 
631   \multirow{2}{0.5cm}{\ldots} &
632   \multirow{2}{3.5cm}{\ldots} & 
633   \multirow{2}{0.5cm}{$ \approx$} & 
634   \multirow{2}{3.5cm}{\ldots}\\
635   \cline{2-2}
636   & $ \Leftarrow$ & & & & \\
637   \hline
638   \multirow{2}{0.5cm}{\ldots} & $\Rightarrow$ & 
639   \multirow{2}{0.5cm}{\ldots} &
640   \multirow{2}{3.5cm}{\ldots} & 
641   \multirow{2}{0.5cm}{$\not \approx$} & 
642   \multirow{2}{3.5cm}{\ldots}\\
643   \cline{2-2}
644   & $\not \Leftarrow$ & & & & \\
645   \hline
646 \end{tabular}
647 \end{center}
648 \end{Exo}
649
650
651
652
653
654
655 \subsection{Formules du calcul des prédicats}
656 % AG : Cette introduction ne convient pas : on utilise aussi des
657 % connecteurs logiques entre formules avec variables libres !
658 % JFC : un atome peut contenir des variables. Cela permet de définir 
659 % des formules avec variables libres
660 % Comme les prédicats produisent des propositions
661 % \begin{itemize}
662 %  \item soit quand les variables sont remplacées par des individus,
663 %  \item soit quand elles sont liées par quantification,
664 % \end{itemize}
665 %  il est possible de relier ces propositions par les connecteurs 
666 %  logiques habituels, comme en calcul propositionnel. On obtient ainsi 
667 %  une formule du calcul des prédicats\ldots
668
669
670 \begin{Def}[Formule]
671 La définition d'une \emph{formule}\index{formule} est:
672
673 \begin{itemize}
674
675 \item un atome est une formule,
676
677 \item si $P$ est une formule, si $Q$ est un symbole de quantificateur
678   et si $x$ est un symbole de variable, alors $Qx\,.\, P $ est une
679   formule, 
680
681 \item si $P$ est une formule, alors $\non(P)$ est une formule,
682
683 \item si $P$ et $Q$ sont des formules, alors 
684   $(P \ou Q)$, 
685   $(P \et Q)$,
686   $(P \imp Q)$, 
687   $(P \eqv Q)$ sont des formules,
688
689 \item il n'existe pas d'autres manières de construire une formule
690 qu'en appliquant les règles précédentes un nombre fini de fois.
691 \end{itemize}
692 \end{Def}
693
694 \begin{Exo}
695 On considère un ensemble d'objets de différentes couleurs.
696 Chacun de ces objet porte un numéro et possède une forme géométrique
697 particulière (cube, sphère prisme).
698 En utilisant les prédicats 
699 $\textit{pair}(x)$, $\textit{cube}(x)$,
700 $\textit{vert}(x)$\ldots, formalisez les phrase suivantes en logique 
701 des prédicats
702 \begin{enumerate}
703 \item Si un objet est sphérique, alors cet objet n'est pas vert ou
704   porte un numéro impair.
705 \item S'il existe un objet vert sphérique, alors il existe un objet
706   vert portant un numéro impair.
707 \item Si tout objet vert porte un numéro impair, alors aucun objet
708   sphérique n'est vert.
709 \end{enumerate}
710 \end{Exo}
711
712
713
714 \section{Sémantique}
715
716
717
718
719 \subsection{Valeurs de vérité}
720
721
722 Le calcul des prédicats utilise, comme le calcul propositionnel, les
723 connecteurs logiques, et produit des propositions.
724 Il est possible d'étendre la notion de \og valeur de vérité\fg{} au
725 calcul des prédicats. 
726 Mais l'étude de la valeur de vérité d'une formule du calcul des
727 prédicats est beaucoup plus compliquée.
728
729 \begin{enumerate}
730  \item Une expression typique (une forme propositionnelle) du calcul
731    propositionnel est $P\imp Q$. 
732 Les \og atomes\fg{} sont ici des variables propositionnelles qui
733 peuvent être remplacées par n'importe quelle proposition. Quelle que
734 soit cette proposition, sa valeur de vérité ne peut être que \og
735 \vrai \fg{} ou \og \faux\fg{}. 
736 Cela permet de lui associer une simple variable booléenne, sa valeur
737 de vérité, pour obtenir simplement la fonction de vérité $\sur p+q$. 
738
739 \item Une expression analogue (une formule) du calcul des prédicats
740   pourrait être $\forall x\, .\, p(x,y)\imp q(x,z)$. 
741   Les atomes sont ici des prédicats binaires qui, eux aussi, ne
742   peuvent prendre que les valeurs \og \vrai\fg{} ou \og \faux\fg{}, mais
743   pas indépendamment des individus considérés.
744 \end{enumerate}
745
746
747
748 Il n'est donc pas possible de remplacer un atome par une simple
749 variable booléenne. Seule une fonction booléenne (de variables non
750 booléennes) peut convenir, pour faire intervenir les valeurs des
751 variables qui sont les arguments du prédicat. 
752 \begin{itemize}
753  \item si $f_p(x,y)$ est la fonction booléenne associée au prédicat
754    $p(x,y)$ 
755 \item si $f_q(x,z)$ est celle qui est associée à $q(x,z)$, 
756 \end{itemize}
757 alors la fonction de vérité de la formule est: $\sur{f_p(x,y)}+f_q(x,z)$.
758
759 Attention, $x$, $y$ et $z$ ne sont pas ici des variables booléennes,
760 mais elles prennent leurs valeurs dans l'univers du discours. Il n'est
761 donc pas question de \og calculer avec $x$, $y$ et $z$ comme en
762 algèbre de Boole\fg{}. 
763
764 Le seul moyen, en général, pour étudier une telle fonction de vérité
765 est de construire le tableau de ses valeurs, en donnant à $x$, $y$ et
766 $z$ successivement toutes les valeurs possibles dans l'univers du
767 discours (si celui-ci est infini, on imagine aisément les problèmes
768 qui vont se poser\ldots). 
769
770
771 Les définitions de tautologie et de conséquence logique s'adaptent
772 comme suit.
773
774 \begin{Def}[Tautologie, conséquence logique, équivalence]
775 si $P$ et $Q$ sont des formules du calcul des prédicats
776
777 \begin{itemize}
778
779 \item $\tauto P$ [$P$ est une tautologie] si et seulement si, pour
780   tous les univers du discours possibles, pour tous les prédicats qui
781   interviennent dans $P$, et pour toutes les valeurs des
782   variables dans chacun des univers, la valeur de vérité de $P$ est
783   \og \vrai\fg{}. 
784
785 \item $\{P\}\tauto Q$ [$Q$ est conséquence logique de $P$] si et seulement
786   si, dans les mêmes conditions que ci-dessus, chaque fois que $P$ est
787   vraie, $Q$ l'est aussi. 
788
789 \item $P\approx Q$ [les formules $P$ et $Q$ sont équivalentes] si et
790   seulement si $\{P\}\tauto Q$ et $\{Q\} \tauto P$. 
791
792 \end{itemize}
793 \end{Def}
794
795
796 Il reste à  donner la définition de la fonction de vérité pour les
797 nouveaux symboles introduits (les quantificateurs)\ldots 
798
799
800 \begin{itemize}
801 \item la valeur de vérité de $\qqs x\,. \, p(x)$ est obtenue en faisant la
802   liste des valeurs de vérité de $p(x)$ pour toutes les valeurs
803   possibles de $x$ dans l'univers du discours: 
804   % (liste effective lorsque  c'est possible, ou démonstration).
805   si, pour toute valeur de $x$, la
806   valeur de vérité de $p(x)$ est $\vrai$, alors la valeur de vérité de
807   $\qqs x\, . \, p(x)$ est $\vrai$. S'il y a une seule valeur de $x$ pour
808   laquelle la valeur de vérité de $p(x)$ est $\faux$, alors la valeur
809   de vérité de $\qqs x\, . \, p(x)$ est $\faux$. 
810
811 \item la valeur de vérité de $\exi x\, . \, p(x)$ est obtenue en faisant la
812   liste des valeurs de vérité de $p(x)$ jusqu'à ce qu'on trouve
813   $\vrai$. Si on trouve $\vrai$, la valeur de vérité de 
814   $\exi x\, . \, p(x)$
815   est $\vrai$. Si, pour tout élément $x$ de l'univers du discours, la
816   valeur de vérité de $p(x)$ est $\faux$,
817   % (liste effective ou  démonstration),
818  alors celle de $\exi x\, . \, p(x)$ est $\faux$. 
819
820 \end{itemize}
821
822
823 Bien entendu, dans certains cas, il n'est pas nécessaire d'établir
824 effectivement la table de vérité d'une formule du calcul des prédicats
825 pour prouver qu'il s'agit d'une tautologie. Par exemple, il est bien
826 clair que, pour un atome $p(x,y,z)$, on a: 
827 $\tauto  (\forall x, y, z \, . \,  p(x,y,z)) \imp 
828 (\forall x, y, z \, . \,  p(x,y,z)) $.  
829
830 % Soit $p$ est un prédicat unaire.
831 % Pour donner un exemple de la complexité introduite en théorie
832 % des valeurs de vérité par le calcul des prédicats, étudions la formule
833 % $\forall x,y \, . \, p(x) \imp p(y)$ 
834 % pour savoir s'il s'agit d'une
835 % tautologie. Pour prouver qu'il s'agit d'une tautologie, il faut prouver
836 % que:  
837
838 % \begin{itemize}
839
840 % %\item 
841 % \item pour tout univers du discours ${\cal U}$,
842
843 % \item pour toutes valeurs des variables $x$ et $y$ dans ${\cal U}$,
844
845 % \end{itemize}
846 % la valeur de vérité de la formule est $\vrai$. \og Pour tout univers du
847 % discours\fg{} : il faut envisager des univers à 1, puis 2,\ldots
848 % éléments et essayer d'en déduire un résultat général, si c'est
849 % possible. 
850
851 % \begin{itemize}
852  
853 % \item Dans un univers à un seul élément, $x$, comme $y$, ne peut
854 %   prendre qu'une seule valeur; on a donc $x=y$, et donc la valeurs de
855 %   vérité de $p(x)$ est la même que celle de $p(y)$, et donc $p(x)\imp
856 %   p(y)$ est $\vraie$ [table de l'implication]. 
857
858 % \item Dans un univers à deux éléments, pour que la valeur de vérité de
859 %   $p(x)$ soit définie, il faut se la donner pour chacune des deux
860 %   valeurs de $x$; or, il faut le faire \og pour tout prédicat unaire
861 %   $p$\fg{} , donc envisager toutes les fonctions booléennes de deux
862 %   variables: il y en a quatre, que nous noterons $z$, $i$, $n$, et
863 %   $r$. Désignons les deux éléments de ${\cal U}$ par 1 et 2 (pour ne
864 %   pas les confondre avec des variables booléennes):\saut 
865 % \centerline{\begin{tabular}{|c|c|c|c|c|} \hline
866 % $x$ & $z(x)$ & $i(x)$ & $n(x)$ & $r(x)$ \\ \hline
867 % $1$ & $\faux$ & $\faux$ & $\vrai$ & $\vrai$ \\ \hline
868 % $2$ & $\faux$ & $\vrai$ & $\faux$ & $\vrai$ \\ \hline
869 % \end{tabular}}\par
870 % \noindent Puis il faut faire le tableau des valeurs de vérité de
871 % $p(x)$, $p(y)$ et de $p(x)\imp p(y)$ en fonction des valeurs de $x$ et
872 % de $y$ et de la fonction booléenne associée à $p$ ($z$, $i$, $n$, ou
873 % $r$)\saut\centerline{ 
874 % \begin{tabular}{|c|c|c|c|c|c|}\hline
875 % fonction booléenne de $p$ & $x$ & $y$ & $p(x)$ & $p(y)$ & $p(x)\imp p(y)$
876 % \\ \hline $z$ & 1 & 1 & $\faux$ & $\faux$ & $\vrai$ \\ \hline 
877 % & 1 & 2 & $\faux$ & $\faux$ & $\vrai$ \\ \hline
878 % & 2 & 1 & $\faux$ & $\faux$ & $\vrai$ \\ \hline
879 % & 2 & 2 & $\faux$ & $\faux$ & $\vrai$ \\ \hline
880 % $i$ & 1 & 1 & $\faux$ & $\faux$ & $\vrai$ \\ \hline
881 % & 1 & 2 & $\faux$ & $\vrai$ & $\vrai$ \\ \hline
882 % & 2 & 1 & $\vrai$ & $\faux$ & $\faux$ \\ \hline
883 % & 2 & 2 & \dotfill & \dotfill & \dotfill \\ \hline
884 % $n$ & \dotfill & \dotfill & \dotfill & \dotfill & \dotfill \\ \hline
885 % \end{tabular}}\par 
886 % \noindent Inutile de construire le reste du tableau: on a trouvé $\faux$ dans une ligne, donc $p(x)\imp p(y)$ n'est pas une tautologie [en effet, il existe un prédicat unaire, un univers à deux éléments, et, dans cet univers, une valeur de $x$ et une valeur de $y$ pour lesquels la formule est fausse\ldots].
887
888 % \end{itemize}
889
890
891 Donnons enfin deux exemples pour lesquels la construction d'une table
892 de vérité n'est pas nécessaire : 
893
894 \begin{Exo}
895 Montrer que 
896 $\tauto (\qqs x\, . \, p(x,x))\imp (\qqs x \, . \, (\exi
897 y\, . \, p(x,y)))$.
898
899 % Soit ${\cal U}$ un univers du discours, $p$ une relation binaire
900 % sur ${\cal U}$.
901
902 % \begin{itemize}
903  
904 % \item Premier cas : dans ${\cal U}$, $\qqs x\, . \, p(x,x)$ est
905 %   $\faux$; alors 
906 %   l'implication est vraie. 
907
908 % \item Deuxième cas : dans ${\cal U}$, $\qqs x\,. \, p(x,x)$ est 
909 % $\vrai$; donc, pour chaque valeur de $x$ dans ${\cal U}$, $p(x,x)$ 
910 % est vrai. Alors  $\forall x \, . \, \exi y\,.\, p(x,y)$ est $\vrai$ 
911 % car, pour toute valeur de $x$, il suffit de prendre pour $y$ la même 
912 % valeur que celle de $x$ pour que $p(x,y)$ soit $\vrai$.
913
914 % \end{itemize}
915 \end{Exo}
916
917
918 % \begin{Ex}
919 % Montrer que 
920 % $(\qqs x\, . \, (r(x)\imp s(x)))\et (\exi x\,.\, (\non r(x)\et s(x))$
921 %  n'est ni une antilogie, ni une tautologie.
922
923 % Pour montrer que cette formule n'est pas une antilogie, il suffit
924 % d'exhiber un exemple dans lequel elle est vraie; pour montrer qu'elle
925 % n'est pas une tautologie, il suffit d'exhiber un exemple dans lequel
926 % elle est fausse. 
927
928 % \begin{itemize}
929
930 % \item ${\cal U}$ est l'ensemble des habitants de la France; $r(x)$ est
931 %   le prédicat \og $x$ habite Belfort\fg{} et $s(x)$ est le prédicat \og
932 %   $x$ habite la France\fg{} . Puisque Belfort est en France, tout
933 %   habitant de Belfort habite la France, donc 
934 %   $\qqs x\, . \, r(x)\imp s(x)$
935 %   est $\vrai$. Mais tous les habitants de la France ne sont pas
936 %   concentrés à Belfort, autrement dit: il existe des habitants de la
937 %   France qui n'habitent pas Belfort, 
938 % donc: $\exi x\, . \, \non r(x) \et s(x)$ est $\vrai$; enfin, d'après
939 % la table de vérité de la conjonction logique, la formule est vraie. 
940
941 % \item ${\cal U}$ est un ensemble $E$, dans lequel on a défini deux
942 %   parties $R$ et $S$, telles que $S\sse R$; $r(x)$ est le prédicat \og
943 %   $x\in R$\fg{} et $s(x)$ est le prédicat \og $x\in S$\fg{} . Comme
944 %   $S\sse R$, tout élément extérieur à $R$ ne peut pas être dans $S$,
945 %   donc $\exi x\,.\, \non r(x) \et s(x)$ est $\faux$, et donc la formule
946 %   est fausse. 
947
948 % \end{itemize}
949
950 % \end{Ex}
951
952
953
954 \subsection{Simplification de formules quantifiées}
955 De la définition de la valeur de vérité d'une formule quantifiée, on 
956 peut déduire:
957
958 \begin{eqnarray*}
959   \non (\exi x\, . \, p(x)) & \approx & (\qqs x \,.\, \non p(x))  \\
960   \non (\qqs x \,.\, p(x)) &\approx & (\exi x\, . \, \non p(x))  
961 \end{eqnarray*}
962
963 % \begin{Ex}
964 % considérons la proposition (fausse): 
965 % \og l'ensemble des entiers naturels admet un élément maximum\fg{}. 
966 % Pour formaliser cette proposition en calcul des prédicats,
967 % il faut introduire le prédicat classique d'inégalité qu'il faudrait,
968 % en toute rigueur, noter $\le (x,y)$, qui signifie que $x$ est
969 % inférieur ou égal à $y$, mais 
970 % pour lequel nous conserverons la notation usuelle $x \leqslant
971 % y$. L'univers du discours est évidemment $\N$, et, pour exprimer que
972 % $\N$ admet un élément maximum, on exprime que tout élément de $\N$ est
973 % inférieur ou égal à cet élément maximum, 
974 % soit: 
975 % $$\exi M \,.\, \qqs n\,.\, n\leqslant M.$$
976
977 % % (en calcul des prédicats, on ne précise jamais
978 % % l'univers du discours dans la formule, comme on le fait habituellement
979 % % en mathématiques: $\exi M\in\N,\ \qqs n\in\N,\ n\leqslant M$)
980 % Pour montrer que cette proposition est fausse, 
981 % on intuite qu'il suffit de démontrer que 
982 % sa négation est vraie, soit 
983 % $$
984 % \non (\exi M \,.\, \qqs n\,.\, n\leqslant M).$$
985
986 % D'après ce que nous venons de voir, cette
987 % négation a même valeur de vérité que
988 % $\qqs M \, .\, \exi n\,.\, \non (n\leqslant M)$, ou encore 
989 % $\qqs M \, .\, \exi n\,.\, M<n$.
990 % Ceci signifie que, pour tout entier
991 % $M$, on peut trouver un entier $n$ qui est plus grand (il suffit de
992 % prendre $n$ égal à $M+1$).
993 % \end{Ex}
994
995 \begin{Exo}
996 \'Ecrire la négation des formules suivantes
997 \begin{enumerate}
998 \item  $\forall x \, .\, p(x) \imp q(x)$
999 \item  $\exists x \, .\, p(x) \land q(x)$
1000 \item  $\forall x \, . \, p(x) \Ssi q(x)$
1001 \item  $\exists x\, .\, (\forall y \,.\,
1002   q(x,y) \imp (p(x,y) \lor r(x,y)))$ 
1003 \end{enumerate}
1004
1005 % Réponses:
1006 % \opt{prof}{
1007 % \begin{enumerate}
1008 % \item $\exists x \, .\, p(x) \land \neg q(x)$
1009 % \item $\forall x \, .\, p(x) \imp \neg q(x)$
1010 % \item $\exists x \, . \, (p(x) \land  \neg q(x)) \lor (\neg p(x) \land q(x))$
1011 % \item 
1012 % $\forall x\, .\, (\exists y \,.\,
1013 %   q(x,y) \land \neg p(x,y) \land \neg r(x,y))$ 
1014 % \end{enumerate}
1015 % }
1016 % \opt{etud}{
1017 % \vspace{10cm}
1018 % } 
1019 \end{Exo}
1020
1021 \begin{Exo}
1022 \'Ecrire la négation des formules suivantes
1023 \begin{enumerate}
1024 \item  $\forall x \, .\, (\exists y \,.\, p(x,y) \land q(x,y))$
1025 \item  $\forall x \, .\, (\exists y \,.\, p(x,y) ) \imp q(x)$
1026 \item  $\forall x \, .\, (\exists y \,.\, p(x,y) ) \imp
1027   (\forall z\, .\, q(z))$
1028 \item $ \forall x \,.\, r(x) \imp (\exists y \,.\, p(x,y))$
1029 \end{enumerate}
1030 \end{Exo}
1031
1032 \noindent Voici d'autres résultats d'équivalences entre formules
1033 permettant de réduire la portée de quantificateurs.
1034
1035
1036 \begin{Th}[Réduction de portée de quantificateurs]
1037 Soit $p$ et $q$ des prédicats unaires. Alors on a les deux
1038 équivalences suivantes :
1039
1040 \begin{eqnarray}
1041   (\qqs x\, . \, p(x) \et q(x)) 
1042   &\approx& 
1043   (\qqs x\, . \, p(x)) 
1044   \et
1045   (\qqs y\, . \, q(y)) \label{eq:reduction:forall}\\
1046   (\exi x\,.\, p(x) \ou q(x)) 
1047   &\approx&
1048   (\exi x\,.\, p(x))
1049   \ou
1050   (\exi y\,.\, q(y))
1051    \label{eq:reduction:exists}
1052 \end{eqnarray}
1053 \end{Th}
1054
1055 \begin{Proof}$ $ 
1056
1057 \paragraph{Preuve  de (\ref{eq:reduction:forall}).}
1058 Si, pour toute valeur de $x$, $p(x)$ et $q(x)$ sont
1059 simultanément vrais, alors, pour toute valeur de $x$, $p(x)$ est vrai,
1060 et, 
1061 pour toute valeur de $y$, $q(y)$ est vrai. 
1062 Réciproquement, si, pour toute
1063 valeur de $x$, $p(x)$ est vrai, et, si, pour toute valeur de $y$,
1064 $q(y)$ 
1065 est aussi vrai, il est bien évident que, pour toute valeur de $x$,
1066 $p(x)$ 
1067 et $q(x)$ sont simultanément vrais. 
1068
1069 \paragraph{Preuve  de (\ref{eq:reduction:exists}).}
1070 S'il existe une valeur de $x$ pour laquelle l'une au moins des deux 
1071 propriétés $p(x)$ ou $q(x)$ est vraie, il est bien clair qu'il existe 
1072 une valeur de $x$ pour laquelle $p(x)$ est vraie ou qu'il en existe 
1073 une pour laquelle $q(y)$ est vraie; la réciproque est aussi évidente.
1074 \end{Proof}
1075
1076 \begin{Exo}
1077 Trouver 
1078 \begin{enumerate}
1079 \item un exemple où $\forall x \, .\, p(x) \lor q(x)$ est vraie  
1080   sans que $(\forall x \, .\, p(x)) \lor (\forall x \, .\, q(x))$ ne le
1081   soit;
1082 \item un exemple où 
1083 $(\exists x \, .\, p(x)) \land (\exists x \, .\,  q(x))$ est vraie 
1084   sans que 
1085   $\exists x \, .\, p(x) \land q(x)$ ne le
1086   soit.
1087 \end{enumerate}
1088 \end{Exo}
1089
1090 \begin{Exo}
1091 Pour chacune des formules suivantes,  
1092 \begin{itemize}
1093 \item dire si c'est une négation, une conjonction, une disjonction, 
1094 une implication, une quantification (universelle ou existentielle);
1095 \item donner la portée des quatificateurs;
1096 \item donner les occurences libres des variables.
1097 \end{itemize}
1098
1099 \begin{enumerate}
1100 \item  $\exists x \, . \, A(x,y) \land B(x)$
1101 \item  $\exists x \, . \, (\exists y \, . \, A(x,y) \Rightarrow B(x))$
1102 \item  $\neg (\exists x \, . \, \exists y \, . \, A(x,y) \Rightarrow B(x))$
1103 \item  $\forall x \, . \, \neg (\exists y \, . \, A(x,y))$
1104 \item  $\exists x \, . \, A(x,y) \land B(x)$
1105 \item  $\exists x \, . \, A(x,x) \land \exists y \, . \,B(y)$
1106 \end{enumerate}
1107 \end{Exo}
1108
1109 \subsection{Substitutions}
1110
1111 Si $t$ est  un terme et $\varphi$ est une formule pouvant contenir la
1112 variable $x$, alors  $\varphi(t/x)$ est le résultat du remplacement de
1113 toutes les occurrences libres de $x$ par $t$ dans $\varphi$. 
1114
1115
1116 Le résultat du remplacement $\varphi(t/x)$ est une formule qui est 
1117 une conséquence logique de la formule originale $\varphi$ si aucune 
1118 des  variables libre de $t$ ne devient liée suite à ce remplacement. 
1119 Pour éviter que de telles variables libres deviennent liées il suffit 
1120 de changer le nom des variables liées de $\varphi$ en des noms frais 
1121 (qui n'apparaissent pas dans les variables libres de $t$). L'oubli de 
1122 cette condition est une cause fréquente d'erreurs de raisonnement.
1123
1124
1125 A titre d'exemple, on considère la formule $\varphi$ définie par 
1126 $\forall y \, .\, y \le x $ sur l'univers $\mathcal{U}$.
1127 \begin{itemize}
1128 \item Si $t$ est un terme sans la variable libre $y$, 
1129 alors  $\varphi(t/x)$ signifie juste que $t$ est l'élément maximal.
1130 \item A l'opposé, si $t$ est $y$, la formule $\varphi(y/x)$ est
1131   $\forall y\,.\, y \le y$ qui ne dit plus que $y$ est maximal. 
1132 \end{itemize}
1133
1134 \begin{Exo}
1135 Soit le langage $\mathcal=\{a, f_2, R_2, S_1\}$, les termes 
1136 $t_i$ et les formules $\varphi_j$ suivantes.
1137 \begin{itemize}
1138 \item $t_1 = f(x,y)$
1139 \item $t_2 = f(a,y)$
1140 \item $t_3 = a$
1141 \item $t_4 = f(x,f(x,x))$
1142 \item $\varphi_1 : R(x,y) \imp \forall y \,. \, S(y)$
1143 \item $\varphi_2 : 
1144   (\forall y \, .\, R(y,a) ) \imp 
1145   (\exists y \, .\, R(x,y))$
1146 \item $\varphi_3 : 
1147   (\forall x \,.\,  \exists z \,.\, R(x,z))
1148   \land 
1149   (\exists x \,.\,  \forall y \,.\, R(y,x))$
1150 \end{itemize}
1151 Déterminer si $t_i$ est substituable à $x$ dans $\varphi_j$ et
1152 calculer,  le cas échéant, $\varphi_j (t_i/x)$ pour $1 \le i \le 4$ et 
1153 $1 \le j \le 3$. Dans le cas où $t_i$ n'est pas substituable, renommer
1154 les variables qui le composent ou les variables de la formule afin
1155 qu'il le soit.
1156 \end{Exo}
1157
1158 \begin{Exo}
1159 Quelle est la valeur de vérité des formules 
1160 \begin{itemize}
1161 \item $\varphi_1 = \exists x,y,z \, . \, 
1162   x \neq y \land 
1163   y \neq z \land 
1164   z \neq x $
1165 \item $\varphi_1 = \forall x,y,z,t \, . \, 
1166   x \neq y \lor
1167   x \neq z \lor
1168   x \neq t \lor
1169   y \neq z \lor
1170   y \neq t \lor
1171   z \neq t$
1172 \end{itemize}
1173  pour les univers suivants
1174 \begin{itemize}
1175 \item $\mathcal{U}_1 = \{0\}$;
1176 \item $\mathcal{U}_2 = \{0,1\}$;
1177 \item $\mathcal{U}_2 = \{0,1,3\}$.
1178 \end{itemize}
1179
1180 % Réponse: 
1181 % \begin{itemize}
1182 % \item la formule $\varphi_1$ est fausse sur $\mathcal{U}_1$ et $\mathcal{U}_2$
1183 % mais vraie sur $\mathcal{U}_3$;
1184 % \item la formule $\varphi_2$ est vraie sur $\mathcal{U}_1$ et fausse ailleurs.
1185 % \end{itemize}
1186 \end{Exo}
1187
1188 \begin{Exo}
1189 Dans le langage $\mathcal{L}=\{R_2, =_2\}$, on considère 
1190 les formules
1191 suivantes:
1192 \begin{eqnarray*}
1193  \Gamma_1 &=&\forall x \,.\, \exists y\, .\, R(x,y) \\
1194  \Gamma_2 &=&\forall x \,.\, (\forall y\, .\, 
1195  (\exists z \, .\, R(x,z) \land R(z,y)) \imp R(x,y)) \\
1196  \Gamma_3 &=&\forall x,y \,.\, (R(x,y) \land R(y,x)) \Ssi
1197  y=x \\
1198  \Gamma_4 &=&\forall x,y \,.\, 
1199  (\exists z \, .\, \neg R(z,x) \land \neg R(z,y)) \lor x =y
1200 \end{eqnarray*}
1201 Déterminer la valeur de vérité de ces formules dans les
1202 interprétations suivantes :
1203 \begin{itemize}
1204 \item $\mathcal{U}_1= \N$ et 
1205 $R(x,y)$ est vraie si et seulement si  $x\le y$. 
1206 Le prédicat $=$ a l'interprétation standard.
1207
1208 \item $\mathcal{U}_2= \N\setminus \{0\}$ et 
1209 $R(x,y)$ est vraie si et seulement si  $x \neq y$ et $x$ divise $y$. 
1210 Le prédicat $=$ a l'interprétation standard.
1211 \end{itemize}
1212 \end{Exo}
1213
1214 % On notera par $A(x)$ une formule du calcul des prédicats (éventuellement
1215 % compliquée!) dans laquelle la variable $x$ présente des occurrences; ces
1216 % occurrences peuvent être libres ou liées, et $A$ peut présenter des
1217 % occurrences libres et des occurrences liées de $x$; bien entendu, il peut
1218 % aussi n'y avoir aucune occurrence libre, ou aucune occurrence liée; enfin,
1219 % d'autres variables peuvent aussi présenter des occurrences dans $A$. Soit
1220 % ensuite $t$ un terme du calcul des prédicats, qui présente des
1221 % occurrences de diverses variables (toutes libres, dans un terme,
1222 % évidemment; un terme ne comporte pas de quantificateurs).
1223
1224 % On dit que ce terme $t$ est libre pour $x$ dans $A$ lorsque les
1225 % occurrences libres de $x$ dans $A$ ne rentrent dans la portée d'aucun
1226 % quantificateur portant sur une variable de $t$.
1227 % \par\noindent
1228 % Exemple: Soit la formule $A(x)=\exi x\,r(x,y)\imp\qqs y\,s(x,y,z)$
1229 % [Cette formule présente une occurrence liée et une occurrence libre de
1230 % $x$].
1231
1232 % \begin{itemize}
1233
1234 % \item Examinons le terme $y$ (une variable est un terme) par rapport à la
1235 % variable $x$ dans $A$. Comme l'occurrence libre de $x$ dans $A$ (la
1236 % seconde) entre dans la portée du quantificateur $\qqs y$, et que $y$ est
1237 % une variable (et même la seule\ldots) du terme $y$, le terme $y$ n'est pas
1238 % libre pour $x$ dans $A$.
1239
1240 % \item Examinons le terme $t=f(x,z)$ [où $f$ est un symbole opératoire,
1241 % $t$ est bien un terme] par rapport à la variable $x$ dans $A$. Comme
1242 % l'occurrence libre de $x$ dans $A$ n'entre pas dans la portée d'un
1243 % quantificateur portant sur $x$ (et pour cause\ldots), ni dans celui d'un
1244 % quantificateur portant sur $z$ (il n'y en a pas\ldots), ce terme $t$ est
1245 % libre pour $x$ dans $A$.
1246
1247 % \end{itemize}
1248 % On appelle substitution libre de la variable $x$ par le terme $t$ dans la
1249 % formule $A$ le remplacement de $x$, dans toutes ses occurrences libres
1250 % dans $A$ (et uniquement celles-ci\ldots) par le terme $t$, à condition que ce
1251 % terme soit libre pour $x$ dans $A$. La nouvelle formule obtenue est notée
1252 % $(x\mid t)A$.
1253
1254 % \begin{itemize}
1255
1256 % \item il est impossible d'effectuer la substitution libre de $x$ par $y$
1257 % dans la formule de l'exemple ci-dessus ($y$ n'est pas libre pour $x$ dans
1258 % $A$).
1259
1260 % \item il est possible d'effectuer la substitution libre de $x$ par
1261 % $t=f(x,z)$ dans $A$, car ce terme est libre pour $x$ dans $A$. Le résultat
1262 % est $(x\mid f(x,z))A=\exi x\,r(x,y)\imp\qqs y\,s(f(x,z),y,z)$.
1263
1264 % \end{itemize}
1265 % Par convention, si $x$ ne présente pas d'occurrences libres dans $A$, la
1266 % substitution libre de $x$ par n'importe quoi est toujours possible, et
1267 % elle laisse la formule $A$ inchangée.
1268
1269 % %________________ 24.
1270
1271 % \subsection{Tautologies quantifiées}
1272
1273 % Soit $A(x)$ la formule $A$ où $x$ est une variable libre et $A(r)$ le
1274 % résultat de  $A[r/x]$. Alors:
1275
1276 % \begin{itemize}
1277
1278 % \item Tautologie 1: $\tauto (\qqs x\,.\, A(x))\imp A(r)$
1279 % \item Tautologie 2: $\tauto A(r)\imp (\exi x \, .\, A(x))$
1280
1281 % \end{itemize} 
1282 % La première est le \og principe de particularisation\fg{} : si, pour
1283 % toute valeur 
1284 % de $x$, $A(x)$ est vrai, alors $A(r)$ est vrai, $r$ étant une \og
1285 % valeur 
1286 % particulière\fg{} de $x$. La seconde est le principe d'\og exhibition
1287 % d'une 
1288 % valeur particulière\fg{} : si on peut trouver une valeur $r$ pour
1289 % laquelle 
1290 % $A(r)$ est vraie alors on peut affirmer qu'il existe une valeur de $x$ 
1291 % pour laquelle $A(x)$ est vraie (c'est $r$!).
1292
1293 % \noindent Exemples (mathématiques):
1294
1295 % \begin{itemize}
1296
1297 % \item Si tout nombre premier n'est divisible que par 1 et par lui-même,
1298 % alors 17 (qui est un nombre premier) n'est divisible que par 1 et par 17.
1299
1300 % \item Puisque 2 divise 6, il existe des nombres qui sont divisibles par 2.
1301
1302 % \end{itemize}
1303 % L'extrême simplicité de ces exemples ne doit pas faire oublier que le
1304 % terme $r$ peut être bien autre chose qu'une constante, en fait, tout terme
1305 % libre pour $x$ dans $A$.
1306
1307 % Soit $A(x)$ une formule répondant à la définition du paragraphe précédent
1308 % et $B$ une formule ne contenant pas d'occurrences libres de $x$. Alors:
1309
1310 % \begin{itemize}
1311
1312 % \item Si $\tauto B\imp A(x)$, alors: $\tauto B\imp (\qqs x\,.\, A(x))$
1313
1314 % \item Si $\tauto A(x)\imp B$, alors: $\tauto(\exi x\,.\, A(x))\imp B$.
1315
1316 % \end{itemize}
1317 % Le premier résultat est le \og principe de
1318 % généralisation\fg{} ; il est très souvent utilisé en
1319 % mathématiques: Si on conduit une démonstration qui a pour conclusion
1320 % un résultat dont l'expression fait intervenir une variable $x$, et si cette
1321 % démonstration n'a fait intervenir aucune hypothèse sur cette variable,
1322 % alors le résultat est vrai pour toute valeur de $x$. On appelle aussi
1323 % cette règle (il s'agira ultérieurement, en théorie de la
1324 % démonstration, d'une règle d'inférence) la règle d'introduction du
1325 % quantificateur universel.
1326
1327 % Le second est l'introduction du quantificateur existentiel. Autant le
1328 % premier est facilement utilisé (souvent abusivement\ldots) autant le
1329 % second 
1330 % est malaisé à saisir. 
1331 % %__________ 3.
1332
1333 % \section{Théorie de la démonstration en calcul des prédicats}
1334
1335 % %________________ 31.
1336
1337 % \subsection{Axiomes et règles d'inférence}
1338 % Pour élaborer la théorie de la démonstration en calcul des prédicats,
1339 % on reprend celle qui a été donnée en calcul propositionnel en ajoutant
1340 % les axiomes et les règles d'inférence qui permettent de traiter les
1341 % nouveaux symboles introduits (les quantificateurs).
1342
1343 % \begin{itemize}
1344
1345 % \item Nouveaux axiomes :
1346
1347 % \begin{itemize}
1348
1349 % \item Axiome 14: $(\qqs x\,  . \, A(x))\imp A(r)$
1350
1351 % \item Axiome 15: $A(r)\imp (\exi x\, . \, A(x))$
1352
1353 % \end{itemize}
1354 % [Dans les conditions indiquées au paragraphe précédent: substitution libre
1355 % de $x$ par $r$ dans $A$, $r$ étant libre pour $x$ dans $A$].
1356
1357 % \item Nouvelles règles d'inférence, avec $C$ sans occurrences libres
1358 %   de $x$:
1359
1360 % \begin{itemize}
1361
1362 % \item $\{C\imp A(x)\}\theor C\imp\qqs x\, . \, A(x)$ [règle d'introduction de
1363 % $\qqs$ ou règle-$\qqs$]
1364
1365 % \item $\{A(x)\imp C\}\theor\exi x\, . \, A(x)\imp C$ [règle d'introduction de
1366 % $\exi$ ou règle-$\exi$].
1367
1368 % \end{itemize}
1369 % \end{itemize}
1370
1371
1372
1373 % \subsection{Validité des résultats établis en calcul
1374 % propositionnel}
1375 % Le calcul propositionnel étant un sous-ensemble du calcul des
1376 % prédicats, tous les théorèmes établis en calcul propositionnel demeurent
1377 % établis en calcul des prédicats. 
1378 % Bref, tant que l'on n'utilise pas les symboles (quantificateurs), pas les axiomes
1379 % (14 et 15) ni les règles d'inférence (introductions de quantificateurs)
1380 % propres au calcul des prédicats, les démonstrations et déductions du
1381 % calcul des propositions s'étendent sans difficultés au calcul des
1382 % prédicats.
1383
1384 % Il ne faudrait pas en conclure hâtivement que les règles d'inférence vraies en
1385 % calcul propositionnel s'appliquent aussi en calcul des prédicats. 
1386 % A titre d'exemple, on va étudier le cas du méta-théorème de la déduction.
1387
1388 % %________________ 33.
1389
1390 % \begin{Th}[méta-théorème de la déduction]
1391 % En calcul des prédicats, on a:
1392 % $$
1393 % \textrm{Si } 
1394 % (B_1,B_2,\ldots,B_{n-1}) \theor B_n\imp C
1395 % \textrm{, alors }
1396 % (B_1,B_2,\ldots,B_n)\theor C
1397 % $$
1398 % \end{Th}
1399 % \begin{Proof}
1400 % De 
1401 % $(B_1,B_2,\ldots,B_{n-1}) \theor B_n\imp C$ et 
1402 % $(B_1,B_2,\ldots,B_{n-1},B_n)$ par modus ponens on en déduit
1403 % $C$.
1404 % \end{Proof}
1405
1406 % En général, la réciproque n'est  pas vraie. 
1407 % Cependant elle reste établie dans les cas suivants:
1408
1409 % \begin{itemize}
1410
1411 % \item 
1412 % lorsque la déduction de $C$ est faite \og à variables
1413 % constantes\fg{} (cette expression 
1414 % %malheureuse, mais consacrée, 
1415 % signifie %simplement
1416 % que la déduction
1417 % n'utilise aucune des 
1418 % règles d'introduction des quantificateurs, donc est faite comme en
1419 % calcul propositionnel).
1420 % \item 
1421 % lorsque les hypothèses de la déduction sont toutes des formules closes
1422 % (c'est à dire sans variables libres).
1423 % \end{itemize}
1424
1425
1426
1427 % \section{Le système formel \og \textit{PR}\fg{} }
1428
1429 % Il s'agit du système formel construit pour la formalisation  
1430 % du calcul des prédicats. Comme pour \og \textit{LP}\fg{} , le nombre de
1431 % symboles est 
1432 % réduit par rapport à celui du calcul des prédicats tel qu'il a été
1433 % décrit 
1434 % ci-dessus, dans le but d'obtenir plus d'efficacité en \og
1435 % démonstration automatique\fg{} .
1436
1437
1438
1439 % \subsection{Définition}
1440
1441 % \begin{itemize}
1442
1443 % \item L'alphabet $\Sigma_{\textit{PR}}$ est celui de \og
1444 %   \textit{LP}\fg{} , auquel on adjoint: 
1445
1446 % \begin{itemize}
1447
1448 % \item le symbole de quantificateur universel
1449 % \item des symboles de variables et d'individus (les \og constantes\fg{} )
1450 % \item des symboles opératoires et fonctionnels
1451
1452 % \end{itemize}
1453
1454 % \item Les formules sont celles du calcul des prédicat (limitées au
1455 % vocabulaire de \og \textit{PR}\fg{} )
1456 % \item Les (schémas d') axiomes sont au nombre de 5:
1457
1458 % \begin{itemize}
1459
1460 % \item Axiome 1: $A\imp(B\imp A)$
1461 % \item Axiome 2: $(A\imp(B\imp C))\imp((A\imp B)\imp(A\imp C))$
1462 % \item Axiome 3: $(\non B\imp\non A)\imp(A\imp B)$
1463 % \item Axiome 4: $(\qqs x\, . \, A(x)) \imp A(t)$
1464 % \item Axiome 5: $(C\imp B(x)) \imp (C\imp \qqs x\, . \, B(x))$ [$x$ n'étant pas
1465 % variable libre de $C$].
1466
1467 % \end{itemize}
1468
1469 % \item Il y a 2 règles d'inférence:
1470
1471 % \begin{itemize}
1472
1473 % \item Le \og modus ponens\fg{} $(A,A\imp B)\theor\ B$
1474 % \item La généralisation $A\theor\ \qqs x\, . \, A$.
1475
1476 % \end{itemize}
1477
1478 % \end{itemize}
1479
1480 % %________________ 42.
1481
1482 % % \subsection{Calcul des prédicats égalitaire}
1483
1484 % % Dans de nombreuses applications, notamment mathématiques, on a besoin de
1485 % %  l'égalité. La \og vraie\fg{} égalité, c'est à dire la capacité de
1486 % % reconnaissance de l'identité de deux objets, n'est pas une notion de
1487 % % logique du premier ordre (celle dont nous nous occupons ici). En effet,
1488 % % deux objets sont identiques lorsque toute propriété qui est vraie pour
1489 % % l'un est aussi vraie pour l'autre, et que toute propriété fausse pour
1490 % % l'un est aussi fausse pour l'autre. Autrement dit, pour définir
1491 % % l'égalité, il faudrait quantifier universellement un symbole de prédicat,
1492 % % écrire une formule qui pourrait ressembler à :\par
1493 % % \centerline{$(x=y)$ si et seulement si $\qqs p\,.\,(p(x)\eqv
1494 % %   p(y))$.}\par\noindent 
1495 % % Or, quantifier un symbole de prédicat n'est pas possible en calcul des
1496 % % prédicats du premier ordre. Donc, lorsqu'on a besoin d'une égalité, on se
1497 % % contente d'une égalité \og affaiblie\fg{} comme simple relation d'équivalence
1498 % % (réflexive, symétrique, transitive), donc comme un prédicat
1499 % % binaire, qu'il faudrait noter $\equiv(x,y)$ mais que l'on note $(x\equiv
1500 % % y)$. Bien entendu, il faut ajouter les axiomes qui fixent les propriétés
1501 % % de cette égalité, pour obtenir un calcul des prédicats égalitaire.
1502
1503 % % %________________ 43.
1504
1505 % %\subsection{Interprétations de \og \textit{PR}\fg{} }
1506
1507
1508 % %________________ 44.
1509
1510 % \subsection{Théorème de complétude de Gödel}
1511 % La démonstration est longue et repose sur un raisonnement par récurrence
1512 % sur la complexité de la formule (en gros, le nombre de connecteurs ou
1513 % quantificateurs qui interviennent dans celle-ci), après avoir démontré la
1514 % propriété individuellement pour chaque formule de complexité 1 (un seul
1515 % connecteur ou quantificateur). Toute la difficulté provient de la
1516 % cardinalité (du \og nombre d'éléments\fg{} ) de l'interprétation. Le
1517 % résultat est connu sous le nom de théorème de complétude de Gödel (1930).
1518 % \begin{Th}[Théorèmes de complétude de Gödel] $ $
1519 % \begin{itemize}
1520 % \item le système formel \og \textit{PR}\fg{} est complet:
1521 %   $$
1522 %   \tauto B  \textrm{ si et seulement si } \theor B 
1523 %   $$
1524 % \item sa généralisation aussi:
1525 %   $$
1526 %   F\tauto B \textrm{ si et seulement si } F\theor B$$
1527 % \end{itemize}
1528
1529 % \end{Th}
1530
1531 % \subsection{Satisfaisabilité et insatisfaisabilité}
1532
1533 % Soit $E$ l'interprétation de \og \textit{PR}\fg{} .
1534
1535 % \begin{itemize}
1536
1537 % \item une formule de \og \textit{PR}\fg{} est dite \emph{satisfaite} dans $E$
1538 %   chaque fois qu'il 
1539 % existe un ensemble de valeurs, choisies dans $E$, pour les variables libres
1540 % qui interviennent dans cette formule tel que la proposition qui en résulte
1541 % est \og vraie\fg{} .
1542
1543 % \item une formule de \og \textit{PR}\fg{} est dite \emph{valide} dans
1544 %   $E$ si, pour tout ensemble 
1545 % de valeurs, choisies dans $E$, pour les variables libres qui interviennent
1546 % dans $E$, la proposition qui en résulte est vraie.
1547
1548 % % \item une formule de \og \textit{PR}\fg{} est \emph{universellement valide ou est une thèse
1549 % % lorsqu'elle est valide dans toute interprétation. L'usage veut cependant
1550 % % que l'on conserve terme de tautologie (qui devrait être réservé au calcul
1551 % % propositionnel).
1552
1553 % \end{itemize}
1554
1555
1556
1557 % Soit $F$ un ensemble de formules de \og \textit{PR}\fg{} ; $F$ est dit
1558 % \emph{satisfaisable} s'il 
1559 % est possible de trouver une interprétation dans laquelle les formules de
1560 % $F$ sont simultanément satisfaites. Une telle interprétation
1561 % est appelée modèle de $F$. S'il n'est pas possible de
1562 % trouver un modèle pour l'ensemble de formules $F$, celui-ci est dit
1563 % \emph{insatisfaisable}, \emph{incohérent}, \emph{contradictoire}.
1564
1565 %  Ce sont ces notions d'insatisfaisabilité qui sont à
1566 % l'origine des méthodes de démonstration dites de réfutation.
1567 % Elles sont basées sur le théorème suivant.
1568 % \begin{Th}[Théorème de contradiction]
1569 % Soit $F$ un ensemble de formules closes et $B$ une formule close de 
1570 % \og \textit{PR}\fg{}. Alors, $F\theor B$ si et
1571 % seulement si $F\union\{\non B\}$ est insatisfaisable 
1572 % \end{Th}
1573
1574 % Ce théorème peut être démontré à l'aide du théorème de complétude.
1575
1576
1577  \gsaut
1578
1579 \centerline{\x{Fin du Chapitre}}
1580