forked from benperso/translation
-
Notifications
You must be signed in to change notification settings - Fork 1
/
doc_en.html
2701 lines (2701 loc) · 141 KB
/
doc_en.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> The powers of two are bound from above by the values of the exponent, i.e. that
<!--{type="expr" input="(pow 2 n) >= (plus n 1)"}-->, as is illustrated in the graph opposite. </p>
<center>
<table class="borderblue">
<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> This inequality is a specific example of <span class="exturl"><a href="https://en.wikipedia.org/wiki/Bernoulli%27s_inequality" target="_blank">Bernoulli’s inequalities</a></span>, demonstrated in the following exercise: </p>
<p>
<!--{type="exercise" input="demo_bernoulli_2"}--> </p>
<p> <span class="light-bulb">ń</span> Use reasoning <span class="buttontheo">by induction</span>. </p>
</div>
<div class="pedagogic paper" key="exercise_description_demo_bernoulli_2">
<!--{type="ex_title"}-->
<p> These inequalities generalize the result see previously. They are attributed to the Swiss mathematician, <span class="exturl"><a href="https://en.wikipedia.org/wiki/Jacob_Bernoulli" target="_blank">Jacques Bernoulli</a></span>. We call them the <span class="exturl"><a href="https://en.wikipedia.org/wiki/Bernoulli%27s_inequality" target="_blank">Bernoulli’s inequality</a></span>. </p>
<p> <span class="light-bulb">ń</span> Use reasoning by induction. </p>
</div>
<div class="pedagogic paper" key="exercise_description_ineq_ex_8">
<!--{type="ex_title"}-->
</div>
<div class="pedagogic paper" key="exercise_description_logic_connector_abs_peirce">
<!--{type="ex_title"}-->
<p><span class="lock">w</span><span class="cons">Constructive logic</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_01">
<!--{type="ex_title"}-->
<p>We can demonstrate that disjunction is distributive <span class="stress">over conjunction</span>.</p>
<p><span class="lock">w</span><span class="cons">Constructive logic</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_02">
<!--{type="ex_title"}-->
<p> It can be shown that conjunction is distributive <span class="stress">over disjunction</span>. </p>
<p> <span class="lock">w</span><span class="cons">Constructive logic</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_06">
<!--{type="ex_title"}-->
<p> In this exercise, the universe of elements is made up of all <span class="exturl"><a href="https://en.wikipedia.org/wiki/Natural_number" target="_blank">natural numbers</a></span>. </p>
<p> The formulae are the <span class="stress">propositions defined on ℕ</span>, and the elements are the integers. </p>
<p> Note "
<!--{type="prop" sci="true" input="forall (x:Nvar), app_prop U P x"}-->" and "
<!--{type="prop" sci="true" input="exists (x:Nvar), app_prop U P x"}-->" quantifications on ℕ. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_08">
<!--{type="ex_title"}-->
<a href="https://en.wikipedia.org/wiki/The_School_of_Athens" target="_blank"><img class="txtwrap" src="./img/aristote-raphael-ecole-d-athenes.jpg" height="30%" width="30%"></a>
<p> The <span class="exturl"><a href="https://en.wikipedia.org/wiki/Syllogism" target="_blank">syllogism</a></span> is a reasoning formalized in the 4<span class="sup">th</span> Century BC in <span class="exturl"><a href="https://en.wikipedia.org/wiki/Ancient_Greece" target="_blank">Ancient Greece</a></span> par <span class="exturl"><a href="https://en.wikipedia.org/wiki/Aristotle" target="_blank">Aristotle</a></span> who considered it a fundamental element of logic and reasoning. </p>
<p> The syllogism served, and continues to serve, as a logical foundation to <span class="exturl"><a href="https://en.wikipedia.org/wiki/Law" target="_blank">Legislation</a></span>, born in <span class="exturl"><a href="https://en.wikipedia.org/wiki/Ancient_Rome#Republic" target="_blank">Ancient Rome</a></span>. It is the scheme on which legal judgements are constructed in western tradition. </p>
<p>Let’s imagine, for example that a tribunal must respond to the question "Is Socrates mortal?". The answer lies in the discovery of un attribute "man". Let’s lay out the definitions:</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;">Minor term</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;">Socrates</td>
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">Middle term</td>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke;">B</td>
<td style="border-bottom: 1px solid whitesmoke;">being a man</td>
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke;">Major term</td>
<td style="border-right: 1px solid whitesmoke;">C</td>
<td>being mortal</td>
</tr>
</tbody>
</table>
<p>It is therefore judged following the schema below:</p>
<table class="slide">
<colgroup>
<col width="200">
<col width="90">
<col width="250">
<col width="250">
</colgroup>
<tbody>
<tr>
<td style="padding-top: 10px; border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Major premise</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;"> All men are mortals. (man ⇒ mortal)</td>
<td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;">The rule of law</td>
</tr>
<tr>
<td style="border-right: 1px solid whitesmoke; border-bottom: 1px solid whitesmoke; vertical-align: middle;">Minor premise</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;">Socrates is a man.</td>
<td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;"> The legal qualification of the minor term (Socrates), which is subject to the proceedings.</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;">Socrates is mortal.</td>
<td style="border-bottom: 1px solid whitesmoke; vertical-align: middle;">The judgement</td>
</tr>
</tbody>
</table>
<p> The challenge the process presents is therefore qualifying (or not) the minor term (the accused) as a middle term. Learning the spirit of the laws (the meaning given to the laws) allows the judge to decide, by studying <span class="exturl"><a href="https://en.wikipedia.org/wiki/Case_law" target="_blank">case law</a></span> that is the set of court decisions. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_12">
<!--{type="ex_title"}-->
<p>This implication is only true in classical logic. This poses no problem to its use in electronics : either the current flows or it doesn’t.</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>The <span class="exturl"><a href="https://en.wikipedia.org/wiki/De_Morgan%27s_laws" target="_blank">De Morgan's laws</a></span> are formulae that allow us to calculate the negation of any mathematical proposition.</p>
<p>We can demonstrate that the negation of a disjunction is the conjunction of the negations of the operands.</p>
<p>These laws are used in IT within the conception of <span class="exturl"><a href="https://en.wikipedia.org/wiki/Logic_gate" target="_blank">logical functions</a></span> and and their physical materialization, notably in the form of <span class="exturl"><a href="https://en.wikipedia.org/wiki/Integrated_circuit">integrated circuits</a></span>.</p>
<p><span class="lock">w</span><span class="cons">Constructive logic</span></p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_14">
<!--{type="ex_title"}-->
<p> A binary <span class="exturl"><a href="https://en.wikipedia.org/wiki/Operator_(mathematics)" target="_blank">operator</a></span> noted, for example, ★, is <span class="exturl"><a href="https://en.wikipedia.org/wiki/Associative_property" target="_blank">associative</a></span> if, whatever the <span class="exturl"><a href="https://en.wikipedia.org/wiki/Operand" target="_blank">operands</a></span> a b c : </p>
<p>a ★ (b ★ c) = (a ★ b) ★ c</p>
<p>Since their position is not important; brackets can be omitted. Hence the value above is written a ★ b ★ c. It is, for example, the associativity of addition that allows us to write 3 + 5 + 8 without the need for brackets.</p>
<p> <span class="lock">w</span><span class="cons">Constructive logic</span> </p>
<div class="slide">
<p> <span class="light-bulb">ń</span> By definition, an equivalence is demonstrated by demonstrating two implications. Definition of <span class="buttontheo">equivalence</span> is chosen to demonstrate
<!--{type="tag" input="s0"}-->. </p>
</div>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_16">
<!--{type="ex_title"}-->
<p> <span class="exturl"><a href="https://en.wikipedia.org/wiki/Contraposition" target="_blank">Contraposition</a></span>, or modus tollens, consists of demonstrating that A implies B, by demonstrating that the negation of B implies the negation of A: if B didn’t stand, A wouldn’t stand, therefore if A stands, then B stands. </p>
<p> This reasoning only applies within <span class="stress">classical logic</span>. However, the inverse implication,
<!--{type="prop" sci="true" input="(A -> B) -> (~B -> ~A)"}--> is true in constructive logic, as demonstrated in the following exercise. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_17">
<!--{type="ex_title"}-->
<p><span class="lock">w</span><span class="cons">Constructive logic</span></p>
<p>This way, the implication is demonstrated using constructive logic.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_27">
<!--{type="ex_title"}-->
<p>Associativity of conjunction is demonstrated in a similar way to associativity of disjunction.</p>
<div class="slide">
<p> <span class="light-bulb">ń</span> Demonstrating disjunction of
<!--{type="prop" sci="true" input="or A B"}--> requires <span class="stress">choosing</span> between the demonstration of A or B. </p>
<p>The method consists of choosing as late as possible, and then exploiting all hypotheses (by disjunction of cases) in order to obtain the maximum amount of information that allows us to make the choice.</p>
</div>
<p> <span class="lock">w</span><span class="cons">Constructive logic</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_31">
<!--{type="ex_title"}-->
<p> <span class="exturl"><a href="https://en.wikipedia.org/wiki/Reductio_ad_absurdum" target="_blank">Ad absurdium reasoning</a></span> consists of demonstrating a proposition A by showing that if its negation, ¬ A, is true, then we obtain a contradiction: </p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Ad absurdium reasoning</span>
<!--{type="prop" sci="true" input="forall A:Prop, ((~(~A)) -> A)"}--></td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p> In effect,
<!--{type="prop" sci="true" input="~(~A)"}--> can be re-written as
<!--{type="prop" sci="true" input="(~A -> False)"}--> by definition of negation. Ad absurdium reasoning is therefore a law of elimination of double negation. </p>
<p>This exercise demonstrates that the excluded middle involves ad absurdium reasoning.</p>
<p> <span class="lock">w</span><span class="cons">Constructive logic</span> </p>
<p>Reciprocal implication is demonstrated in the exercise below. As a result, ad absurdium reasoning is equivalent to the excluded middle, and is therefore not acknowledged by constructive logic:</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>We can demonstrate that disjunction of two negations is the negation of conjunction of the propositions. This implication is made with constructive logic, but not the inverse implication, as shown in the next exercise.</p>
<p> <span class="lock">w</span><span class="cons">Constructive logic</span> </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_33">
<!--{type="ex_title"}-->
<p>It can be demonstrated that disjunction is distributive <span class="stress">over implication</span>.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_ex_easy_34">
<!--{type="ex_title"}-->
<p>It can be demonstrated that conjunction is "half distributive" over 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">Constructive logic</span></p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_connector_peirce_law">
<!--{type="ex_title"}-->
<a href="https://en.wikipedia.org/wiki/Charles_Sanders_Peirce" target="_blank"><img class="txtwrap" src="./img/peirce.jpg" height="30%" width="30%"></a>
<p> <span class="exturl"><a href="https://en.wikipedia.org/wiki/Peirce%27s_law" target="_blank">Peirce's law</a></span> is true in classical logic. <span class="exturl"><a href="https://en.wikipedia.org/wiki/Charles_Sanders_Peirce" target="_blank">Charles Sanders Peirce</a></span> was an American philosopher, logician and mathematician. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_connector_tuto_01">
<!--{type="ex_title"}-->
<p>What can be deduced from the conjunction "A ∧ B"?</p>
<p>Follow the instructions to solve the problem.</p>
<p> <span class="light-bulb">A</span>Each exercise has a conclusion and an initial context, which lays out the variables and the hypothesis. </p>
<p> <span class="light-bulb">A</span>The conclusion and the hypothesis are <span class="exturl"><a href="https://en.wikipedia.org/wiki/Statement_(logic)" target="_blank">mathematical statements</a></span>. The objective is to come up with a series of statements, which make up the <span class="exturl"><a href="https://en.wikipedia.org/wiki/Mathematical_proof" target="_blank">proof</a></span> that the conclusion is true. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_21">
<!--{type="ex_title"}-->
<p>In Scotland, a private club has the following rules:</p>
<ul>
<li>Every non-Scottish member wears red socks.</li>
<li>Every member wears a kilt or doesn't wear red socks.</li>
<li>The married members don't go out on Sunday.</li>
<li>A member goes out on Sunday if and only if he is Scottish.</li>
<li>Every member who wears a kilt is Scottish and married.</li>
<li>Every Scottish member wears a kilt.</li>
</ul>
<p>Now, we show that these rules are so strict that no one can be accepted!</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_03">
<!--{type="ex_title"}-->
<p>It is demonstrated that the complement of a union is the intersection of the complements.</p>
<p>We call this formula a De Morgan law by analogy with the De Morgan laws established for conjunctions and disjunctions. There are indeed similarities between the properties (distributivity, associativity, commutativity) of the union, of the intersection and of the complement, and those of the disjunction, the conjunction and the negation respectively.</p>
<p>This is a consequence of the definition of the set operators: belonging to a union of two sets is the disjunction of membership to each of the two sets.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_07">
<!--{type="ex_title"}-->
<p>The demonstration of the distributivity of the existential quantifier over disjunction is concluded.</p>
<p> <span class="light-bulb">ń</span> It is necessary to generate the unknown witness variable <span class="button" style="font-family: 'Times New Roman'; font-weight: bold; font-size: 14px; padding: 3px;">x?</span> within the scope (or a sub-scope) that contains the variable(s) allowing us to figure out this unknown witness value. In this example, the witness value is provided within the scopes created <span class="buttontheo">by using disjunction of cases</span>. This reasoning is therefore used before reasoning <span class="buttontheo">by construction</span>. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_09">
<!--{type="ex_title"}-->
<p>It can be shown that the empty set <span class="exturl"><a href="https://en.wikipedia.org/wiki/Subset" target="_blank">subset</a></span> of any set.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_easy_08">
<!--{type="ex_title"}-->
<p>What is the logical negation of a universal quantification?</p>
<p>The negation of "for every x, F (x)" is not "for every x, not F (x)", but "there exists x such that F (x)".</p>
<p>Here, one of the two implications is demonstrated.</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_easy_09">
<!--{type="ex_title"}-->
<p>What is the logical negation of an existential quantification?</p>
<p>The negation of "there exists x, such that F (x)" is not "there exists x, such that not F (x)", but “for every value x, not F (x)".</p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_01">
<!--{type="ex_title"}-->
<p>The binary relation on ℕ "is less than", noted
<!--{type="prop" sci="true" input="app_rel rel_le x y"}-->, is defined in these exercises by an existential formula:</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td> <span class="def">Is less than</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>We can demonstrate that addition is increasing for this relation.</p>
<p>"Is less than" exercises:</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>"Is less than" Exercises:</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>There are two kinds of people on a mysterious island. There are so-called honestants who always speak the truth, and the others are swindlecants who always lie.</p>
<p> Show that if <span style="font-weight: bold">a</span> and <span style="font-weight: bold">b</span> are two people on the island and that if <span style="font-weight: bold">a</span> says that <span style="font-weight: bold">b</span> is lying, at least one of the two is a swindlecant. </p>
<p> <span class="light-bulb">ń</span> The axiom <span class="buttontheo">speaking the truth or lying</span> is used to generate two cases: either <span style="font-weight: bold">a</span> is honestant, or <span style="font-weight: bold">a</span> is swindlecant. The theory "Honestants and Swindlecants" is made up of the following axioms: </p>
<table class="slide">
<colgroup>
<col width="25%">
<col width="75%">
</colgroup>
<tbody>
<tr>
</tr>
<tr>
<td style="vertical-align: top"><span class="def" style="padding-top: 20px">Honestants and Swindlecants</span></td>
<td style="padding-top: 24px;">
<!--{type="prop" input="forall (a:gbmember), (or (is_good a) (is_bad a))"}--></td>
</tr>
<tr>
<td style="vertical-align: top; padding-top: 8px"><span class="def">The truth told by the honestant</span></td>
<td>
<!--{type="prop" style="padding-top: 20px" input="forall (a:gbmember) (P:Prop), (is_good a) -> (say a P) -> P"}--></td>
</tr>
<tr>
<td style="vertical-align: top; padding-top: 8px"><span class="def">The lie told by the swindlecant</span></td>
<td>
<!--{type="prop" input="forall (a:gbmember) (P:Prop), (is_bad a) -> (say a P) -> (~ P)"}--></td>
</tr>
</tbody>
<tbody>
</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> Show that if <span style="font-weight: bold">a</span> says that <span style="font-weight: bold">a</span> and <span style="font-weight: bold">b</span> are both swindlecants, then <span style="font-weight: bold">a</span> is a swindlecant. </p>
<p> "Honestants and Swindlecants" exercises: </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> Show that if <span style="font-weight: bold">a</span> says
<!--{type="expr" input="False"}--> then he is a swindlecant. </p>
<p></p> Exercises "Honestants and Swindlecants" :
<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>Show that a person living on the island cannot say that he himself is a swindlecant.</p>
<p></p> Exercises "Honestants and Swindlecants" :
<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> In 1834, the German mathematician <span class="exturl"><a href="https://en.wikipedia.org/wiki/Peter_Gustav_Lejeune_Dirichlet" target="_blank">Johann Dirichlet</a></span> announced the <span class="exturl"><a href="https://en.wikipedia.org/wiki/Pigeonhole_principle" target="_blank">pigeonhole principle</a></span>, which applies to the case in which n pigeons occupy m holes: </p>
<p style="align: center; font-style: italic">If n > m, then at least one hole must contain strictly more than one pigeon.</p>
<p> In other words, by <span class="exturl"><a href="https://en.wikipedia.org/wiki/Contraposition" target="_blank">contraposition</a></span>, if each hole contains at the most one pigeon, then n <= m. </p>
<p> Let’s consider <span class="stress">the storage function</span> of n+1 pigeons, indexed from 0 to n, in holes: this function takes the index of a pigeon as argument, and returns an index of a hole. The assumption that a hole contains at the most one pigeon, translates into f being an <span class="stress">injective function</span> (the fiber of a hole has at most one element). Furthermore, given that by hypothesis, m holes contain the pigeons, there is one pigeon, indexed x, such that f(x)=m. </p>
<p>Demonstrating the pigeonhole principle therefore consists of demonstrating that if the function f is injective over the set [0 ... n], then there is one pigeon numbered x, such that its hole, f(x), is greater or equal to n.</p>
<p>To simplify this, we can reason with a notion stronger than injectivity and consider strictly increasing functions:</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>Opposite, it is demonstrated that the strict increase is a stronger condition than injectivity over [0 ... n], which is expressed here in the following way :</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>The pigeonhole principle is demonstrated in the following exercise, following the strict increase of the storage function.</p>
<p> </p>
<h3>Solution</h3>
<p> <span class="light-bulb">ń</span> Use a case base reasoning with the help of
<!--{type="tag" input="2"}-->. </p>
<p>Use theorems below on equalities and inequalities:</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Symmetry</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">Inequality rewritings</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">Strict inequality</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>The pigeonhole principle is presented in the previous exercise. It is do with demonstrating that if a function is injective over [0 .. n], then there exists x in [0 ... n] such that f(x) ≥ n.</p>
<p> We have previously demonstrated that a sufficient condition for being injective over [0 ... n] is to be strictly increasing over [0 ... n]. </p>
<p>The pigeonhole principle is demonstrated opposite, using a strictly increasing function as the hypothesis.</p>
<div class="slide">
<p> <span class="light-bulb">ń</span> Use reasoning by recurrence over n. </p>
</div>
<p>The theorems below enable us to transform an inequality between two integers to a strcit inequality, and vice versa:</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Transition to the next integer</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>The different forms of transitivity of comparison operators also enable us to introduce or eliminate strict inequalities from inequalities, and vice versa:</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td><span class="def">Transitivity</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>This result is available in the other exercises, as <span class="buttontheo">set characterization</span> of a transitive relation.</p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_31">
<!--{type="ex_title"}-->
<p> <span class="light-bulb">ń</span> Use the characterization of a transitive relation, and the conservation of inclusion by composition. </p>
<p> <span class="light-bulb">A</span>Selecting a term in a proposition with the cursor allows you to replace it with another term; it is therefore necessary to prove that it is equal to the original term. </p>
<h3>Also see</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>Composition conserves inclusion.</p>
<p> This result is available in other exercises, as "combination by <span class="buttontheo">composition</span>" rule. </p>
</div>
<div class="custom pedagogic" key="exercise_description_logic_quantifier_ex_le_48">
<!--{type="ex_title"}-->
<p>The law of excluded middle is demonstrated by assuming ad absurdium rule (double negation elimination).</p>
<p><span class="lock">w</span><span class="cons">Constructive logic</span></p>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_71">
<!--{type="ex_title"}-->
<p>Mrs. Muddled has three children, Alice, Bill, and Carl.</p>
<p>When asked her 3 children's ages, Mrs. Muddled said that Alice is the youngest unless Bill is, and that if Carl isn't the youngest then Alice is the oldest.</p>
<p> Who is the oldest and who is the youngest?</p>
<h3>Theory</h3>
<p>Information given by Mrs. Muddled is provided by assumptions <span class="propid">4</span> et <span class="propid">5</span></p>
<p>There’s some implicit meaning in the superlative words “youngest” and “oldest” provided by the following rules : </p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td> <span class="def">Antonymy</span>
<!--{type="prop" input="forall (x:Child), (Youngest x) -> (~(Oldest x))"}--><br><br>
<!--{type="prop" input="forall (x:Child), (Oldest x) -> (~(Youngest x))"}--> </td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
<p>Finally, “youngest” and “oldest” are opposites. Since there is more than one child, no one can be both.</p>
<table class="slide">
<colgroup>
<col width="100%">
</colgroup>
<tbody>
<tr>
<td> <span class="def">Uniqueness</span>
<!--{type="prop" input="forall (x y:Child), (x <> y) -> (Youngest x) -> (~(Youngest y))"}--><br><br>
<!--{type="prop" input="forall (x y:Child), (x <> y) -> (Oldest x) -> (~(Oldest y))"}--> </td>
</tr>
</tbody>
<tbody>
</tbody>
</table>
</div>
<div class="pedagogic paper" key="exercise_description_logic_quantifier_ex_le_72">
<!--{type="ex_title"}-->
</div>
<div class="pedagogic paper" key="exercise_description_sigma_ex_15">
<!--{type="ex_title"}-->
</div>
<div class="pedagogic paper" key="exercise_description_sigma_ex_16">
<!--{type="ex_title"}-->
</div>
<div key="help_description_icon_exercises_check">
<p>exercise solved. Click 'Start' to load the solution.</p>
</div>
<div key="help_description_icon_exercises_difficulty">
<p>difficulty level from 0 (easy) -to 3 (hard).</p>
</div>
<div key="help_description_icon_exercises_lighbulb">
<p>Solution hints (tutorial exercises provide this service)</p>
</div>
<div key="help_description_icon_exercises_lock">
<p>Lock. Obtain the 'tutorial' cockade of current chapter (and possibly prerequisite chapters) to unblock exercise.</p>
</div>
<div key="help_description_icon_trophy_all">
<p>The 'universal' cockade is obtained when all exercises of the chapter are solved.</p>
</div>
<div key="help_description_icon_trophy_diagnostic">
<p>The 'express' cockade is obtained when all exercises marked 'express' are resolved. As a result, chapter theorems are available in the diagnosis window.</p>
</div>
<div key="help_description_icon_trophy_tutorial">
<p>The 'tutorial' cockade is obtained when all tutorial exercises are solved.</p>
</div>
<div key="help_description_icon_trophy_unavoidable">
<p>The cockade 'unavoidable' is obtained when all the exercises marked 'unavoidable' of the chapter are solved.</p>
</div>
<div key="help_description_shortcut_browsing_left_scope">
<p>Display scope to the left of current the scope</p>
</div>
<div key="help_description_shortcut_browsing_lower_prop">
<p>Move focus to the statement below</p>
</div>
<div key="help_description_shortcut_browsing_open_scope">
<p>Open justification scope</p>
</div>
<div key="help_description_shortcut_browsing_redo">
<p>Redo proof step</p>
</div>
<div key="help_description_shortcut_browsing_right_scope">
<p>Display scope to the right of the current scope</p>
</div>
<div key="help_description_shortcut_browsing_undo">
<p>Undo last proof step</p>
</div>
<div key="help_description_shortcut_browsing_upper_prop">
<p>Move focus to the statement above</p>
</div>
<div key="help_description_shortcut_commutativity_commut_left">
<p>Select term on the left</p>
</div>
<div key="help_description_shortcut_commutativity_commut_mode">
<p>Activate keybaord commutative mode</p>
</div>
<div key="help_description_shortcut_commutativity_commut_right">
<p>Select term on the right</p>
</div>
<div key="help_description_shortcut_commutativity_commut_shift_left">
<p>Move selected term to the left</p>
</div>
<div key="help_description_shortcut_commutativity_commut_shift_right">
<p>Move selected term to the right</p>
</div>
<div key="help_description_shortcut_commutativity_enter_commut">
<p>Apply terms reordering</p>
</div>
<div key="help_description_shortcut_commutativity_esc_commut">
<p>Exit keyboard commutative mode</p>
</div>
<div key="help_description_shortcut_evar_enter_evar">
<p>Assign a value to a proof variable</p>
</div>
<div key="help_description_shortcut_evar_esc_evar">
<p>Exit keyboard proof variable mode</p>
</div>
<div key="help_description_shortcut_evar_evar_left">
<p>Select previous proof variable</p>
</div>
<div key="help_description_shortcut_evar_evar_mode">
<p>Activate keyboard proof variable mode</p>
</div>
<div key="help_description_shortcut_evar_evar_right">
<p>Select next proof variable</p>
</div>
<div key="help_description_shortcut_proof_context">
<p>Show / hide context (statements from other scopes available for deduction) </p>
</div>
<div key="help_description_shortcut_proof_deduce">
<p>Open diagnostic window in deduction</p>
</div>
<div key="help_description_shortcut_proof_enter">
<p>Perform one of the following:</p>
<ul>
<li style="font-size:14px">Open diagnostic window in deduction if the statement is justified</li>
<li style="font-size:14px">Open diagnostic window in justification if the statement is not justified</li>
<li style="font-size:14px">Unify statement</li>
</ul>
</div>
<div key="help_description_shortcut_proof_justify">
<p>Perform one of the following:</p>
<ul>
<li style="font-size:14px">Open diagnostic window in justification if the statement is not justified</li>
<li style="font-size:14px">Display justification theorem in the toolbox if the proposal is justified</li>
</ul>
</div>
<div key="help_description_shortcut_selection_enter_select">
<p>Open diagnostics window to rewrite selected term</p>
</div>
<div key="help_description_shortcut_selection_esc_select">
<p>Exit keybaord selection mode</p>
</div>
<div key="help_description_shortcut_selection_group_select">
<p>Mark selected term as group (keep intact the term during rewriting)</p>
</div>
<div key="help_description_shortcut_selection_select_down">
<p>Select first argument</p>
</div>
<div key="help_description_shortcut_selection_select_left">
<p>Select previous argument</p>
</div>
<div key="help_description_shortcut_selection_select_mode">
<p>Activate keyboard selection mode</p>
</div>
<div key="help_description_shortcut_selection_select_right">
<p>Select next argument</p>
</div>
<div key="help_description_shortcut_selection_select_shift_left">
<p>Increase selection with term on the left</p>
</div>
<div key="help_description_shortcut_selection_select_shift_right">
<p>Increase selection with next terme</p>
</div>
<div key="help_description_shortcut_selection_select_up">
<p>Select the function whose argument is selected term</p>
</div>
<div key="help_description_shortcut_unification_enter_union">
<p>Unify with selected statement</p>
</div>
<div key="help_description_shortcut_unification_esc_union">
<p>Exit keyboard unification mode</p>
</div>
<div key="help_description_shortcut_unification_left_union">
<p>Select left statement</p>
</div>
<div key="help_description_shortcut_unification_right_union">
<p>Select right statement</p>
</div>
<div key="help_description_shortcut_unification_union_mode">
<p>Activate keyboard unfication mode</p>
</div>
<div key="help_section_description_browsing">
<p>The proof is presented in the style of natural deduction: justified statements are positioned on top of each other; assumptions are on top, and the conclusion is the last statement.</p>
<p>A justification is a theorem applied to statements above justified statement. A justification may also be a proof, which is then in another scope (represented by a tab).</p>
<p>One can navigate in the paper with the cursor, or with the keyboard thanks to keyboard shortcuts below:</p>
</div>
<div key="help_section_description_commutativity">
<p>When choosing commutative rewriting, one can reorder the terms with the curor by drag-and-drop, or with the keyboard thanks to keyboard shortcuts below:</p>
</div>
<div key="help_section_description_evar">
<p>Proof variables may appear when applying a theorem (a proof varaible is represented with a blue tag)</p>
<p>On can assign a value to a proof variable by clicking on it, or with keyboard shortcuts below:</p>
</div>
<div key="help_section_description_exercises">
<!--TODO-->
</div>
<div key="help_section_description_proof">
<p>Several proof actions are possible:</p>
<ul>
<li style="font-size:14px">Justify (if the proposal is not already justified)</li>
<li style="font-size:14px">Unify (if unifiable statements are proposed)</li>
<li style="font-size:14px">Deduce</li>
<li style="font-size:14px">Delete (if the proposal is not used by any justification)</li>
<li style="font-size:14px">Move by dragging and dropping the index tag of the statement (as long as the deductive style is respected : a statement used by a justification can only be above justified statement)</li>
</ul>
<p>Keyboard shortcuts are available:</p>
</div>
<div key="help_section_description_selection">
<p>Selecting a term allows to rewrite it (development, factoring, ...)</p>
<p>Term selection is done either with the cursor or with keyboard shortcuts below:</p>
</div>
<div key="help_section_description_trophy">
<!--TODO-->
</div>
<div key="help_section_description_unification">
<p>When several unifications are possible, select the appropriate statement with the cursor or with keyboard shortcuts below:</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>The <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Structure_alg%C3%A9brique" target="_blank">algebraic structures</a></span> are of this chapter study of objects.</p>
<p> In the early nineteenth <span class="sup">century,</span> <span class="exturl"><a href="https://fr.wikipedia.org/wiki/%C3%89variste_Galois" target="_blank">Evariste Galois</a></span> introduced the concept of <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Groupe_(math%C3%A9matiques)" target="_blank">group</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> During the <span class="sup">19th</span> century, mathematicians lay the foundations for analyzing the properties of real functions (functions in real terms): continutité, convergence, limits, differentiation, integration, ... </p>
<p></p>
<p> In France from the beginning of the century, <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Augustin_Louis_Cauchy" target="_blank">Augustin-Louis Cauchy</a></span> in particular studying the convergence properties of the positive increasing sequences, introduced in this chapter. In Germany, <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Bernhard_Riemann" target="_blank">Bernhard Riemann</a></span> , and <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Karl_Weierstrass" target="_blank">Karl Weierstrass</a></span> develop theories of integration and function limits. </p>
</div>
<div class="pager" key="pager_analysis_induction">
<p> <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Raisonnement_par_r%C3%A9currence" target="_blank">Mathematical induction</a></span> is a simple and yet very powerful theorem. It allows to prove that a proposition P (n) dependent on an index n, is true regardless of the value of the index, which means true for an infinite number of values of the index n. </p>
<p> For example, without induction, it would require a very large amount (if not infinite) of calculation steps to get confidant that P is true for any value of n, while induction provides with absolute certainty in a few proof steps. </p>
</div>
<div class="pager" key="pager_analysis_limits">
<p>The limit of a function at a point or at infinity is formally introduced. The calculation method by composition of limits is presented : for example under certain conditions, the limit of a sum is the sum of the limits. This method enables to compute the limit of any function by decomposing it into elementary functions with known limits. </p>
</div>
<div class="pager" key="pager_analysis_series">
<p> A series is a function of ℕ in ℝ. Here we introduce some fundamental properties of these functions: </p>
<ul>
<li>increasing decreasing monotonicities</li>
<li>upper and lower bounds</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>Calculus is about transforming an equality relation (or inequality), between real numbers or vectors for example. The challenge is to work out a sequence of algebraic manipulations (factorize, expand, ...) from assumption(s) to conclusion.</p>
</div>
<div class="pager" key="pager_eq_seg">
<p>A equality can be transformed, especially with the operations introduced in this chapter:</p>
<ul>
<li>left and right operations that can "pass a term to the other side" by changing its sign</li>
<li>combinations of equalities, typically to solve systems of equations</li>
<li>squaring, root squaring (if the value is positive), ...</li>
</ul>
</div>
<div class="pager" key="pager_ineq_seg">
<p>Inequalities compare two real numbers. They transform similarly to the equations with:</p>
<ul>
<li>operations to left and right sides</li>
<li>combinations (addition, subtraction)</li>
<li>functions (opposite, square root, ...)</li>
<li>...</li>
</ul>
<p>If the function applied to the left and right sides of an inequality is decreasing, then the sense of the inequality is reversed.</p>
</div>
<div class="pager" key="pager_logic">
<p> The grammar of <span class="exturl"><a href="https://en.wikipedia.org/wiki/Propositional_calculus" target="_blank">propositions</a></span>, and associated reasoning rules, form a logical system called <span class="exturl"><a href="https://en.wikipedia.org/wiki/Natural_deduction" target="_">natural deduction</a></span>, notably used for developing mathematical <span class="exturl"><a href="https://en.wikipedia.org/wiki/Mathematical_proof" target="_blank">demonstrations</a></span>. </p>
<p>This system is valuable because it is independent from the theory studied. A theory is the set of axioms (acknowledged theorems) defining objects and their properties.</p>
</div>
<div class="pager" key="pager_logic_connector">
<p>Logical connectors are fundamental elements for forming mathematical propositions from two propositions, whatever A and B are:</p>
<ul>
<li>implication, A implies B, noted "A ⇒ B"</li>
<li>conjunction, A and B, noted "A ∧ B"</li>
<li>disjunction, A or B, noted "A ∨ B"</li>
<li>negation, not A, noted "¬ A"</li>
</ul>
<p>Each of these connectors is associated with two rules:</p>
<ul>
<li>a rule to justify (or demonstrate) the proposition: how can we justify "A ∧ B" ?</li>
<li>a rule to deduce a new proposition: what can we deduce from "A ∧ B" ?</li>
</ul>
</div>
<div class="pager" key="pager_logic_function">
<p>A function f is a formula that has a value x, such that the proposition "y=f(x)" is a functional relation of x and y.</p>
</div>
<div class="pager" key="pager_logic_quantifier">
<p>Mathematical propositions can also be formulae with variables taking on certain values: for example "3 is a prime number" can be considered as the formula "x is a prime number" where the variable "x" is replaced by "3".</p>
<p> For a formula with a variable, we need to express that the proposition is true <span class="stress" style="font-size: 16px">for every</span> value the variable assumes, or that <span class="stress" style="font-size: 16px">there exists</span> at least one value for which the proposition is true. These new elements language are the quantifiers. </p>
</div>
<div class="pager" key="pager_logic_relation">
<p>Relations, omnipresent in mathematics, are formulae that relate two values belonging to two, potentially different, universes. We talk about binary relation when the values belong to the same universe.</p>
<p>The characterization of relations, as well as their properties, are presented.</p>
</div>
<div class="pager" key="pager_rewrite_seg">
<p>Rewriting operations allow to deduce a new equality, almost identical, in which a term
<!--{type="expr" input="a"}--> is replaced by a term
<!--{type="expr" input="b"}--> , provided
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="a = b"}--> . Rewriting of a to b is given by the algebraic calculation:</p>
<ul>
<li>factoring, expansion</li>
<li>remarkable identities</li>
<li>simplifications</li> ...
</ul>
<p>For example, one can deduce from
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="x=(2*(x-1))"}--> the statement
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="x= (2*x) - 2"}--> by replacing the term
<!--{type="expr" input="2*(x-1)"}--> by
<!--{type="expr" input="minus (2*x) 2"}--> ; we known that
<!--{type="prop" sci="true" style="vertical-align:-3px;" input="(2*(x-1)) = ((2*x)-2)"}--> by expansion.</p>
</div>
<div class="pager" key="pager_set_operators">
<p>A set E is a collection of objects that are called <span class="stress" style="font-size:16px">the elements</span> of E.</p>
<p>The proposition that an element x belongs to E, or is an element of E, is noted <span class="stress" style="font-size:16px">
<!--{type="prop" sci="true" input="sis_element x E"}--></span>. The negation of membership, ¬(
<!--{type="prop" sci="true" input="sis_element x E"}-->), is noted <span class="stress" style="font-size:16px">
<!--{type="prop" sci="true" input="~sis_element x E"}--></span>. </p>
<p>A <span class="exturl"><a href="https://en.wikipedia.org/wiki/Set_(mathematics)" target="blank">set operator</a></span> allows us to construct one set from other sets.</p>
</div>
<div class="pager" key="pager_set_rewoperators">
<p>Algebraic calculations on sets resemble calculations on numbers because: </p>
<ul>
<li>set operations (intersection, union, ...) have properties similar to operations on reals (addition, multiplication, ...): these operations are associative, commutative, distributive, ... </li>
<li>set equality and real equality are equivalence relations that are transitive, symmetric and reflexive (see next section)</li>
</ul>
<p>Set algebra is equivalent to the <span class="exturl"><a href="https://fr.wikipedia.org/wiki/Alg%C3%A8bre_de_Boole_(logique)" target="_blank">Boolean algebra</a></span> : either an element belongs to a set, or it does not. This algebra is central in computer science, in software development and in the design of electronic circuits. </p>
</div>
<div class="pager" key="pager_settheory">
<a href="https://en.wikipedia.org/wiki/Georg_Cantor" target="_blank"><img class="txtwrap" src="./img/cantor.jpg" height="12%" width="12%"></a>
<p> At the end of the 19<span class="sup">th</span> Century, the German mathematician <span class="exturl"><a href="https://en.wikipedia.org/wiki/Georg_Cantor" target="_blank">Georg Cantor</a></span> developed the <span class="exturl"><a href="https://en.wikipedia.org/wiki/Set_theory" target="_blank">set theory</a></span>. This theory allows us to define fundamental elements of mathematics, notably integers, real numbers, functions ... </p>
<p>In 1930, The Austro-Hungarian mathematician, <span class="exturl"><a href="https://en.wikipedia.org/wiki/Kurt_G%C3%B6del" target="_blank">Kurt Gödel</a></span> even demonstrated that any theory can be translated into the set theory. </p>
</div>
<div class="pager" key="pager_sigma_seg">
<p>Sigma notation used to sum a series of indexed terms noted
<!--{type="expr" input="app_series a i"}--> (with the index i from 1 to n typically). This sum is noted:
<!--{type="expr" style="vertical-align: -4px;" input="(sigma(k,1,n,(app_series a k)))"}--> .</p>
<p>In this notation, the index k is a dummy variable: it is not declared in the context and is valid only for the summed expression.</p>
<p>Sigma properties are those of the addition (associativity, distributivity of multiplication, ...) and those of index shits.</p>
</div>
<div key="slide_demo_tuto_app_(3 * x - 6 = zero,lradd,0)">
<!-- (3 * x - 6 = zero,lradd,0)
by Forward lradd)
-->
<div class="pedagogic slide" expr="(3 * x - 6 = zero,lradd,0)" exercise="demo_tuto_app">
<p>The objective is to <span class="stress">isolate the term
<!--{type="expr" input="pow x 2"}--></span> on the left. Start by isolating x on the left as in the previous exercise, and then square left and right sides of the resulting equality.</p>
</div>
</div>
<div key="slide_demo_tuto_app_(3 * x = 6,lrdiv,0)">
<!-- (3 * x = 6,lrdiv,0)
by Forward lrdiv)
-->
<div class="pedagogic slide" expr="(3 * x = 6,lrdiv,0)" exercise="demo_tuto_app">
<p>Divide by 3 on the left and right sides in order to isolate x.</p>
</div>
</div>
<div key="slide_demo_tuto_app_(x = 2,app_square,0)">
<!-- (x = 2,app_square,0)
by Forward app_square)
-->
<div class="pedagogic slide" expr="(x = 2,app_square,0)" exercise="demo_tuto_app">
<p>The square function is applied on the left and right sides.</p>
</div>
</div>
<div key="slide_demo_tuto_comb_(3 * x - y = zero,combadd,0)">
<!-- (3 * x - y = zero,combadd,0)
by Forward combadd)
-->
<div class="pedagogic slide" expr="(3 * x - y = zero,combadd,0)" exercise="demo_tuto_comb">
<p>The objective is to isolate x by first <span class="stress">eliminating y.</span> We note that y shows on the left hand side of statement
<!--{type="tag" input="s0"}--> and that the opposite of y shows on the left side of
<!--{type="tag" input="s1"}--> .</p>
<p>We can eliminate y by adding sides to sides
<!--{type="tag" input="s1"}--> and
<!--{type="tag" input="s0"}--> .</p>
</div>
</div>
<div key="slide_demo_tuto_comb_(4 * x = 4,lrdiv,0)">
<!-- (4 * x = 4,lrdiv,0)
by Forward lrdiv)
-->
<div class="pedagogic slide" expr="(4 * x = 4,lrdiv,0)" exercise="demo_tuto_comb">
<p>Variable x is isolated by removing the coefficient 4 with a left and right division by 4.</p>
</div>
</div>
<div key="slide_demo_tuto_first_(2 * x + 1 = 5,lrsub,0)">
<!-- (2 * x + 1 = 5,lrsub,0)
by Forward lrsub)
-->
<div class="pedagogic slide" expr="(2 * x + 1 = 5,lrsub,0)" exercise="demo_tuto_first">
<p>The objective is to <span class="stress">isolate
<!--{type="expr" input="x"}--></span> on the left side, that is to say to obtain, by successive operations, an equality of the form x = ....</p>
<p>Start by isolating
<!--{type="expr" input="2*x"}--> by eliminating 1 on the left with left and right subtraction of 1.</p>
</div>
</div>
<div key="slide_demo_tuto_first_(2 * x = 4,lrdiv,0)">
<!-- (2 * x = 4,lrdiv,0)
by Forward lrdiv)
-->
<div class="pedagogic slide" expr="(2 * x = 4,lrdiv,0)" exercise="demo_tuto_first">
<p> Isolate
<!--{type="expr" input="x"}--> by eliminating 2 on left right sides with a division by 2 (trivially diffreemnt from 0). </p>
</div>
</div>
<div key="slide_demo_tuto_first_(find_expr x 2)">
<!-- (find_expr x 2)
by Backward (find_expr_intro)
-->
<div class="pedagogic slide" expr="(find_expr x 2)" exercise="demo_tuto_first">
</div>
</div>
<div key="slide_demo_tuto_fun_(( fanonym (SReals) (sunknown Expr) (x) (3 * x)),app_def,0)">
<!-- (( fanonym (SReals) (sunknown Expr) (x) (3 * x)),app_def,0)
by Forward app_def)
-->
<div class="pedagogic slide" expr="(( fanonym (SReals) (sunknown Expr) (x) (3 * x)),app_def,0)" exercise="demo_tuto_fun">
</div>
</div>
<div key="slide_demo_tuto_fun_(( fanonym (SReals) (sunknown Expr) (x) (x)),app_def,0)">
<!-- (( fanonym (SReals) (sunknown Expr) (x) (x)),app_def,0)
by Forward app_def)
-->
<div class="pedagogic slide" expr="(( fanonym (SReals) (sunknown Expr) (x) (x)),app_def,0)" exercise="demo_tuto_fun">
</div>
</div>
<div key="slide_demo_tuto_fun_((app_expr f a) = 3 * a,combadd,0)">
<!-- ((app_expr f a) = 3 * a,combadd,0)
by Forward combadd)
-->
<div class="pedagogic slide" expr="((app_expr f a) = 3 * a,combadd,0)" exercise="demo_tuto_fun">
</div>
</div>
<div key="slide_demo_tuto_fun_((app_expr g b) = b,lrmul,0)">
<!-- ((app_expr g b) = b,lrmul,0)
by Forward lrmul)
-->
<div class="pedagogic slide" expr="((app_expr g b) = b,lrmul,0)" exercise="demo_tuto_fun">
</div>