forked from edukera-japanese-translation/translation
-
Notifications
You must be signed in to change notification settings - Fork 0
/
doc_fr.html
2785 lines (2785 loc) · 153 KB
/
doc_fr.html
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<div class="pedagogic paper" key="exercise_description_demo_bernoulli_1">
<!--{type="ex_title"}-->
<p> <span class="txtwrap slide" style="padding-top:15px"> <img src="./img/demo_bernoulli_1.png"> </span> </p>
<p> Les puissances de 2 sont minorées par les valeurs de l'exposant, c'est à dire que
<!--{type="expr" input="(pow 2 n) >= (plus n 1)"}-->, comme l'illustrent le graphe ci-contre et le tableau ci-dessous : </p>
<center>
<table class="borderblue">
S
<colgroup>
<col width="60">
<col width="60">
<col width="60">
</colgroup>
<tbody>
<tr>
<td><span class="bold">
<!--{type="expr" input="n"}--></span></td>
<td><span class="bold">
<!--{type="expr" input="n+1"}--></span></td>
<td><span class="bold">
<!--{type="expr" input="2^n"}--></span></td>
</tr>
<tr>
<td>
<!--{type="expr" input="0"}--></td>
<td>
<!--{type="expr" input="1"}--></td>
<td>
<!--{type="expr" input="1"}--></td>
</tr>
<tr>
<td>
<!--{type="expr" input="1"}--></td>
<td>
<!--{type="expr" input="2"}--></td>
<td>
<!--{type="expr" input="2"}--></td>
</tr>
<tr>
<td>
<!--{type="expr" input="2"}--></td>
<td>
<!--{type="expr" input="3"}--></td>
<td>
<!--{type="expr" input="4"}--></td>
</tr>
<tr>
<td>
<!--{type="expr" input="3"}--></td>
<td>
<!--{type="expr" input="4"}--></td>
<td>
<!--{type="expr" input="8"}--></td>
</tr>
<tr>
<td>...</td>
<td>...</td>
<td>...</td>
</tr>
</tbody>
</table>
</center>
<p> Cette inégalité est un cas particulier des <span class="exturl"><a href="https://fr.wikipedia.org/wiki/In%C3%A9galit%C3%A9_de_Bernoulli" target="_blank">inégalités de Bernoulli</a></span>, démontrées dans l'exercice ci-dessous : </p>
<p>
<!--{type="exercise" input="demo_bernoulli_2"}--> </p>
</div>
<div class="pedagogic paper" key="exercise_description_demo_bernoulli_2">
<!--{type="ex_title"}-->
<p>Ces inégalités généralisent le résultat du précédent exercice. Elles sont attribuées au mathématicien suisse <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Jacques_Bernoulli" target="_blank">Jacques Bernoulli</a></span>. On les appelle les <span class="exturl"><a href="https://fr.wikipedia.org/wiki/In%C3%A9galit%C3%A9_de_Bernoulli" target="_blank">inégalités de Bernoulli</a></span>.</p>
</div>
<div class="pedagogic paper" key="exercise_description_ineq_ex_8">
<!--{type="ex_title"}-->
<p>L'object est de démontrer le théorème d'addition terme à terme de deux inégalités. Ce théorème est donc verrouillé.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_connector_abs_peirce">
<!--{type="ex_title"}-->
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_01">
<!--{type="ex_title"}-->
<p>On démontre que la disjonction est distributive <span class="stress">sur la conjonction</span>.</p>
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_02">
<!--{type="ex_title"}-->
<p> On démontre que la conjonction est distributive <span class="stress">sur la disjonction</span>. </p>
<p> <span class="lock">w</span><span class="cons">Logique constructiviste</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_06">
<!--{type="ex_title"}-->
<p> Dans cet exercice, l'univers des éléments est l'ensemble des <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Entier_naturel" target="_blank">entiers naturels</a></span>. </p>
<p> Les formules sont appelées des <span class="stress">propositions définies sur ℕ</span>, et les éléments sont les entiers. </p>
<p> On note "
<!--{type="prop" sci="true" input="forall (x:Nvar), app_prop U P x"}-->" et "
<!--{type="prop" sci="true" input="exists (x:Nvar), app_prop U P x"}-->" les quantifications sur ℕ. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_08">
<!--{type="ex_title"}-->
<a href="https://fr.wikipedia.org/wiki/L%27%C3%89cole_d%27Ath%C3%A8nes" target="_blank"><img class="txtwrap" src="./img/aristote-raphael-ecole-d-athenes.jpg" height="30%" width="30%"></a>
<p> Le <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Syllogisme" target="_blank">syllogisme</a></span> est un raisonnement formalisé au 4<span class="sup">ème</span> siècle avant notre ère dans la <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Gr%C3%A8ce_antique" target="_blank">Grèce antique</a></span> par <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Aristote" target="_blank">Aristote</a></span> qui le considérait comme l'élément fondamental de la logique et du raisonnement. </p>
<p> Le syllogisme a servi, et sert encore, de fondation logique au <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Droit" target="_blank">Droit</a></span> qui est né dans la <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Rome_antique#La_R.C3.A9publique_romaine" target="_blank">Rome antique</a></span>. Il est le schéma sur lequel sont construits les jugements de droit dans la tradition occidentale. </p>
<p>Imaginons par exemple qu'un tribunal doive répondre à la question "Socrate est-il mortel ?". La réponse passe par la découverte d'un attribut "Homme". Posons les définitions :</p>
<table class="slide">
<colgroup>
<col width="150">
<col width="30">
<col width="150">
</colgroup>
<tbody>
<tr>
<td style="padding-top: 10px; border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">Terme mineur</td>
<td style="padding-top: 10px; border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">A</td>
<td style="padding-top: 10px; border-bottom: 1px solid whitesmoke;">Socrate</td>
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">Terme moyen</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">B</td>
<td style="border-bottom: 1px solid whitesmoke;">être un Homme</td>
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke;">Terme majeur</td>
<td style="border-right: 1px solid whitesmoke;">C</td>
<td>être mortel</td>
</tr>
</tbody>
</table>
<p>Le jugement est alors établi suivant le schéma ci-dessous :</p>
<table class="slide">
<colgroup>
<col width="150">
<col width="140">
<col width="250">
</colgroup>
<tbody>
<tr>
<td style="padding-top: 10px; border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Prémisse majeure</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">B ⇒ C</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;"> Tous les Hommes sont mortels. (Homme ⇒ mortel)</td>
<!-- <td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;">La règle de droit</td> -->
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Prémisse mineure</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">A ⇒ B</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Socrate est un Homme.</td>
<!-- <td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;"> La qualification juridique du terme mineur (Socrate) qui fait l’objet du procès.</td> -->
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Conclusion</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">A ⇒ C</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Socrate est mortel.</td>
<!-- <td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;">Le jugement</td> -->
</tr>
</tbody>
</table>
<p> L'enjeu du procès est donc la qualification ou non du terme mineur (l'accusé) en terme moyen. L'apprentissage de l'esprit des lois (le sens donné aux lois) permettant au juge de décider, se fait par l'étude de la <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Jurisprudence" target="_blank">jurisprudence</a></span> qui est l'ensemble des décisions de justice. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_12">
<!--{type="ex_title"}-->
<p>Cette implication n'est vraie qu'en logique classique. Cela ne pose pas de problème à son utilisation en électronique : soit le courant passe, soit il ne passe pas.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_13">
<!--{type="ex_title"}-->
<a href="./img/Diopsis.jpg" target="_blank"><img class="txtwrap" src="./img/Diopsis.jpg" height="30%" width="30%"></a>
<p>Les <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Lois_de_De_Morgan" target="_blank">lois de De Morgan</a></span> sont des formules permettant de calculer la négation de n'importe quelle proposition mathématique.</p>
<p>On démontre que la négation d'une disjonction est la conjonction des négations des opérandes.</p>
<p>Ces lois sont utilisées en informatique dans la conception des <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Fonction_logique" target="_blank">fonctions logiques</a></span> et de leur matérialisation physique sous forme notamment de <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Circuit_int%C3%A9gr%C3%A9">circuits intégrés</a></span>.</p>
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_14">
<!--{type="ex_title"}-->
<p> Un <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Op%C3%A9rateur_(symbole)" target="_blank">opérateur</a></span> binaire, noté par exemple ★, est <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Associativit%C3%A9" target="_blank">associatif</a></span> si quels que soient les <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Op%C3%A9rande" target="_blank">opérandes</a></span> a b c : </p>
<p>a ★ (b ★ c) = (a ★ b) ★ c</p>
<p>Leur position n'ayant pas d'importance, les parenthèses peuvent être omises. La valeur ci-dessus s'écrit donc a ★ b ★ c. C'est par exemple l'associativité de l'addition qui permet d'écrire 3 + 5 + 8 sans besoin de faire figurer des parenthèses.</p>
<p> <span class="lock">w</span><span class="cons">Logique constructiviste</span> </p>
<div class="slide">
<p>On démontre une équivalence en démontrant deux implications, par définition de l'équivalence. On choisit la définition <span class="buttontheo">équivalence</span> pour démontrer
<!--{type="tag" input="s0"}-->. </p>
</div>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_16">
<!--{type="ex_title"}-->
<p> La <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Proposition_contrapos%C3%A9e" target="_blank">contraposée</a></span>, ou modus tollens, consiste à démontrer A implique B en démontrant que la négation de B implique la négation de A : si on n'avait pas B, on n'aurait pas A, donc si on a A, on a B. </p>
<p> Ce raisonnement n'est vrai qu'en <span class="stress">logique classique</span>. En revanche, l'implication inverse,
<!--{type="prop" sci="true" input="(A -> B) -> (~B -> ~A)"}--> est vraie en logique constructiviste, comme on le démontre dans l'exercice suivant. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_17">
<!--{type="ex_title"}-->
<p>Dans ce sens, l'implication se démontre en logique constructiviste.</p>
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_27">
<!--{type="ex_title"}-->
<p>De manière similaire à l'associativité de la conjonction, on démontre l'associativité de la disjonction.</p>
<div class="slide">
<p>Démontrer la disjonction
<!--{type="prop" sci="true" input="or A B"}--> nécessite de <span class="stress">faire un choix</span> entre la démonstration de A et celle de B. </p>
<p>La méthode consiste choisir le plus tard possible, et à exploiter d'abord toutes les hypothèses (par disjonction de cas) pour obtenir le maximum d'information permettant de décider.</p>
</div>
<p> <span class="lock">w</span><span class="cons">Logique constructiviste</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_31">
<!--{type="ex_title"}-->
<p> Le <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Raisonnement_par_l%27absurde" target="_blank">raisonnement par l'absurde</a></span> consiste à démontrer une proposition A en montrant que si sa négation, ¬ A, est vraie, alors on obtient une contradiction : </p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Raisonnement par l'absurde</span>
<!--{type="prop" sci="true" input="forall A:Prop, ((~(~A)) -> A)"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p> En effet,
<!--{type="prop" sci="true" input="~(~A)"}--> se réécrit
<!--{type="prop" sci="true" input="(~A -> False)"}--> par définition de la négation. Le raisonnement par l'absurde est donc une règle d'élimination de la double négation. </p>
<p>On démontre dans cet exercice que le tiers exclu implique le raisonnement par l'absurde.</p>
<p></p>
<p> <span class="lock">w</span><span class="cons">Logique constructiviste</span> </p>
<p>L'implication réciproque est démontrée dans l'exercice ci-dessous. Ainsi, le raisonnement par l'absurde est équivalent au tiers exclu, et n'est donc pas admis en logique constructiviste : </p>
<p>
<!--{type="exercise" input="logic_quantifier_ex_le_48"}--> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_32">
<!--{type="ex_title"}-->
<p>On démontre que la disjonction de deux négations est la négation de la conjonction des propositions. Cette implication se fait en logique constructiviste, mais pas l'implication inverse comme on le constate dans l'exercice suivant.</p>
<p> <span class="lock">w</span><span class="cons">Logique constructiviste</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_33">
<!--{type="ex_title"}-->
<p>On démontre que la disjonction est distributive <span class="stress">sur l'implication</span>.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_34">
<!--{type="ex_title"}-->
<p>On démontre que la conjonction est "à moitié distributive" sur l'implication.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_connector_peirce_abs_te">
<!--{type="ex_title"}-->
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_connector_peirce_law">
<!--{type="ex_title"}-->
<p><a href="https://fr.wikipedia.org/wiki/Charles_Sanders_Peirce" target="_blank"><img class="txtwrap" src="./img/peirce.jpg" height="30%" width="30%"></a><span class="exturl"><a href="https://fr.wikipedia.org/wiki/Charles_Sanders_Peirce" target="_blank">Charles Sanders Peirce</a></span> est un sémiologue et philosophe américain de la seconde moitié du 19<span class="sup">ème</span> siècle. </p>
<p> La <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Loi_de_Peirce" target="_blank">loi de Peirce</a></span> est vrai en logique classique.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_tuto_01">
<!--{type="ex_title"}-->
<p>Que peut-on déduire de la conjonction "A ∧ B" ?</p>
<p><span class="light-bulb">A</span>Suivre les indications de résolution (appuyer sur le bouton avec une ampoule en haut à droite de l'écran).</p>
<!-- <p><span class="light-bulb">A</span>Un exercice possède une conclusion et un contexte initial qui pose les variables et les hypothèses.</p>
<p><span class="light-bulb">A</span>La conclusion et les hypothèses sont des <span class="exturl"><a href="http://fr.wikipedia.org/wiki/Proposition" target="_blank">propositions mathématiques</a></span>. L'objectif est d'élaborer un enchaînement de propositions appelé <span class="exturl"><a href="http://fr.wikipedia.org/wiki/D%C3%A9monstration_%28math%C3%A9matiques_%C3%A9l%C3%A9mentaires%29" target="_blank">démonstration</a></span>, permettant de justifier la conclusion.</p> -->
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_21">
<!--{type="ex_title"}-->
<p>Il existe en Ecosse un club très fermé qui obéit aux règles suivantes :</p>
<ul>
<li> Tout membre non écossais porte des chaussettes rouges.</li>
<li>Tout membre porte un kilt ou ne porte pas de chaussettes rouges.</li>
<li>Les membres mariés ne sortent pas le dimanche.</li>
<li>Un membre sort le dimanche si et seulement s’il est écossais.</li>
<li>Tout membre qui porte un kilt est écossais et marié.</li>
<li>Tout membre écossais porte un kilt.</li>
</ul>
<p>On démontre que ce club est si fermé qu’il ne peut accepter personne !</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_03">
<!--{type="ex_title"}-->
<p>On démontre que le complément d'une union est l'intersection des compléments.</p>
<p>On appelle cette formule une loi de De Morgan par analogie avec les lois de De Morgan établies pour les conjonctions et disjonctions. On constate en effet une similitude des propriétés (distributivité, associativité, commutativité) de l'union, de l'intersection et du complément, et celles de la disjonction, la conjonction et la négation respectivement.</p>
<p>Cette analogie résulte de la définition des opérateurs ensemblistes : l'appartenance à l'union de deux ensembles est la disjonction des appartenances à chacun des deux ensembles.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_07">
<!--{type="ex_title"}-->
<p>On achève la démonstration de la distributivité de la quatification existentielle sur la disjonction.</p>
<p> Il faut faire apparaître la valeur témoin inconnue <span class="button" style="font-family: 'Times New Roman'; font-weight: bold; font-size: 14px; padding: 3px;">x?</span> dans une portée (ou une sous-portée) qui contient la (les) variables(s) permettant de renseigner cette valeur témoin inconnue. Dans l'exemple ci-contre, la valeur témoin est fournie dans les portées créées <span class="buttontheo">par disjonction de cas</span>. Ce raisonnement est donc utilisé <span class="stress">avant</span> le raisonnement <span class="buttontheo">par construction</span>. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_09">
<!--{type="ex_title"}-->
<p>On montre que l'ensemble vide est un <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Inclusion_(math%C3%A9matiques)" target="_blank">sous-ensemble</a></span> de n'importe quel ensemble.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_easy_08">
<!--{type="ex_title"}-->
<p>Quelle est la négation logique d'une quantification universelle ?</p>
<p>La négation de "quel que soit x, F (x)" n'est pas "quel que soit x, non F (x)", mais "il existe x tel que non F (x)".</p>
<p>On démontre ici une des deux implications.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_easy_09">
<!--{type="ex_title"}-->
<p>Quelle est la négation logique d'une quantification existentielle ?</p>
<p>La négation de "il existe x tel que F (x)" n'est pas "il existe x tel que non F (x)", mais "quel que soit x, non F (x)".</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_01">
<!--{type="ex_title"}-->
<p>La relation binaire sur ℕ "être plus petit que", notée
<!--{type="prop" sci="true" input="app_rel rel_le x y"}-->, est définie dans ces exercices par une formule existentielle :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td> <span class="def">Etre plus petit que</span>
<!--{type="prop" sci="true" input="forall (x y:Nvar), equiv (app_rel rel_le x y) (exists (z:Nvar),y=x+z)"}--> </td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p>On démontre que l'addition est croissante pour cette relation.</p>
<p>Exercices "être plus petit que" :</p>
<p>
<!--{type="exercise" input="logic_quantifier_ex_le_02"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_03"}--></p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_02">
<!--{type="ex_title"}-->
<p>Exercices "être plus petit que" :</p>
<p>
<!--{type="exercise" input="logic_quantifier_ex_le_01"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_03"}--></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_04">
<!--{type="ex_title"}-->
<p> <span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 1 Eléments de logique</a></span></span> </p>
<p>Sur l'île des purs et des pires, il y a des habitants. Ces habitants sont soit des purs, soit des pires. Les purs disent toujours la vérité alors que les pires mentent toujours.</p>
<p> Montrer que si <span style="font-weight: bold">a</span> et <span style="font-weight: bold">b</span> sont deux habitants de l'île et que <span style="font-weight: bold">a</span> dit que <span style="font-weight: bold">b</span> est pire, alors au moins l'un des deux est pire. </p>
<p>On utilise l'axiome <span class="buttontheo">pur ou pire</span> pour générer deux cas : soit <span style="font-weight: bold">a</span> est pur, soit <span style="font-weight: bold">a</span> est pire. </p>
<!-- La théorie "vérités et
mensonges" est munie des axiomes suivants :
</p>
<table class="slide">
<colgroup>
<col width="25%">
<col width="75%">
</colgroup>
<tbody>
<tr>
<tr>
<td style="vertical-align: top"><span class="def"
style="padding-top: 20px">Nature Pure ou pire</span></td>
<td style="padding-top: 24px;"><span type="prop">forall
(a:gbmember), (or (is_good a) (is_bad a))</span></td>
</tr>
<td style="vertical-align: top; padding-top: 8px"><span
class="def">Vérité des purs</span></td>
<td><span type="prop" style="padding-top: 20px">forall
(a:gbmember) (P:Prop), (is_good a) -> (say a P) -> P</span></td>
</tr>
<tr>
<td style="vertical-align: top; padding-top: 8px"><span
class="def">Mensonge des pires</span></td>
<td><span type="prop">forall (a:gbmember) (P:Prop),
(is_bad a) -> (say a P) -> (~ P)</span></td>
</tr>
<tbody>
</table>-->
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_05">
<!--{type="ex_title"}-->
<p> <span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 1 Eléments de logique</a></span></span> </p>
<p> Montrer que si <span style="font-weight: bold">a</span> dit que <span style="font-weight: bold">a</span> et <span style="font-weight: bold">b</span> sont tous les deux pires, alors <span style="font-weight: bold">a</span> est pire. </p>
<p> Les exercices "vérités et mensonges" : </p>
<!--{type="exercise" input="logic_quantifier_ex_le_04"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_05"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_06"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_07"}-->
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_06">
<!--{type="ex_title"}-->
<p> <span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 1 Eléments de logique</a></span></span> </p>
<p> Montrer que si <span style="font-weight: bold">a</span> dit une
<!--{type="expr" input="False"}--> alors c'est un pire. </p>
<p></p> Les exercices "vérités et mensonges" :
<p></p>
<!--{type="exercise" input="logic_quantifier_ex_le_04"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_05"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_06"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_07"}-->
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_07">
<!--{type="ex_title"}-->
<p> <span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 1 Eléments de logique</a></span></span> </p>
<p>Montrer qu'un habitant ne peut pas dire qu'il est lui-même un pire.</p>
<p></p> Les exercices "vérités et mensonges" :
<p></p>
<!--{type="exercise" input="logic_quantifier_ex_le_04"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_05"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_06"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_07"}-->
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_13">
<!--{type="ex_title"}-->
<!-- <a href="https://fr.wikipedia.org/wiki/Principe_des_tiroirs" target="_blank"><img class="txtwrap" src="http://img.1.im6.fr/03E8000007913469-photo-dressing-tiroir-casiers-chaussettes.jpg" height="30%" width="30%"></img></a> -->
<span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 2 Relations et fonctions</a></span></span>
<p> En 1834, le mathématicien allemand <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Johann_Peter_Gustav_Lejeune_Dirichlet" target="_blank">Johann Dirichlet</a></span> énonça le <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Principe_des_tiroirs" target="_blank">principe des tiroirs</a></span>, qui s'applique dans le cas où n chaussettes occupent m tiroirs : </p>
<p style="align: center; font-style: italic">Si n > m, alors au moins un tiroir doit contenir strictement plus d'une chaussette.</p>
<p> Autrement dit, par <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Proposition_contrapos%C3%A9e" target="_blank">contraposée</a></span>, si chaque tiroir contient au plus une chaussette, alors n <= m. </p>
<p> Considérons une <span class="stress">fonction f de rangement</span> de n+1 chaussettes, indexées de 0 à n, dans des tiroirs : elle prend en argument l'indice d'une chaussette et retourne l'indice d'un tiroir. La condition qu'un tiroir contient au plus une chaussette, se traduit par le fait que la fonction de rangement est <span class="stress">injective</span> : deux chaussettes se rangent dans deux tiroirs différents. De plus, puisque par hypothèse m tiroirs contiennent les chaussettes, il existe une chaussette, indicée x, telle que f(x)=m. </p>
<p>Démontrer le principe des tiroirs consiste donc à démontrer que si la fonction f est injective sur l'ensemble [0 ... n], alors il existe une chaussette indicée x, telle que son tiroir, f(x), est supérieur ou égal à n.</p>
<p>Pour simplifier, on va raisonner sur une notion plus forte que l'injectivité et considérer des fonctions strictement croissantes :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td>
<!--{type="prop" sci="true" input=" forall (n:Nvar) (f:NvarFun), equiv (FFMono n f) (forall (x y:Nvar), ExprLT x y -> ExprLT y n -> ExprLT (app_fun f x) (app_fun f y))"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p>On démontre ci-contre que la croissance stricte est bien une condition plus forte que l'injectivité sur [0 ... n], qui s'exprime ici de la manière suivante :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td>
<!--{type="prop" sci="true" input="forall (n:Nvar) (f:NvarFun), equiv (FFInj n f) (forall (x y:Nvar), ExprLT x n -> ExprLT y n -> app_fun f x = app_fun f y -> nvar x = nvar y)"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p>Le principe des tiroirs est démontré dans l'exercice suivant à partir de la croissance stricte de la fonction de rangement.</p>
<p> </p>
<h3>Résolution</h3>
<p> Effectuer un raisonnement à base de cas à l'aide de
<!--{type="tag" input="2"}-->. </p>
<p>Utiliser les raisonnements ci-dessous sur les égalités et les inégalités :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Symétrie de l'égalité</span>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (x=y) (y=x))"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (x<>y) (y<>x))"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Réécriture symétrique de l'inégalité</span>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (ExprGT x y) (ExprLT y x))"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (ExprGTEQ x y) (ExprLTEQ y x))"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Inégalité stricte</span>
<!--{type="prop" sci="true" input="forall (x y:O1U), (ExprGT x y) -> (x <> y)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y:O1U), (ExprLT x y) -> (x <> y)"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_14">
<!--{type="ex_title"}-->
<span class="def">source : <span class="exturl"><a href="http://www.lri.fr/~paulin/MathInfo" target="_blank">TP 2 Relations et fonctions</a></span></span>
<p>Le principe des tiroirs est présenté dans l'exercice précédent. Il s'agit de démontrer que si une fonction est injective sur [0 .. n], alors il existe x dans [0 ... n] tel que f(x) ≥ n. </p>
<p>On a démontré précédemment qu'une condition suffisante pour être injective sur [0 ... n] est d'être strictement croissante sur [0 ... n].</p>
<p>Le principe des tiroirs est démontré ci-contre avec l'hypothèse de croissance stricte.</p>
<div class="slide">
<p> Utiliser un raisonnement par récurrence sur n. </p>
</div>
<p>Les théorèmes suivants sont disponibles pour transformer une inégalité entre deux entiers en une inégalité stricte, et inversement :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Transition vers l'entier suivant</span>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (ExprGT x y) (ExprGTEQ x (y+1)))"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y:O1U), (equiv (ExprGTEQ x y) (ExprGT (x+1) y))"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p>Les différentes formes de la transitivité des relations d'ordres permettent également d'introduire ou d'éliminer des inégalités, strictes ou non :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Transitivité</span>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGT x y) -> (ExprGT y z) -> (ExprGT x z)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGTEQ x y) -> (ExprGT y z) -> (ExprGT x z)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGT x y) -> (ExprGTEQ y z) -> (ExprGT x z)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGTEQ x y) -> (ExprGTEQ y z) -> (ExprGTEQ x z)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGT x y) -> (ExprGTEQ y z) -> (ExprGTEQ x z)"}--><br><br>
<!--{type="prop" sci="true" input="forall (x y z:O1U), (ExprGTEQ x y) -> (ExprGT y z) -> (ExprGTEQ x z)"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_27">
<!--{type="ex_title"}-->
<p>Ce résultat est disponible dans les autres exercices en tant que <span class="buttontheo">caratérisation ensembliste</span> d'une relation transitive.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_31">
<!--{type="ex_title"}-->
<p> Utiliser la caractérisation ensembliste d'une relation transitive, et la conservation de l'inclusion par composition. </p>
<p> <span class="light-bulb">A</span>Sélectionner un terme avec la souris dans une proposition permet de le remplacer par un autre terme ; il faut alors pouver l'égalité avec le terme remplacé. </p>
<h3>Voir également</h3>
<p>
<!--{type="exercise" input="logic_quantifier_ex_le_27"}-->
<!--{type="exercise" input="logic_quantifier_ex_le_47"}--> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_47">
<!--{type="ex_title"}-->
<p>La composition conserve l'inclusion.</p>
<p> Ce résultat est disponible dans les autres exercices en tant que combinaison par <span class="buttontheo">composition</span>. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_48">
<!--{type="ex_title"}-->
<p>On démontre la règle du tiers exclu en supposant admis le raisonnement par l'absurde.</p>
<p><span class="lock">w</span><span class="cons">Logique constructiviste</span></p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_71">
<!--{type="ex_title"}-->
<p>Madame Confuse a trois enfants, Alice Bill et Carl.</p>
<p>Quand on lui demande l'âge de ses enfants, Mme Confuse répond qu'Alice est la plus jeune, à moins que Bill le soit, et que si Carl n'est pas le plus jeune alors Alice est la plus âgée.</p>
<p>Quel est l'enfant le plus jeune, quel est l'enfant le plus âgé ?</p>
<!-- <h3>Formalisation</h3> -->
<p>On suppose que les enfants sont différents et qu'il n'ont pas le même âge.</p>
<p><span class="light-bulb">A</span>La réponse de Mme Confuse est modélisée par les hypothèses <span class="propid">4</span> et <span class="propid">5</span>.</p>
<p>Utiliser les axiomes ci-contre pour déterminer l'enfant le plus jeune.</p>
<!-- <p>De plus, si un enfant est le plus vieux (le plus jeune), alors il n'est pas le plus jeune (le plus âgé) :</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td>
<span class="def">Antonymie</span>
<span type="prop">forall (x:Child), (Youngest x) -> (~(Oldest x))</span><br></br>
<span type="prop">forall (x:Child), (Oldest x) -> (~(Youngest x))</span>
</td>
</tr>
<tbody>
</table>
<p>Enfin, si un enfant est le plus jeune (le plus âgé), alors n'importe quel autre enfant n'est pas le plus jeune (le plus âgé)</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td>
<span class="def">Unicité</span>
<span type="prop">forall (x y:Child), (x <> y) -> (Youngest x) -> (~(Youngest y))</span><br></br>
<span type="prop">forall (x y:Child), (x <> y) -> (Oldest x) -> (~(Oldest y))</span>
</td>
</tr>
<tbody>
</table> -->
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_72">
<p> <span class="def">source : <span class="exturl"> <a href="http://images.math.cnrs.fr/Coqito-ergo-sum.html" target="_blank"> Aurélien Alvarez pour lemonde.fr </a> </span> </span> </p>
<h2 style="margin-top:0">Enoncé</h2>
<p style="position:relative;left:-30px"><iframe frameborder="0" width="400" height="225" src="http://www.dailymotion.com/embed/video/xzpqbm" allowfullscreen></iframe><br></p>
<h2>Solution</h2>
<p style="position:relative;left:-30px"><iframe frameborder="0" width="400" height="225" src="http://www.dailymotion.com/embed/video/xzpqco" allowfullscreen></iframe></p>
<p><span class="stress">A vous de jouer !</span> résolvez l'énigme à l'aide de l'axiomatique mise à disposition.</p>
</div>
<div class="pedagogic paper" key="exercise_description_sigma_ex_15">
<!--{type="ex_title"}-->
<p>Si on considère la suite des n premiers entiers ordonnés du plus grand au plus petit, on constate que la somme du ième élément de cette suite et du ième premier entier est égale à n+1, quel que soit i. </p>
<p>Le tableau ci-dessous illustre ce phénomène (la dernière colonne est la somme des autres) : </p>
<table class="borderblue">
<colgroup>
<col width="80">
<col width="15">
<col width="15">
<col width="15">
<col width="15">
<col width="140">
</colgroup>
<tbody>
<tr>
<td><span class="bold">Croissant</span></td>
<td>
<!--{type="expr" input="1"}--></td>
<td>
<!--{type="expr" input="2"}--></td>
<td><span>...</span></td>
<td>
<!--{type="expr" input="n"}--></td>
<td>
<!--{type="expr" input="S"}--></td>
</tr>
<tr>
<td><span class="bold">Décroissant</span></td>
<td>
<!--{type="expr" input="n"}--></td>
<td>
<!--{type="expr" input="n-1"}--></td>
<td><span>...</span></td>
<td>
<!--{type="expr" input="1"}--></td>
<td>
<!--{type="expr" input="S"}--></td>
</tr>
<tr>
<td><span class="bold">Somme</span></td>
<td>
<!--{type="expr" input="n+1"}--></td>
<td>
<!--{type="expr" input="n+1"}--></td>
<td><span>...</span></td>
<td>
<!--{type="expr" input="n+1"}--></td>
<td>
<!--{type="expr" input="2*S"}--> =
<!--{type="expr" input="n*(n+1)"}--></td>
</tr>
</tbody>
</table>
<p>Utiliser le <span class="buttontheo">parcours à rebours</span> pour obtenir la somme des entiers du plus grand au plus petit
<!--{type="expr" style="vertical-align:-3px;" input="(sigma(k,0,n,n-k))"}-->.</p>
<p><span class="lock">w</span> La formule <span class="buttontheo">premiers entiers</span> est verrouillée dans cet exercice.</p>
</div>
<div class="pedagogic paper" key="exercise_description_sigma_ex_16">
<!--{type="ex_title"}-->
<p>Utiliser l'identité <span class="propid">1</span> le plus tôt possible. Cette identité s'obtient en développant
<!--{type="expr" input="(n+1)^3"}--> :</p>
<table>
<colgroup>
<col width="500">
</colgroup>
<tbody>
<tr>
<td style="border-color: whitesmoke;">
<!--{type="expr" input="(n+1)^3"}--> <span style="margin : 5px">=</span>
<!--{type="expr" input="(n+1)*((n^2)+(2*n)+1)"}--> <span style="margin : 5px">=</span>
<!--{type="expr" input="(n^3)+(3*(n^2))+(3*n)+1"}--> </td>
</tr>
</tbody>
</table>
<p><span class="lock">w</span> La formule <span class="buttontheo">premiers carrés</span> est verrouillée dans cet exercice.</p>
</div>
<div key="help_description_icon_exercises_check">
<p>exercice résolu. Cliquer sur 'commencer' pour charger la solution.</p>
</div>
<div key="help_description_icon_exercises_difficulty">
<p>difficulté de l'exerices (le nombre de flammes, de 0 à 3, indique le niveau de difficulté).</p>
</div>
<div key="help_description_icon_exercises_lighbulb">
<p>Indications (les exercices de didacticiel offrent ce service)</p>
</div>
<div key="help_description_icon_exercises_lock">
<p>Verrou. L'obtention des cocardes 'didacticiel' du chapitre courant (et éventuellement des chapitres prérequis) permet de débloquer l'accès à l'exercice.</p>
</div>
<div key="help_description_icon_trophy_all">
<p>La cocarde 'universel' est obtenue lorsque tous les exercices du chapitre sont résolus.</p>
</div>
<div key="help_description_icon_trophy_diagnostic">
<p>La cocarde 'express' est obtenue lorsque tous les exercices marqués 'express' sont résolus. L'obtention de cette cocarde rend accessibles dans le diagnostic les théorèmes du chapitres.</p>
</div>
<div key="help_description_icon_trophy_tutorial">
<p>La cocarde 'didacticiel' est obtenue lorsque tous les exercices de didacticiel sont résolus.</p>
</div>
<div key="help_description_icon_trophy_unavoidable">
<p>La cocarde 'Incontournable' est obtenue lorsque tous les exercices incontournables du chapitre sont résolus.</p>
</div>
<div key="help_description_shortcut_browsing_left_scope">
<p>Afficher la portée à gauche de la portée courante</p>
</div>
<div key="help_description_shortcut_browsing_lower_prop">
<p>Déplacer le focus sur la propostion en dessous de la proposition courante</p>
</div>
<div key="help_description_shortcut_browsing_open_scope">
<p>Ouvrir la portée de justification</p>
</div>
<div key="help_description_shortcut_browsing_redo">
<p>Exécuter l'étape de démonstration annulée</p>
</div>
<div key="help_description_shortcut_browsing_right_scope">
<p>Afficher la portée à droite de la portée courante.</p>
</div>
<div key="help_description_shortcut_browsing_undo">
<p>Annuler la dernière étape de démonstration</p>
</div>
<div key="help_description_shortcut_browsing_upper_prop">
<p>Déplacer le focus sur la proposition au dessus de la proposition courante.</p>
</div>
<div key="help_description_shortcut_commutativity_commut_left">
<p>Sélectionner le terme à gauche.</p>
</div>
<div key="help_description_shortcut_commutativity_commut_mode">
<p>Activer le mode commutativité au clavier.</p>
</div>
<div key="help_description_shortcut_commutativity_commut_right">
<p>Sélectionner le terme de droite.</p>
</div>
<div key="help_description_shortcut_commutativity_commut_shift_left">
<p>Déplacer le terme sélectionné à gauche.</p>
</div>
<div key="help_description_shortcut_commutativity_commut_shift_right">
<p>Déplacer le terme sélectionné à droite.</p>
</div>
<div key="help_description_shortcut_commutativity_enter_commut">
<p>Appliquer l'ordre des termes pour la commutativité.</p>
</div>
<div key="help_description_shortcut_commutativity_esc_commut">
<p>Sortir du mode commutativité au clavier.</p>
</div>
<div key="help_description_shortcut_evar_enter_evar">
<p>Affecter une valeur à une inconnue de raisonnement</p>
</div>
<div key="help_description_shortcut_evar_esc_evar">
<p>Sortir du mode affectation d'une inconnue de raisonnement au clavier</p>
</div>
<div key="help_description_shortcut_evar_evar_left">
<p>Sélectionner l'inconnue de raisonnement précédente</p>
</div>
<div key="help_description_shortcut_evar_evar_mode">
<p>Activer le mode affectation d'une inconnue de raisonnement au clavier</p>
</div>
<div key="help_description_shortcut_evar_evar_right">
<p>Sélectionner l'inconnue de raisonnement suivante</p>
</div>
<div key="help_description_shortcut_proof_context">
<p>Afficher/cacher le contexte (propositions des autres portées disponibles en déduction) </p>
</div>
<div key="help_description_shortcut_proof_deduce">
<p>Ouvrir la fenêtre de diagnostic en déduction</p>
</div>
<div key="help_description_shortcut_proof_enter">
<p>Effectuer une des actions suivantes :</p>
<ul>
<li style="font-size:14px">Ouvrir la fenêtre de diagnostic en déduction si la proposition est justifiée</li>
<li style="font-size:14px">Ouvrir la fenêtre de diagnostic en justification si la proposition n'est pas justifiée</li>
<li style="font-size:14px">Unifier avec la proposition proposée par la copie numérique</li>
</ul>
</div>
<div key="help_description_shortcut_proof_justify">
<p>Effectuer une des actions suivantes :</p>
<ul>
<li style="font-size:14px">Ouvrir la fenêtre de diagnostic en justification si la proposition n'est pas justifiée</li>
<li style="font-size:14px">Afficher le théorème dans la boîte à outil si la proposition est justifiée</li>
</ul>
</div>
<div key="help_description_shortcut_selection_enter_select">
<p>Ouvrir la fenêtre de diagnostic de réécriture du terme sélectionné</p>
</div>
<div key="help_description_shortcut_selection_esc_select">
<p>Sortir du mode sélection au clavier</p>
</div>
<div key="help_description_shortcut_selection_group_select">
<p>Marquer le terme sélectionné comme groupe (permet de garder le terme intact lors des réécritures)</p>
</div>
<div key="help_description_shortcut_selection_select_down">
<p>Sélectionner le premier argument</p>
</div>
<div key="help_description_shortcut_selection_select_left">
<p>Sélectionner l'argument précédent</p>
</div>
<div key="help_description_shortcut_selection_select_mode">
<p>Activer le mode sélection au clavier</p>
</div>
<div key="help_description_shortcut_selection_select_right">
<p>Sélectionner l'argument suivant</p>
</div>
<div key="help_description_shortcut_selection_select_shift_left">
<p>Augmenter la sélection avec l'argument précédent</p>
</div>
<div key="help_description_shortcut_selection_select_shift_right">
<p>Augmenter la sélection avec l'argument suivant</p>
</div>
<div key="help_description_shortcut_selection_select_up">
<p>Sélectionner la fonction dont l'argument est le terme sélectionné</p>
</div>
<div key="help_description_shortcut_unification_enter_union">
<p>Unifier avec la proposition sélectionnée</p>
</div>
<div key="help_description_shortcut_unification_esc_union">
<p>Sortir du mode unification au clavier</p>
</div>
<div key="help_description_shortcut_unification_left_union">
<p>Sélectionner la propostion à gauche</p>
</div>
<div key="help_description_shortcut_unification_right_union">
<p>Sélectionner la proposition à droite</p>
</div>
<div key="help_description_shortcut_unification_union_mode">
<p>Activer le mode unfication au clavier</p>
</div>
<div key="help_section_description_browsing">
<p>Le raisonnement est présenté dans le style de la déduction naturelle : les propositions justifiées sont disposées les unes sous les autres, avec les hypothèses en tête et la conclusion en dernier.</p>
<p>Une justification est un théorème appliqué à des propositions qui se situent au-dessus de la propostion justifiée. Une justification peut également être un raisonnement, qui se trouve alors dans une autre portée logique (représentée par un onglet).</p>
<p>On navigue dans la copie à la souris, ou en mettant le focus sur la proposition souhaitée à l'aide des raccourcis clavier ci-dessous :</p>
</div>
<div key="help_section_description_commutativity">
<p>Lorsque l'on choisit la réécriture par commutativité, on spécifie l'ordre des termes soit à la souris par glisser-lâcher, soit à l'aide des raccourcis clavier ci-dessous :</p>
</div>
<div key="help_section_description_evar">
<p>L'application de certains théorèmes peut faire apparaître dans la copie des inconnues de raisonnement (un identifiant dans une pastille bleue)</p>
<p>On renseigne les valeurs de ces inconnues soit en cliquant dessus, soit à l'aide des raccourcis clavier ci-dessous :</p>
</div>
<div key="help_section_description_exercises">
<!--TODO-->
</div>
<div key="help_section_description_proof">
<p>Plusieurs actions de démonstration sont possibles :</p>
<ul>
<li style="font-size:14px">Justifier (si la proposition n'est pas déjà justifiée)</li>
<li style="font-size:14px">Unifier (si des propositions unifiables sont proposées)</li>
<li style="font-size:14px">Déduire</li>
<li style="font-size:14px">Supprimer (si la proposition n'est pas utilisée par une justification)</li>
<li style="font-size:14px">Déplacer par glisser-lâcher de l'indice de la proposition (sous contrainte du style déductif : une proposition ne peut être qu'au dessus d'une proposition qui l'utilise dans sa justification)</li>
</ul>
<p>Les raccourcis clavier ci-dessous sont disponibles :</p>
</div>
<div key="help_section_description_selection">
<p>Les opérations de réécriture (développement, factorisation, ...) sont possibles en sélectionnant le terme à réécrire</p>
<p>La sélection se fait soit à la souris, soit à l'aide des raccourcis clavier ci-dessous :</p>
</div>
<div key="help_section_description_trophy">
<!--TODO-->
</div>
<div key="help_section_description_unification">
<p>Lorsque plusieurs unifications sont possibles, il faut sélectionner la proposition adéquate, soit à la souris, soit à l'aide des raccourcis clavier ci-dessous :</p>
</div>
<div key="pager_account"></div>
<div class="pager" key="pager_algebra">
<a href="https://fr.wikipedia.org/wiki/%C3%89variste_Galois" target="_blank"><img class="txtwrap" src="./img/Evariste_galois.jpg" height="20%" width="20%"></a>
<p>Les <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Structure_alg%C3%A9brique" target="_blank">structures algébriques</a></span> sont les objets d'étude de ce chapitre.</p>
<p> Au début du XIX<span class="sup">ème</span> siècle, <span class="exturl"><a href="https://fr.wikipedia.org/wiki/%C3%89variste_Galois" target="_blank">Evariste Galois</a></span> introduit le concept de <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Groupe_(math%C3%A9matiques)" target="_blank">groupe</a></span>. </p>
</div>
<div key="pager_algebra_structures"></div>
<div class="pager" key="pager_analysis">
<a href="https://fr.wikipedia.org/wiki/Augustin_Louis_Cauchy" target="_blank"><img class="txtwrap" src="./img/Augustin-Louis_Cauchy_1901.jpg" height="12%" width="12%"></a>
<p> Au cours du 19<span class="sup">ème</span> siècle, les mathématiciens posent les bases de l’analyse des propriétés des fonctions réelles (fonctions à valeur réelle) : continutité, convergence, limite, dérivation, intégration, ... </p>
<p></p>
<p> En France dès le début du siècle, <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Augustin_Louis_Cauchy" target="_blank">Augustin Louis Cauchy</a></span> étudie notamment les propriétés de convergence des suites croissantes positives, introduites dans ce chapitre. En Allemagne, <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Bernhard_Riemann" target="_blank">Bernhard Riemann</a></span> et <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Karl_Weierstrass" target="_blank">Karl Weierstrass</a></span> élaborent les théories de l’intégration et des limites de fonction. </p>
</div>
<div class="pager" key="pager_analysis_induction">
<p> Le <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Raisonnement_par_r%C3%A9currence" target="_blank">raisonnement par récurrence</a></span> est un raisonnement incontournable, simple et puissant. Il permet de démontrer qu’une proposition P(n), dépendant d’un indice n, est vraie quelle que soit la valeur de l’indice, c’est à dire notamment vraie pour une infinité de valeurs de l’indice n. </p>
<p> Par exemple, sans le raisonnement par récurrence, il faudrait une infinité de calculs (ou une très grande quantité) pour avoir la certitude (ou quasi-certitude) que la proposition “
<!--{type="expr" input="4^n - 1"}--> est divisible par 3” est vraie quelle que soit la valeur de n, alors qu’un raisonnement par récurrence donne la certitude en quelques lignes de démonstration. </p>
</div>
<div class="pager" key="pager_analysis_limits">
<p>La limite d’une fonction en un point ou en l’infini est introduite formellement. La méthode de calcul par composition de limites est présentée : par exemple, sous certaines conditions, la limite d’une somme est la somme des limites. Cette méthode permet de calculer la limite de n’importe quelle fonction par décomposition en fonctions élémentaires, dont on connaît les valeurs limites. </p>
</div>
<div class="pager" key="pager_analysis_series">
<p> Une suite est une fonction de ℕ dans ℝ. On introduit ici quelques propriétés fondamentales des ces fonctions : </p>
<ul>
<li>croissance, décroissance</li>
<li>majoration, minoration</li>
<li>convergence, divergence</li>
</ul>
</div>
<div key="pager_badges"></div>
<div key="pager_credits"></div>
<div key="pager_dashboard"></div>
<div class="custom pager" key="pager_demo_seg">
<p>Le calcul algébrique consiste à transformer une relation d'égalité (ou d'inégalité), entre des nombres réels ou des vecteurs par exemple. L'enjeu est d'élaborer une séquence de transformations (factorisation, développement, ...) pour démontrer certaines propriétés mathématiques.</p>
</div>
<div class="pager" key="pager_eq_seg">
<p>Une égalité peut se transformer, notamment à l’aide des transformations introduites dans ce chapitre :</p>
<ul>
<li>les opérations à gauche et à droite, qui permettent de “passer un terme de l’autre côté” en changeant son signe</li>
<li>les combinaisons d’égalité, qui permettent typiquement de résoudre des systèmes d’équation</li>
<li>le passage au carré, ou le passage à la racine carrée (si la valeur est positive), ...</li>
</ul>
</div>
<div class="pager" key="pager_ineq_seg">
<p>Les inégalités comparent deux nombres réels. Elles se transforment de manière similaire aux égalités :</p>
<ul>
<li>opérations à gauche et à droite</li>
<li>combinaisons (addition, soustraction)</li>
<li>applications de fonctions (opposé, carré, racine, …)</li>
<li>…</li>
</ul>
<p>Si la transformation appliquée à gauche et à droite d’une inégalité est une fonction décroissante, le sens de l’inégalité entre les valeurs obtenues est inversé.</p>
</div>
<div class="pager" key="pager_logic">
<p>Les règles de formation des <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Proposition" target="_blank">propositions</a></span>, et les règles de raisonnement associées, forment un système logique, appelé <span class="exturl"><a href="https://fr.wikipedia.org/wiki/D%C3%A9duction_naturelle" target="_">déduction naturelle</a></span>, utilisé notamment dans l'élaboration des <span class="exturl"><a href="https://fr.wikipedia.org/wiki/D%C3%A9monstration_(math%C3%A9matiques_%C3%A9l%C3%A9mentaires)" target="_blank">démonstrations</a></span> mathématiques.</p>
<p>La valeur de ce système tient notamment dans le fait qu’il est indépendant de la théorie étudiée. Une théorie est l'ensemble des axiomes (théorèmes admis) définissant des objets et leurs propriétés.</p>
</div>
<div class="pager" key="pager_logic_connector">
<p>Les connecteurs logiques sont des éléments fondamentaux pour former des propositions mathématiques à partir de deux propositions quelconques A et B :</p>
<ul>
<li>l’implication, A implique B, notée "A ⇒ B"</li>
<li>la conjonction, A et B, notée "A ∧ B"</li>
<li>la disjonction, A ou B, notée "A ∨ B"</li>
<li>la négation, non A, notée "¬ A"</li>
</ul>
<p>Chacun de ces connecteurs est associé à deux régles :</p>
<ul>
<li>une règle permettant de justifier (ou démontrer) la proposition : comment justifier "A ∧ B" ?</li>
<li>une règle permettant de déduire une nouvelle proposition : que peut on déduire de "A ∧ B" ?</li>
</ul>
</div>
<div class="pager" key="pager_logic_function">
<p>Une fonction f d'une variable x d'un univers A, est une procédure de calcul d'un élément y d'un univers B telle que la proposition "y=f(x)" est une relation fonctionnelle de A vers B.</p>
</div>
<div class="pager" key="pager_logic_quantifier">
<p>Les propositions mathématiques peuvent également être des formules avec des variables prenant certaines valeurs : par exemple “3 est un nombre premier” peut être considéré comme la formule “x est un nombre premier” où la variable “x” prend la valeur “3”.</p>
<p>Pour une formule à variable, on a besoin d’exprimer que la proposition obtenue est vraie <span class="stress" style="font-size:16px">quelle que soit</span> la valeur de la variable, ou qu’<span class="stress" style="font-size:16px">il existe</span> au moins une valeur pour laquelle la proposition est vraie. Ces nouveaux éléments de langage sont les quantificateurs.</p>
</div>
<div class="pager" key="pager_logic_relation">
<p>Les relations, omniprésentes en mathématiques, sont des formules mettant en relation deux valeurs appartenant à deux univers, potentiellement différents. On parle de relation binaire lorsque les valeurs appartiennent au même univers.</p>
<p>La caractérisation ensembliste des relations, ainsi que leurs propriétés, sont présentées.</p>
</div>
<div class="pager" key="pager_rewrite_seg">
<p>Les réécritures permettent de déduire d’une égalité, une égalité presque identique dans laquelle un terme
<!--{type="expr" input="a"}--> est remplacé par un terme
<!--{type="expr" input="b"}-->, à condition que
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="a = b"}-->. Les réécritures de a en b sont données par le calcul algébrique :</p>
<ul>
<li>factorisation, développement</li>
<li>idéntitiés remarquables</li>
<li>simplifications</li> ...
</ul>
<p>Par exemple, on peut déduire de
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="x=(2*(x-1))"}--> la proposition
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="x= (2*x) - 2"}--> en remplaçant le terme
<!--{type="expr" input="2*(x-1)"}--> par
<!--{type="expr" input="minus (2*x) 2"}--> ; on sait en effet que
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="(2*(x-1)) = ((2*x)-2)"}--> par développement.</p>
</div>
<div class="pager" key="pager_set_operators">
<p>Un ensemble E est une collection d'objets qu'on appelle <span class="stress" style="font-size:16px">les éléments</span> de E.</p>
<p>La proposition qu'un élément x appartient à E, ou est élément de E, se note <span class="stress" style="font-size:16px">
<!--{type="prop" sci="true" input="sis_element x E"}--></span>. La négation de l'appartenance, ¬(
<!--{type="prop" sci="true" input="sis_element x E"}-->), se note <span class="stress" style="font-size:16px">
<!--{type="prop" sci="true" input="~sis_element x E"}--></span>. </p>
<p>Un <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Op%C3%A9ration_ensembliste" target="blank">opérateur ensembliste</a></span> permet de construire un ensemble à partir d'autres ensembles.</p>
</div>
<div class="pager" key="pager_set_rewoperators">
<p>Les calculs algébriques sur les ensembles ressemblent aux calculs sur les nombres parce que : </p>
<ul>
<li>les opérations ensemblistes (intersection, union, ...) ont des propriétés similaires aux opérations numériques (addition, multiplication, ...) : associativité, commutativité, distributivité, ... </li>
<li>l'égalité ensembliste et l'égalité numérique sont des relations d'équivalence qui sont transitives, symétriques et réflexives (voir section suivante)</li>
</ul>
<p>L'algèbre ensembliste est équivalente à l'<span class="exturl"><a href="https://fr.wikipedia.org/wiki/Alg%C3%A8bre_de_Boole_(logique)" target="_blank">algèbre booléenne</a></span> : soit un élement appartient à un ensemble, soit il n'y appartient pas. Cette algèbre est centrale en informatique, dans l'écriture des programmes et dans l'élaboration des circuits électroniques. </p>
</div>
<div class="pager" key="pager_settheory">
<a href="https://fr.wikipedia.org/wiki/Georg_Cantor" target="_blank"><img class="txtwrap" src="./img/cantor.jpg" height="12%" width="12%"></a>
<p> A la fin du 19<span class="sup">ème</span> siècle, le mathématicien allemand <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Georg_Cantor" target="_blank">Georg Cantor</a></span> élabore la <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Th%C3%A9orie_des_ensembles" target="_blank">théorie des ensembles</a></span>. Elle permet de définir les éléments fondamentaux des mathématiques, notamment les nombres entiers, les nombres réels, les fonctions ... </p>
<p>En 1930, le mathématicien austro-hongrois <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Kurt_G%C3%B6del" target="_blank">Kurt Gödel</a></span> montre même que n'importe quelle théorie peut se traduire dans la théorie des ensembles. </p>
</div>
<div class="pager" key="pager_sigma_seg">
<p>La notation sigma sert à faire la somme des termes d’une série de n nombres indéxés notés
<!--{type="expr" input="app_series a i"}--> (avec l'indice i compris entre 1 et n typiquement). Cette somme se note :
<!--{type="expr" style="vertical-align: -4px;" input="(sigma(k,1,n,(app_series a k)))"}-->.</p>
<p>Dans cette notation, l'indice k est une variable muette : elle n'est pas déclarée dans le contexte et n'est valable que pour l'expression sommée.</p>
<p>Les propriétés du sigma sont celles de l’addition (associativité, distributivité de la multiplication, …) et celles des changements d’écriture de l’indexation des nombres sommés.</p>
</div>
<div key="slide_demo_tuto_app_(3 * x - 6 = zero,lradd,0)">
<!-- (3 * x - 6 = zero,lradd,0)
by Forward lradd)
-->
<div expr="(3 * x - 6 = zero,lradd,0)" class="pedagogic slide" exercise="demo_tuto_app">
<p>L'objectif est d'<span class="stress">isoler
<!--{type="expr" input="pow x 2"}--></span> à gauche. On commence donc par isoler x à gauche comme dans les exercices précédents, puis on passe au carré à gauche et à droite.</p>
</div>
</div>
<div key="slide_demo_tuto_app_(3 * x = 6,lrdiv,0)">
<!-- (3 * x = 6,lrdiv,0)
by Forward lrdiv)
-->
<div expr="(3 * x = 6,lrdiv,0)" class="pedagogic slide" exercise="demo_tuto_app">
<p>On divise par 3 à gauche et à droite pour isoler x.</p>
</div>
</div>
<div key="slide_demo_tuto_app_(x = 2,app_square,0)">
<!-- (x = 2,app_square,0)
by Forward app_square)