forked from teorth/QED
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
2794 lines (2632 loc) · 352 KB
/
index.html
File metadata and controls
2794 lines (2632 loc) · 352 KB
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
<!DOCTYPE HTML>
<html lang="en">
<head>
<title>QED</title>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<!-- Latest compiled and minified CSS -->
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css" integrity="sha384-BVYiiSIFeK1dGmJRAkycuHAHRg32OmUcww7on3RYdg4Va+PmSTsz/K68vbdEjh4u" crossorigin="anonymous">
<!-- Optional theme -->
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap-theme.min.css" integrity="sha384-rHyoN1iRsVXV4nD0JutlnGaslCJuC7uwjduW9SVrLvRYooPp2bWYgmgJQIXwl/Sp" crossorigin="anonymous">
<link rel="stylesheet" href="main.css">
<script defer src="js/logic.js"></script>
<script defer src="js/gui.js"></script>
<script defer src="js/main.js"></script>
</head>
<body>
<div class="container">
<header>
<h2>QED - an interactive textbook</h2>
</header>
<div class="clearfix" id="exercise-button-box"><b>Sections and exercises</b><div id="exercise-button-subbox"></div></div>
<br>
<div class="clearfix hidden" id="exercise"><UL>
<li>Welcome to QED, a short interactive text in <A HREF="https://en.wikipedia.org/wiki/Propositional_calculus" target="_blank">propositional logic</A> arranged in the format of a computer game.</li>
<li>Propositional logic is the logic of <A HREF="https://en.wikipedia.org/wiki/Atomic_sentence" target="_blank">atomic propositions</A> (which in this text are given names such as <I>A</I>, <I>B</I>, or <I>C</I>) and the statements one can form from these propositions using logical connectives such as AND, OR, and IMPLIES. It is a subset of <A HREF="https://en.wikipedia.org/wiki/First-order_logic" target="_blank">first-order logic</A>, which is the main form of logic used in mathematics.</li>
<li>The objective of this "game" is to prove statements in propositional logic from the given hypotheses by clicking and dragging on statements that one has already deduced. By solving exercises in this game, you should develop a greater understanding of propositional logic.</li>
<li>Expand the "Sections and exercises" section above and then click on the "Exercise 1.1" button to begin the text and start the sequence of exercises!</li>
</UL>
</div>
<br>
<div class="wrapper">
<div class="box root" id="root-environment"></div>
<div class="box term" id="term-window"></div>
<div class="box formula" id="formula-window"></div>
<div class="box deductions" id="deductions-box"></div>
<div class="box operators" id="operators-window"></div>
</div>
<div class="clearfix" id="proof-box" style="background-color:#ddd"></div>
<div class="clearfix">
<div class="halfbox" id="achievement-box" style="background-color:#bbb">
</div>
<div class="halfbox" id="notification-box" style="background-color:#ccc">
</div>
</div>
<button id="undo-button">IMMEDIATE UNDO</button>
<button id="restart-button">RESTART EXERCISE</button>
<button id="unsolve-button">UNSOLVE EXERCISE</button>
<button id="prev-exercise">PREVIOUS EXERCISE</button>
<button id="next-exercise">NEXT EXERCISE</button>
<button id="reset-button">RESET QED</button>
<button id="edit-state-button">EDIT STATE</button>
<p></p>
<H4 id="version-header"> This is
<a href="https://github.com/teorth/QED/blob/master/HISTORY.md">version 2.10.8</a>.
</H4>
If the text has updated to a new version since your last session, you may need to reset the text in order for it to work correctly, or at least redo some of the exercises that unlock certain laws. This page works best when viewed on a large screen and with the ability to drag-and-drop; in particular, this page is unlikely to be all that functional on a cell phone. Also one may need a recently updated browser in order for the page to work properly (in particular, grid layouts and local storage should be supported for the best experience).
<P>
</P>
Further discussion of this text may be found at <A HREF="https://terrytao.wordpress.com/2018/08/18/qed-version-2-0-an-interactive-text-in-first-order-logic/" target="_blank">this blog post</A>.
<P></P>
Here are some other interactive logic demonstrations:
<UL>
<LI><A HREF="https://play.google.com/store/apps/details?id=org.flowgrid.emojic">Emojic</A></LI>
<LI><A HREF="http://nandgame.com/">NandGame</A> - Build a computer from scratch</LI>
<LI><A HREF="http://proofs.openlogicproject.org/">Natural deduction proof editor and checker</A></LI>
<LI><A HREF="https://en.wikipedia.org/wiki/Tarski%27s_World">Tarski's World</A></LI>
<LI><A HREF="http://incredible.pm/"">The incredible proof machine</A></LI>
<LI><A HREF="http://www.markability.net/">The markable mark</A></LI>
<LI><A HREF="https://www.oercommons.org/authoring/1364-basic-wff-n-proof-a-teaching-guide/view">WFF'N PROOF</A></LI>
</UL>
<footer>
Originally written by Terence Tao. Now <A HREF="https://github.com/teorth/QED">on github</A> under a MIT license.
</footer>
<noscript>This text requires JavaScript to run. It appears that Javascript is not supported by your browser.</noscript>
<div id="dataContainer">
<div id="lawContainer">
<div class="law" id="law-LawConjunction1"><A HREF="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</A></div>
<div class="law" id="law-LawConjunction2"><A HREF="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</A> (left)</div>
<div class="law" id="law-LawConjunction3"><A HREF="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</A> (right)</div>
<div class="law" id="law-LawDisjunction1"><A HREF="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</A> (left)</div>
<div class="law" id="law-LawDisjunction2"><A HREF="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</A> (right)</div>
<div class="law" id="law-LawAssumption">IMPLICATION INTRODUCTION</div>
<div class="law" id="law-And">AND</div>
<div class="law" id="law-Or">OR</div>
<div class="law" id="law-Implies">IMPLIES</div>
<div class="law" id="law-Iff">IFF</div>
<div class="law" id="law-Not">NOT</div>
<div class="law" id="law-LawImplication"><A HREF="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</A></div>
<div class="law" id="law-Push">PUSH</div>
<div class="law" id="law-PushAlt">PUSH (alternate form)</div>
<div class="law" id="law-ModusPonens"><A HREF="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</A></div>
<div class="law" id="law-CaseAnalysis"><A HREF="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</A></div>
<div class="law" id="law-BiconditionalIntroduction">BICONDITIONAL INTRODUCTION</div>
<div class="law" id="law-BiconditionalElimination1">BICONDITIONAL ELIMINATION (left)</div>
<div class="law" id="law-BiconditionalElimination2">BICONDITIONAL ELIMINATION (right)</div>
<div class="law" id="law-caseElimination1"><A HREF="https://en.wikipedia.org/wiki/Disjunctive_syllogism" target="_blank">DISJUNCTIVE ELIMINATION</A> (left)</div>
<div class="law" id="law-caseElimination2"><A HREF="https://en.wikipedia.org/wiki/Disjunctive_syllogism" target="_blank">DISJUNCTIVE ELIMINATION</A> (right)</div>
<div class="law" id="law-ExcludedMiddle"><A HREF="https://en.wikipedia.org/wiki/Law_of_excluded_middle" target="_blank">EXCLUDED MIDDLE</A></div>
<div class="law" id="law-True">TRUE</div>
<div class="law" id="law-False">NOT FALSE</div>
<div class="law" id="law-False2">NOT FALSE (alternate form)</div>
<div class="law" id="law-PushVar">PUSH (for free variables)</div>
<div class="law" id="law-free">FREE VARIABLE INTRODUCTION</div>
<div class="law" id="law-forAll">FOR ALL</div>
<div class="law" id="law-thereExists">THERE EXISTS</div>
<div class="law" id="law-PushSet">PUSH (for set variables)</div>
<div class="law" id="law-Pull">PULL</div>
<div class="law" id="law-Pull2">PULL</div>
<div class="law" id="law-Existence">EXISTENCE</div>
<div class="law" id="law-Existence2">EXISTENCE</div>
<div class="law" id="law-Reflexivity">EQUALITY IS <A HREF="https://en.wikipedia.org/wiki/Reflexive_relation" target="_blank">REFLEXIVE</A></div>
<div class="law" id="law-UniversalIntroduction"><A HREF="https://en.wikipedia.org/wiki/Universal_generalization" target="_blank"> UNIVERSAL INTRODUCTION</A></div>
<div class="law" id="law-UniversalIntroduction2"><A HREF="https://en.wikipedia.org/wiki/Universal_generalization" target="_blank"> UNIVERSAL INTRODUCTION</A></div>
<div class="law" id="law-UniversalRenamingBoundVar">RENAMING BOUND VARIABLE (universal)</div>
<div class="law" id="law-ExistentialRenamingBoundVar">RENAMING BOUND VARIABLE (existential)</div>
<div class="law" id="law-BarbaraSingular">BARBARA SYLLOGISM (singular form)</div>
<div class="law" id="law-UniversalSpecification"><A HREF="https://en.wikipedia.org/wiki/Universal_instantiation" target="_blank">UNIVERSAL SPECIFICATION</A></div>
<div class="law" id="law-UniversalSpecification2">REVERSE <A HREF="https://en.wikipedia.org/wiki/Universal_generalization" target="_blank"> UNIVERSAL INTRODUCTION</A></div>
<div class="law" id="law-ExistentialInstantiation"><A HREF="https://en.wikipedia.org/wiki/Existential_instantiation" target="_blank">EXISTENTIAL INSTANTIATION</A></div>
<div class="law" id="law-ExistentialInstantiation2"><A HREF="https://en.wikipedia.org/wiki/Existential_instantiation" target="_blank">EXISTENTIAL INSTANTIATION</A></div>
<div class="law" id="law-ExistentialIntroduction"><A HREF="https://en.wikipedia.org/wiki/Existential_generalization">EXISTENTIAL INTRODUCTION</A></div>
<div class="law" id="law-ExistentialIntroduction2"><A HREF="https://en.wikipedia.org/wiki/Existential_generalization">EXISTENTIAL INTRODUCTION</A></div>
<div class="law" id="law-Indiscernability"><A HREF="https://en.wikipedia.org/wiki/Identity_of_indiscernibles" target="_blank">INDISCERNABILITY OF IDENTICALS</A></div>
</div>
<div id="exerciseContainer">
<div class="exercise" id="EXERCISE-1.1" data-unlocks="LawConjunction1">
<div class="name"></div>
<div class="notes">
<UL>
<li>The <B>Root environment</B> window below contains all the statements that one already knows to be true for the given exercise (which, in this case, are <I>A</I>, <I>B</I> and <I>C</I>). Initially this window will just contain the given hypotheses of the exercise.</li>
<li>Statements can be <A HREF="https://en.wikipedia.org/wiki/Atomic_formula" target="_blank">atomic formulas</A> such as <I>A</I>, <I>B</I>, and <I>C</I>, or compound formulas formed from the atomic formulas and logical connectives such as AND, OR, and NOT. For instance, (<I>A</I> AND <I>B</I>) OR <I>C</I> is a compound formula, and thus a potential statement in one's argument.</li>
<li>If one drags one statement to another, the <B>Available deductions</B> window below will show what conclusions one can draw from these statements using the available <A HREF="https://en.wikipedia.org/wiki/Rule_of_inference" target="_blank">deduction rules</A>; if any conclusions can be drawn, one can add them to the <B>Root environment</B> window by clicking on the button containing the conclusion.</li>
<li>For instance, to solve this level one drags the <I>A</I> statement onto the <I>B</I> statement (or vice versa), clicks on the button marked "<I>A</I> AND <I>B</I>" to add that statement to the <B>Root environment</B>, drags the new <I>A</I> AND <I>B</I> statement onto the <I>C</I> statement (or vice versa), and then clicks on the button containing the desired conclusion.</li>
<li>By opening the first exercise of Section 1 (Exercise 1.1), you unlocked the rule of <A HREF="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">conjunction introduction</A>. This asserts that if a statement <I>A</I> is known, and the statement <I>B</I> is known, then one can deduce the compound statement <I>A</I> AND <I>B</I>. This is the only rule one starts with, but more deductive rules will be unlocked whenever one begins a new section of the textbook. The <B>Achievements</B> window will record all the unlocked laws.</li>
<li>Progress is recorded in the <B>Achievements</B> and <B>Event log</B> windows below. This progress will be saved between sessions (assuming your browser supports local storage), unless you reset this interactive text completely using the button at the bottom of the page.</li>
<li>Your deductions will be recorded as a human-readable proof in the <B>Proof</B> window below. This window is not absolutely necessary in order to play the game, but should help you understand and interpret the moves you are making.</li>
<li>The exercise is completed when you have managed to obtain the desired conclusion (in this case, (<I>A</I> AND <I>B</I>) AND <I>C</I>) in the <B>Root environment</B> window. This will unlock further exercises and sections of the textbook, turning the exercise buttons from gray to yellow.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span><em>B</em>. <i>[given]</i></span></li>
<li><span><em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em>, <em>B</em>: deduce <em>A</em> AND <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>, <em>C</em>: deduce (<em>A</em> AND <em>B</em>) AND <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-1.2" data-unlocked-by="1.1">
<div class="name">AND IS <A HREF="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</A></div>
<div class="notes">
<UL>
<li>It is permissible to drag a statement onto itself.</li>
<LI>You can move forwards and backwards through the unlocked exercises using the "PREVIOUS EXERCISE" and "NEXT EXERCISE" buttons at the bottom of this page, or by using the '<' and '>' hotkeys.</LI>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em>, <em>A</em>: deduce <em>A</em> AND <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-2.1" data-unlocked-by="1.1" data-unlocks="LawConjunction2 LawConjunction3">
<div class="name">AND IS <A HREF="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</A></div>
<div class="notes">
<UL>
<li>The rules of <A HREF="https://en.wikipedia.org/wiki/Conjunction_elimination">conjunction elimination</A> have been unlocked. These rules assert that if a conjunction statement such as <I>A</I> AND <I>B</I> is known, then one can deduce either of the two individual statements <I>A</I> or <I>B</I> of that statement separately.</li>
<li>To activate this rule, click on a compound statement of the form <I>A</I> AND <I>B</I>.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>B</em>, <em>A</em>: deduce <em>B</em> AND <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-2.2(a)" data-unlocked-by="2.1">
<div class="name">AND IS <A HREF="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</A> (left)</div>
<div class="notes">
<UL>
<li>One can think of a deduction rule as a template in which the <A HREF="https://en.wikipedia.org/wiki/Atomic_formula" target="_blank">atomic formulas</A> of the deduction rule (such as <I>A</I> or <I>B</I>) can be replaced by compound formulas (e.g. "<I>A</I> AND <I>B</I>"). This can greatly increase the power of such laws.</li>
<li><Q>Each problem that I solved became a rule, which served afterwards to solve other problems</Q> - <A HREF="https://en.wikiquote.org/wiki/Ren%C3%A9_Descartes" target="_blank">René Descartes</A>. Each exercise solved in this text becomes a new deduction rule that you may use in subsequent exercises. The <B>Achievements</B> window lists all the rules of inference one has available, either through being unlocked by opening the appropriate exercise, or by proving that rule as one of the exercises.</li>
<li>One can also use the numbers '1' through '9' as hotkeys for the available eductions (or the first 9 of them, at any rate).</li>
</UL>
</div>
<ol class="proof">
<li><span>(<em>A</em> AND <em>B</em>) AND <em>C</em>. <i>[given]</i></span></li>
<li><span>From (<em>A</em> AND <em>B</em>) AND <em>C</em>: deduce <em>A</em> AND <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From (<em>A</em> AND <em>B</em>) AND <em>C</em>: deduce <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>B</em>, <em>C</em>: deduce <em>B</em> AND <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em>, <em>B</em> AND <em>C</em>: deduce <em>A</em> AND (<em>B</em> AND <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-2.2(b)" data-unlocked-by="2.1">
<div class="name">AND IS <A HREF="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</A> (right)</div>
<div class="notes">
<UL>
<li>There are no "wrong" moves in the QED game - every move you make is a valid deduction! However, you may end up making "useless" moves - moves that are logically valid, but do not bring one closer to the desired conclusion. If you are finding the deduction environment to be getting too cluttered, you can click on the exercise button (in this case, Exercise 2.2(b)) to start from the beginning; one can also press the "RESTART EXERCISE" (or presses "r") at the bottom of the page.</li>
<li>One can also delete sentences by selecting them and then pressing the delete key, though one should caution that this may render the exercise unsolvable without a restart if a key hypothesis ends up being deleted.</li>
<li>Finally, one can also "UNDO" a deduction if one presses the "IMMEDIATE UNDO" button at the bottom of this page (or presses "u") immediately after making a deduction. This feature is not available if the deduction solves the exercise, or if one has performed any action between the deduction and the undo.</li>
<LI>Thanks to Stijn Vanhee and Siddhartha Srivastava for supplying a short proof.</LI>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em> AND (<em>B</em> AND <em>C</em>). <i>[given]</i></span></li>
<li><span>From <em>A</em> AND (<em>B</em> AND <em>C</em>): deduce (<em>B</em> AND <em>C</em>) AND <em>A</em>. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>From (<em>B</em> AND <em>C</em>) AND <em>A</em>: deduce <em>B</em> AND (<em>C</em> AND <em>A</em>). <i>[AND IS <a href="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</a> (left)]</i></span></li>
<li><span>From <em>B</em> AND (<em>C</em> AND <em>A</em>): deduce (<em>C</em> AND <em>A</em>) AND <em>B</em>. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>From (<em>C</em> AND <em>A</em>) AND <em>B</em>: deduce <em>C</em> AND (<em>A</em> AND <em>B</em>). <i>[AND IS <a href="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</a> (left)]</i></span></li>
<li><span>From <em>C</em> AND (<em>A</em> AND <em>B</em>): deduce (<em>A</em> AND <em>B</em>) AND <em>C</em>. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-3.1(a)" data-unlocked-by="2.1" data-unlocks="LawDisjunction1 LawDisjunction2" data-reveals="FormulaWindow">
<div class="name"></div>
<div class="notes">
<UL>
<li>Some deductive rules use formulas (also known as <A HREF="https://en.wikipedia.org/wiki/Well-formed_formula" target="_blank">well-formed formulas</A>) as input.</li>
<li>Formulas look the same as statements, but whereas statements in the root environment are known to be true, a formula could be either true or false. As such, we place them in a separate <B>Formulas</B> window, which is now unlocked for use. For instance, in this exercise, the formulas <I>B</I> and <I>C</I> are <i>not</i> known to be true, but are still available for use in some rules of inference. The formula <I>A</I> is known to be true, so it can belong to both the <B>Root environment</B> and <B>Formulas</B> windows.</li>
<li>In mathematical logic, the logical connective OR (also known as <A HREF="https://en.wikipedia.org/wiki/Logical_disjunction" target="_blank">disjunction</A>) is interpreted as an <I>inclusive</I> or; the statement "<I>A</I> OR <I>B</I>" asserts that <I>at least one</I> of <I>A</I> and <I>B</I> are true, and in particular will remain true if <I>both</I> of <I>A</I> and <I>B</I> are true. This feature of OR is captured in part by the laws of <A HREF="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">disjunction introduction</A> that have just been unlocked.</li>
<li>To use one of these laws, drag a formula from the <B>Formulas</B> window to a sentence in the <B>Root environment</B> window (or drag a sentence in the <B>Root environment</B> window to a formula in the <B>Formulas</B> window).</li>
<li>To apply this exercise to future exercises, one needs to select three hypotheses (<I>A</I>, Formula <I>B</I>, and Formula <I></I>) rather than just one or two. To do this, drag the first hypothesis to the second and then CTRL-click the third, or clicks the first and then CTRL-click the next two. Similarly for applying any other exercise with three or more hypotheses.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em>: deduce <em>A</em> OR <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>: deduce <em>C</em> OR (<em>A</em> OR <em>B</em>). <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-3.1(b)" data-unlocked-by="3.1(a)">
<div class="name">OR IS <A HREF="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</A> (left)</div>
<div class="notes">
The reverse implication (deducing <I>A</I> from <I>A</I> OR <I>A</I>) is true, but will be deferred to Exercise 9.1(b), as we first need to introduce the important concept of an assumption and then introduce some further laws of disjunction.
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em>: deduce <em>A</em> OR <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-4.1" data-unlocked-by="3.1(a)" data-unlocks="LawAssumption">
<div class="name"></div>
<div class="notes">
<UL>
<li>The <B>Root environment</B> window holds all the statements that are known to be true under the given hypothesis. But sometimes in an argument, we also need to consider statements that are only <I>conditionally</I> known to be true, under one or more assumptions. For instance, we might not know that a statement <I>A</I> is true unconditionally, but instead know that <I>A</I> is conditionally true under the assumption of a second statement <I>B</I>.</li>
<li>In this interactive text, assumptions are depicted as subwindows of the <B>Root environment</B> window. For instance, to depict the knowledge of <I>A</I> conditionally under the assumption of <I>B</I>, one would form a subwindow of <B>Root environment</B> titled "<B>Assume <I>B</I></B>", and place <I>A</I> inside that window.</li>
<li>The <A HREF="https://en.wikipedia.org/wiki/Conditional_proof" target="_blank">law of assumption</A> (or <I>implication introduction</I>) asserts that if <I>A</I> is a formula, then it will be true if we first make an assumption that <I>A</I> holds.</li>
<li>Try dragging the formula <I>A</I> to the <B>Root environment</B> window (or clicking on the formula) to make such an assumption!</li>
<li>Every deductive rule that one can apply in the root environment, one can also apply in a sub-environment. This is the key to solving the current exercise (and to many subsequent exercises).
</UL>
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>], <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> AND <em>A</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-5.1" data-unlocked-by="4.1" data-unlocks="And Or">
<div class="name"></div>
<div class="notes">
<UL>
<li>One can combine formulas together to create compound formulas.</li>
<li>For binary logical connectives such as AND and OR, this is done here by dragging formulas together in the <B>Formulas</B> window.</li>
<li>See what happens if one drags the formula <I>A</I> onto the formula <I>B</I> or vice versa!</li>
<li>For the purposes of recording proof length, the creation of new formulas is considered to be a "free move" in this text, in that it does not use up any lines of the proof.</li>
</UL>
</div>
<ol class="proof">
<li><span>Deduce (<em>A</em> AND <em>B</em>) OR <em>C</em> [assuming (<em>A</em> AND <em>B</em>) OR <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-5.2" data-unlocked-by="5.1">
<div class="name"></div>
<div class="notes">
<UL>
<li>Assumptions can be nested.</li>
<li>The statement "<I>A</I>, assuming <I>B</I>, <I>A</I>" asserts that if one assumes <I>B</I>, and then subsequently assumes <I>A</I>, then the statement <I>A</I> will be true under these two assumptions.</li>
<li>As with Exercise 4.1, the key to solving this exercise is in using the fact that any deductive rule that is applicable in the root environment, can also be applied in any sub-environment.</li>
</UL>
</div>
<ol class="proof">
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>B</em>, <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-6.1(a)" data-unlocked-by="5.1" data-unlocks="Implies LawImplication">
<div class="name">IMPLIES IS <A HREF="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</A></div>
<div class="notes">
<UL>
<li>The logical connective IMPLIES is also known as <A HREF="https://en.wikipedia.org/wiki/Material_conditional" target="_blank">material implication</A> (or the <I>conditional</I>); informally, one can think of the assertion IMPLIES(<I>A</I>, <I>B</I>) as the assertion that <I>B</I> is "at least as true as" <I>A</I>. (But they do not need to be <I>equally</I> true: in particular, if <I>A</I> is false and <I>B</I> is true, then it turns out that <I>A</I> IMPLIES <I>B</I> is true.<li>The statement <I>A</I> IMPLIES <I>B</I> can also be written as IF <I>A</I>, THEN <I>B</I>.</li>
<li>The <A HREF="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">deduction theorem</A> asserts that if you can prove a statement <I>B</I> under the assumption of another statement <I>A</I>, then you can deduce the compound statement <I>A</I> IMPLIES <I>B</I>. It is very commonly used in mathematics to prove implication statements.<li>To use the deduction theorem, take a statement that is known under some hypothesis, and drag it out of the window corresponding to that hypothesis into the parent window. (In many cases, the parent window will be the <B>Root environment</B> window.)</li>
<li>In some proof systems for propositional calculus, the deduction theorem is not one of the given laws of inference, but actually has to be proven as a theorem, which explains the name. However, in this text, we will take the deduction theorem as a primitive inference rule.</li>
</UL>
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-6.1(b)" data-unlocked-by="6.1(a)">
<div class="name"></div>
<div class="notes">
To prove an implication of the form <I>X</I> IMPLIES <I>Y</I>, first create <I>X</I> as a formula in the <B>Formulas</B> window, drag it to the <B>Root environment</B> window to use it as an assumption, and then try to establish <I>Y</I> inside the window corresponding to that assumption. Then use the deduction theorem.
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> AND (<em>A</em> OR <em>B</em>) [assuming <em>A</em> AND (<em>A</em> OR <em>B</em>)]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> AND (<em>A</em> OR <em>B</em>) [assuming <em>A</em> AND (<em>A</em> OR <em>B</em>)]: deduce <em>A</em> [assuming <em>A</em> AND (<em>A</em> OR <em>B</em>)]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em> AND (<em>A</em> OR <em>B</em>)]: deduce (<em>A</em> AND (<em>A</em> OR <em>B</em>)) IMPLIES <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-6.2" data-unlocked-by="6.1(a)">
<div class="name">DOUBLE <A HREF="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</A></div>
<div class="notes">
<UL>
<li>This exercise easily follows from two applications of the deduction theorem, but is convenient for use in later exercises.</li>
<li>The appearance of [root environment] in the list of assumptions is not needed to <i>solve</i> the exercise; but it affects the user interface for <I>applying</I> the exercise. Namely, to invoke this theorem in the future, one should drag a statement "up" two levels, undoing two levels of assumption. (Without [root environment], one would instead click on the statement rather than drag it up two levels.)</li>
</UL>
</div>
<ol class="proof">
<li><span><em>C</em> [assuming <em>A</em>, <em>B</em>]. <i>[given]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-7.1" data-unlocked-by="6.1(a)" data-unlocks="Push PushAlt">
<div class="name"></div>
<div class="notes">
<UL>
<li>If a statement is known without an assumption, then it can be "pushed" into an enviroment with that assumption. For instance, if <I>A</I> is known to be true unconditionally, then it is also known to be true assuming <I>B</I>.</li>
<li>The push law is also known as "weakening" or <A HREF="https://en.wikipedia.org/wiki/Monotonicity_of_entailment" target = "_blank">monotonicity of entailment</A>.</li>
<li>To apply a push, drag a statement into an assumption environment that shares the same parent environment as the original statement. (Alternatively, if this environment has not yet been created, drag the statement onto a formula containing the assumption, or vice versa.)</li>
</UL>
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em>, <em>B</em>]. <i>[PUSH (alternate form)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>A</em>). <i>[DOUBLE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-7.2" data-unlocked-by="7.1">
<div class="name">DOUBLE PUSH</div>
<div class="notes">
<UL>
<li>This exercise easily follows from two applications of the push law, but turns out to be convenient in some subsequent exercises.</li>
<li>The presence of the assumption environment [assuming <I>B</I>, <I>C</I>] is needed for two technical reasons. Firstly, it populates the formula window with the atomic formulas <I>B</I>, <I>C</I>, which otherwise would not be present. Secondly, it affects the user interface for applying the double push rule. Namely, to invoke this law, one should push a statement "down" two levels, into an assumption window that is two levels nested below the one that the statement lies in.</li>
<li>Thanks to Steve Trout for contributing a short proof.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em>: deduce <em>A</em> [assuming <em>B</em>]. <i>[PUSH (alternate form)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>B</em>]: deduce <em>A</em> [assuming <em>B</em>, <em>C</em>]. <i>[PUSH (alternate form)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.1(a)" data-unlocked-by="7.1" data-unlocks="ModusPonens">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</A> (ASSUMPTION FORM)</div>
<div class="notes">
<UL>
<li><A HREF="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">Modus ponens</A> is one of the most famous deductive rules. It asserts that if a statement <I>A</I> is known to be true, and it is also known that <I>A</I> IMPLIES <I>B</I>, then one can conclude that <I>B</I> is also true.</li>
<li>To apply this rule, drag the hypothesis <I>A</I> of an implication onto the implication <I>A</I> IMPLIES <I>B</I>. The two statements must lie in the same assumption window for the law to be applied.</li>
<li>Incidentally, this exercise (the "assumption" form of Modus ponens) is a useful tool for several subsequent exercises in this text, so keep it in mind. To apply this exercise, drag a hypothesis <I>A</I> to a conclusion <I>B</I> that has already been obtained under the assumption of <I>A</I>.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span><em>B</em> [assuming <em>A</em>]. <i>[given]</i></span></li>
<li><span>From <em>B</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>A</em>, <em>A</em> IMPLIES <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.1(b)" data-unlocked-by="8.1(a)">
<div class="name">REVERSE <A HREF="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</A></div>
<div class="notes">
This exercise will be useful in some later exercises. To apply it, click on an implication statement such as <I>A</I> IMPLIES <I>B</I>.
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em> [assuming <em>A</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>], <em>A</em> IMPLIES <em>B</em> [assuming <em>A</em>]: deduce <em>B</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.2" data-unlocked-by="8.1(a)">
<div class="name">IMPLIES IS <A HREF="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</A></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>B</em> [assuming <em>A</em>]. <i>[REVERSE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>B</em> IMPLIES <em>C</em>: deduce <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>B</em> [assuming <em>A</em>], <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em>]: deduce <em>C</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.3" data-unlocked-by="8.1(a)">
<div class="name">AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a> (implication form)</div>
<div class="notes">
The fact that AND is commutative, proven in Exercise 2.1, will be helpful here.
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>B</em> AND <em>A</em> [assuming <em>A</em> AND <em>B</em>]. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>From <em>B</em> AND <em>A</em> [assuming <em>A</em> AND <em>B</em>]: deduce (<em>A</em> AND <em>B</em>) IMPLIES (<em>B</em> AND <em>A</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.4(a)" data-unlocked-by="8.1(a)">
<div class="name"></div>
<div class="notes">
General tip: one can press "n" to advance to the next available unsolved exercise, or "N" to advance to the last available unsolved exercise (which will usually be the first exercise of the section after the last solved exercise).
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>). <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>A</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>): deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>) [assuming <em>A</em> AND <em>B</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em> AND <em>B</em>], <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>) [assuming <em>A</em> AND <em>B</em>]: deduce <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>B</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>B</em> [assuming <em>A</em> AND <em>B</em>], <em>B</em> IMPLIES <em>C</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>C</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em> AND <em>B</em>]: deduce (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.4(b)" data-unlocked-by="8.1(a)">
<div class="name"></div>
<div class="notes">
</div>
<ol class="proof">
<li><span>(<em>A</em> AND <em>B</em>) IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>A</em>, <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em>, <em>B</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>, <em>B</em>], <em>B</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> AND <em>B</em> [assuming <em>A</em>, <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em>: deduce (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em> [assuming <em>A</em>, <em>B</em>]. <i>[DOUBLE PUSH]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em>, <em>B</em>], (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>C</em> [assuming <em>A</em>, <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>). <i>[DOUBLE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.4(c)" data-unlocked-by="8.1(a)">
<div class="name"></div>
<div class="notes">
Thanks to William Chargin and Junghyeon Park for a short proof.
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>). <i>[given]</i></span></li>
<li><span>From <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>C</em>): deduce (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em>. <i>[EXERCISE 8.4(a)]</i></span></li>
<li><span>Deduce (<em>B</em> AND <em>A</em>) IMPLIES (<em>A</em> AND <em>B</em>). <i>[EXERCISE 8.3]</i></span></li>
<li><span>From (<em>B</em> AND <em>A</em>) IMPLIES (<em>A</em> AND <em>B</em>), (<em>A</em> AND <em>B</em>) IMPLIES <em>C</em>: deduce (<em>B</em> AND <em>A</em>) IMPLIES <em>C</em>. <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</a>]</i></span></li>
<li><span>From (<em>B</em> AND <em>A</em>) IMPLIES <em>C</em>: deduce <em>B</em> IMPLIES (<em>A</em> IMPLIES <em>C</em>). <i>[EXERCISE 8.4(b)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.5(a)" data-unlocked-by="8.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Absorption_(logic)" target="_blank">ABSORPTION (right)</A></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>B</em> [assuming <em>A</em>]. <i>[REVERSE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>], <em>B</em> [assuming <em>A</em>]: deduce <em>A</em> AND <em>B</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES (<em>A</em> AND <em>B</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.5(b)" data-unlocked-by="8.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Absorption_(logic)" target="_blank">ABSORPTION (left)</A></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>A</em> IMPLIES (<em>A</em> AND <em>B</em>). <i>[<a href="https://en.wikipedia.org/wiki/Absorption_(logic)" target="_blank">ABSORPTION (right)</a>]</i></span></li>
<li><span>Deduce (<em>A</em> AND <em>B</em>) IMPLIES (<em>B</em> AND <em>A</em>). <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a> (implication form)]</i></span></li>
<li><span>From <em>A</em> IMPLIES (<em>A</em> AND <em>B</em>), (<em>A</em> AND <em>B</em>) IMPLIES (<em>B</em> AND <em>A</em>): deduce <em>A</em> IMPLIES (<em>B</em> AND <em>A</em>). <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.6(a)" data-unlocked-by="8.1(a)">
<div class="name"></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>A</em>, <em>A</em> IMPLIES <em>C</em>: deduce <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>From <em>C</em>, <em>B</em>: deduce <em>C</em> AND <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-8.6(b)" data-unlocked-by="8.1(a)">
<div class="name"></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>: deduce <em>B</em> AND <em>A</em>. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>From <em>B</em> AND <em>A</em>, <em>B</em> IMPLIES <em>C</em>: deduce <em>C</em> AND <em>A</em>. <i>[EXERCISE 8.6(a)]</i></span></li>
<li><span>From <em>C</em> AND <em>A</em>: deduce <em>A</em> AND <em>C</em>. <i>[AND IS <a href="https://en.wikipedia.org/wiki/Commutative_property" target="_blank">COMMUTATIVE</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.1(a)" data-unlocked-by="8.1(a)" data-unlocks="CaseAnalysis">
<div class="name">OR IS COMMUTATIVE</div>
<div class="notes">
<UL>
<li>We now return to the laws of disjunction (i.e., the laws of the "OR" connective).</li>
<li>To complement the laws of <A HREF="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">disjunction introduction</A> from Section 3, one has the law of <A HREF="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">case analysis</A>: if a statement <I>C</I> is known to be true under the assumption <I>A</I>, and also known to be true under the assumption <I>B</I>, then it is true under the assumption <I>A</I> OR <I>B</I>.</li>
<li>For instance, to solve the current exercise, first establish <I>B</I> OR <I>A</I> under the assumption of <I>A</I>, and then separately establish <I>B</I> OR <I>A</I> under the assumption of <I>B</I>. Then drag the two conclusions together!</li>
<li>Splitting into cases is a common technique in mathematics. For instance, to prove a statement <I>A</I> involving a natural number <i>n</i>, one might first prove the statement <I>A</I> assuming <i>n</I> is odd, and then prove it assuming <I>n</I> is even. Since <i>n</I> has to be odd or even, the law of case analysis then establishes the statement <I>A</I> unconditionally.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>B</em> OR <em>A</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>B</em> [assuming <em>B</em>]: deduce <em>B</em> OR <em>A</em> [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From <em>B</em> OR <em>A</em> [assuming <em>A</em>], <em>B</em> OR <em>A</em> [assuming <em>B</em>]: deduce <em>B</em> OR <em>A</em> [assuming <em>A</em> OR <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>B</em> OR <em>A</em> [assuming <em>A</em> OR <em>B</em>]: deduce <em>B</em> OR <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.1(b)" data-unlocked-by="9.1(a)">
<div class="name">OR IS <A HREF="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</A> (right)</div>
<div class="notes">
This is the reverse of Exercise 3.1(b).
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>A</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>], <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em> OR <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>A</em> OR <em>A</em>, <em>A</em> [assuming <em>A</em> OR <em>A</em>]: deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.2(a)" data-unlocked-by="9.1(a)">
<div class="name">OR IS <A HREF="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</A> (left)</div>
<div class="notes">
<UL>
<li>From this point onwards, the solutions will begin to be somewhat lengthy.</li>
<li>Thanks to Steve Trout, William Chargin, Daniel Spivak, and Keith Winstein for contributing a (relatively) short proof, and Anders Kaseorg for an even shorter proof.</li>
</UL>
</div>
<ol class="proof">
<li><span>(<em>A</em> OR <em>B</em>) OR <em>C</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>B</em> [assuming <em>B</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>B</em>]. <i>[EXERCISE 3.1(a)]</i></span></li>
<li><span>Deduce <em>C</em> [assuming <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>C</em> [assuming <em>C</em>]: deduce <em>B</em> OR <em>C</em> [assuming <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>B</em> OR <em>C</em> [assuming <em>C</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>A</em>], <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>B</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>A</em> OR <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>A</em> OR <em>B</em>], <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming <em>C</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming (<em>A</em> OR <em>B</em>) OR <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From (<em>A</em> OR <em>B</em>) OR <em>C</em>, <em>A</em> OR (<em>B</em> OR <em>C</em>) [assuming (<em>A</em> OR <em>B</em>) OR <em>C</em>]: deduce <em>A</em> OR (<em>B</em> OR <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.2(b)" data-unlocked-by="9.1(a)">
<div class="name">OR IS <A HREF="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</A> (right)</div>
<div class="notes">
Thanks to William Chargin for a short proof.
</div>
<ol class="proof">
<li><span><em>A</em> OR (<em>B</em> OR <em>C</em>). <i>[given]</i></span></li>
<li><span>From <em>A</em> OR (<em>B</em> OR <em>C</em>): deduce (<em>B</em> OR <em>C</em>) OR <em>A</em>. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>From (<em>B</em> OR <em>C</em>) OR <em>A</em>: deduce <em>B</em> OR (<em>C</em> OR <em>A</em>). <i>[OR IS <a href="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</a> (left)]</i></span></li>
<li><span>From <em>B</em> OR (<em>C</em> OR <em>A</em>): deduce (<em>C</em> OR <em>A</em>) OR <em>B</em>. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>From (<em>C</em> OR <em>A</em>) OR <em>B</em>: deduce <em>C</em> OR (<em>A</em> OR <em>B</em>). <i>[OR IS <a href="https://en.wikipedia.org/wiki/Associative_property" target="_blank">ASSOCIATIVE</a> (left)]</i></span></li>
<li><span>From <em>C</em> OR (<em>A</em> OR <em>B</em>): deduce (<em>A</em> OR <em>B</em>) OR <em>C</em>. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.3(a)" data-unlocked-by="9.1(a)">
<div class="name">OR <A HREF="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</A> OVER AND (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> OR (<em>B</em> AND <em>C</em>). <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> OR <em>B</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> OR <em>C</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em> [assuming <em>A</em>], <em>A</em> OR <em>C</em> [assuming <em>A</em>]: deduce (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>Deduce <em>B</em> AND <em>C</em> [assuming <em>B</em> AND <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>B</em> AND <em>C</em> [assuming <em>B</em> AND <em>C</em>]: deduce <em>B</em> [assuming <em>B</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>B</em> AND <em>C</em> [assuming <em>B</em> AND <em>C</em>]: deduce <em>C</em> [assuming <em>B</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>B</em> [assuming <em>B</em> AND <em>C</em>]: deduce <em>A</em> OR <em>B</em> [assuming <em>B</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>C</em> [assuming <em>B</em> AND <em>C</em>]: deduce <em>A</em> OR <em>C</em> [assuming <em>B</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em> [assuming <em>B</em> AND <em>C</em>], <em>A</em> OR <em>C</em> [assuming <em>B</em> AND <em>C</em>]: deduce (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>B</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>A</em>], (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>B</em> AND <em>C</em>]: deduce (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>A</em> OR (<em>B</em> AND <em>C</em>)]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>A</em> OR (<em>B</em> AND <em>C</em>), (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>) [assuming <em>A</em> OR (<em>B</em> AND <em>C</em>)]: deduce (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.3(b)" data-unlocked-by="9.1(a)">
<div class="name">AND <A HREF="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</A> OVER OR (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> AND (<em>B</em> OR <em>C</em>). <i>[given]</i></span></li>
<li><span>From <em>A</em> AND (<em>B</em> OR <em>C</em>): deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND (<em>B</em> OR <em>C</em>): deduce <em>B</em> OR <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em>: deduce <em>A</em> [assuming <em>B</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> [assuming <em>B</em>], <em>B</em> [assuming <em>B</em>]: deduce <em>A</em> AND <em>B</em> [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>B</em>]: deduce (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>Deduce <em>C</em> [assuming <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em>: deduce <em>A</em> [assuming <em>C</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> [assuming <em>C</em>], <em>C</em> [assuming <em>C</em>]: deduce <em>A</em> AND <em>C</em> [assuming <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em> AND <em>C</em> [assuming <em>C</em>]: deduce (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>B</em>], (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>C</em>]: deduce (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>B</em> OR <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>B</em> OR <em>C</em>, (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>) [assuming <em>B</em> OR <em>C</em>]: deduce (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.3(c)" data-unlocked-by="9.1(a)">
<div class="name">AND <A HREF="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</A> OVER OR (right)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span>(<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>). <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>A</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>B</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>B</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>B</em> OR <em>C</em> [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em> AND <em>B</em>], <em>B</em> OR <em>C</em> [assuming <em>A</em> AND <em>B</em>]: deduce <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming <em>A</em> AND <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>Deduce <em>A</em> AND <em>C</em> [assuming <em>A</em> AND <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> AND <em>C</em> [assuming <em>A</em> AND <em>C</em>]: deduce <em>A</em> [assuming <em>A</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>C</em> [assuming <em>A</em> AND <em>C</em>]: deduce <em>C</em> [assuming <em>A</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em> AND <em>C</em>]: deduce <em>B</em> OR <em>C</em> [assuming <em>A</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em> AND <em>C</em>], <em>B</em> OR <em>C</em> [assuming <em>A</em> AND <em>C</em>]: deduce <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming <em>A</em> AND <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming <em>A</em> AND <em>B</em>], <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming <em>A</em> AND <em>C</em>]: deduce <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>)]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>), <em>A</em> AND (<em>B</em> OR <em>C</em>) [assuming (<em>A</em> AND <em>B</em>) OR (<em>A</em> AND <em>C</em>)]: deduce <em>A</em> AND (<em>B</em> OR <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.3(d)" data-unlocked-by="9.1(a)">
<div class="name">OR <A HREF="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</A> OVER AND (right)</div>
<div class="notes">
Thanks to Jan Wieners for the short proof.
</div>
<ol class="proof">
<li><span>(<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>). <i>[given]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>): deduce <em>A</em> OR <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From <em>A</em> OR <em>C</em>: deduce <em>A</em> OR <em>C</em> [assuming <em>B</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>B</em> [assuming <em>B</em>], <em>A</em> OR <em>C</em> [assuming <em>B</em>]: deduce <em>B</em> AND (<em>A</em> OR <em>C</em>) [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li>
<li><span>From <em>B</em> AND (<em>A</em> OR <em>C</em>) [assuming <em>B</em>]: deduce (<em>B</em> AND <em>A</em>) OR (<em>B</em> AND <em>C</em>) [assuming <em>B</em>]. <i>[AND <a href="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</a> OVER OR (left)]</i></span></li>
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>From (<em>B</em> AND <em>A</em>) OR (<em>B</em> AND <em>C</em>) [assuming <em>B</em>]: deduce (<em>B</em> AND <em>C</em>) OR (<em>B</em> AND <em>A</em>) [assuming <em>B</em>]. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>From (<em>B</em> AND <em>C</em>) OR (<em>B</em> AND <em>A</em>) [assuming <em>B</em>]: deduce ((<em>B</em> AND <em>C</em>) OR <em>B</em>) AND ((<em>B</em> AND <em>C</em>) OR <em>A</em>) [assuming <em>B</em>]. <i>[OR <a href="https://en.wikipedia.org/wiki/Distributive_property" target="_blank">DISTRIBUTES</a> OVER AND (left)]</i></span></li>
<li><span>From ((<em>B</em> AND <em>C</em>) OR <em>B</em>) AND ((<em>B</em> AND <em>C</em>) OR <em>A</em>) [assuming <em>B</em>]: deduce (<em>B</em> AND <em>C</em>) OR <em>A</em> [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li>
<li><span>From (<em>B</em> AND <em>C</em>) OR <em>A</em> [assuming <em>B</em>]: deduce <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>B</em>]. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>From <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>A</em>], <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>B</em>]: deduce <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>A</em> OR <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From (<em>A</em> OR <em>B</em>) AND (<em>A</em> OR <em>C</em>): deduce <em>A</em> OR <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>A</em> OR (<em>B</em> AND <em>C</em>) [assuming <em>A</em> OR <em>B</em>]: deduce <em>A</em> OR (<em>B</em> AND <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.4(a)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</A> (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>C</em>: deduce <em>C</em> [assuming <em>A</em>]. <i>[REVERSE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>C</em> [assuming <em>A</em>]: deduce <em>C</em> OR <em>B</em> [assuming <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (left)]</i></span></li>
<li><span>Deduce <em>B</em> [assuming <em>B</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>B</em> [assuming <em>B</em>]: deduce <em>C</em> OR <em>B</em> [assuming <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Disjunction_introduction" target="_blank">DISJUNCTION INTRODUCTION</a> (right)]</i></span></li>
<li><span>From <em>C</em> OR <em>B</em> [assuming <em>A</em>], <em>C</em> OR <em>B</em> [assuming <em>B</em>]: deduce <em>C</em> OR <em>B</em> [assuming <em>A</em> OR <em>B</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Proof_by_exhaustion" target="_blank">CASE ANALYSIS</a>]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>C</em> OR <em>B</em> [assuming <em>A</em> OR <em>B</em>]: deduce <em>C</em> OR <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a> (ASSUMPTION FORM)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.4(b)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</A> (right)</div>
<div class="notes">
Thanks to William Chargin for a short proof.
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>: deduce <em>B</em> OR <em>A</em>. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>From <em>B</em> OR <em>A</em>, <em>B</em> IMPLIES <em>C</em>: deduce <em>C</em> OR <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (left)]</i></span></li>
<li><span>From <em>C</em> OR <em>A</em>: deduce <em>A</em> OR <em>C</em>. <i>[OR IS COMMUTATIVE]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.4(c)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</A> (both)</div>
<div class="notes">
<UL>
<li>This exercise involves three hypotheses, so it cannot be directly invoked by clicking or dragging on these hypotheses. However, if one drags the first hypothesis to the second and then CTRL-clicks the third, or if one clicks the first and then CTRL-clicks the next two, one will be able to apply this exercise (once it is proven), of course. Alternatively, one can use the two halves of this dilemma in Exercise 19(a) and Exercise 19(b) as a substitute.</li>
<li>This exercise can be solved quickly if one uses Exercises 9.4(a) and 9.4(b). (Of course, you must then solve these exercises first!)</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IMPLIES <em>C</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IMPLIES <em>D</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>A</em> IMPLIES <em>C</em>: deduce <em>C</em> OR <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (left)]</i></span></li>
<li><span>From <em>C</em> OR <em>B</em>, <em>B</em> IMPLIES <em>D</em>: deduce <em>C</em> OR <em>D</em>. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (right)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.5(a)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Monotonic_function" target="_blank">MONOTONICITY</A> OF AND (right)</div>
<div class="notes">
Thanks to dP dt for the short proof, and Anders Kaseorg for a shorter proof (located using computer search!).
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce (<em>B</em> AND <em>C</em>) IMPLIES (<em>B</em> AND <em>C</em>). <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</a>]</i></span></li>
<li><span>From (<em>B</em> AND <em>C</em>) IMPLIES (<em>B</em> AND <em>C</em>): deduce <em>B</em> IMPLIES (<em>C</em> IMPLIES (<em>B</em> AND <em>C</em>)). <i>[EXERCISE 8.4(b)]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>, <em>B</em> IMPLIES (<em>C</em> IMPLIES (<em>B</em> AND <em>C</em>)): deduce <em>A</em> IMPLIES (<em>C</em> IMPLIES (<em>B</em> AND <em>C</em>)). <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</a>]</i></span></li>
<li><span>From <em>A</em> IMPLIES (<em>C</em> IMPLIES (<em>B</em> AND <em>C</em>)): deduce (<em>A</em> AND <em>C</em>) IMPLIES (<em>B</em> AND <em>C</em>). <i>[EXERCISE 8.4(a)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.5(b)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Monotonic_function" target="_blank">MONOTONICITY</A> OF OR (right)</div>
<div class="notes">
Thanks to Pace Nielsen, Andrew Liftin, Alan Lu, and Ephim Kolmogorov for the short proof.
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>A</em> OR <em>C</em> [assuming <em>A</em> OR <em>C</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em> [assuming <em>A</em> OR <em>C</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>A</em> OR <em>C</em> [assuming <em>A</em> OR <em>C</em>], <em>A</em> IMPLIES <em>B</em> [assuming <em>A</em> OR <em>C</em>]: deduce <em>B</em> OR <em>C</em> [assuming <em>A</em> OR <em>C</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (left)]</i></span></li>
<li><span>From <em>B</em> OR <em>C</em> [assuming <em>A</em> OR <em>C</em>]: deduce (<em>A</em> OR <em>C</em>) IMPLIES (<em>B</em> OR <em>C</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.5(c)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Monotonic_function" target="_blank">MONOTONICITY</A> OF AND (left)</div>
<div class="notes">
Thanks to Gesse Roure for a short proof.
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>C</em> AND <em>A</em> [assuming <em>C</em> AND <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em> [assuming <em>C</em> AND <em>A</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>C</em> AND <em>A</em> [assuming <em>C</em> AND <em>A</em>], <em>A</em> IMPLIES <em>B</em> [assuming <em>C</em> AND <em>A</em>]: deduce <em>C</em> AND <em>B</em> [assuming <em>C</em> AND <em>A</em>]. <i>[EXERCISE 8.6(b)]</i></span></li>
<li><span>From <em>C</em> AND <em>B</em> [assuming <em>C</em> AND <em>A</em>]: deduce (<em>C</em> AND <em>A</em>) IMPLIES (<em>C</em> AND <em>B</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-9.5(d)" data-unlocked-by="9.1(a)">
<div class="name"><A HREF="https://en.wikipedia.org/wiki/Monotonic_function" target="_blank">MONOTONICITY</A> OF OR (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span>Deduce <em>C</em> OR <em>A</em> [assuming <em>C</em> OR <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em> [assuming <em>C</em> OR <em>A</em>]. <i>[PUSH]</i></span></li>
<li><span>From <em>C</em> OR <em>A</em> [assuming <em>C</em> OR <em>A</em>], <em>A</em> IMPLIES <em>B</em> [assuming <em>C</em> OR <em>A</em>]: deduce <em>C</em> OR <em>B</em> [assuming <em>C</em> OR <em>A</em>]. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (right)]</i></span></li>
<li><span>From <em>C</em> OR <em>B</em> [assuming <em>C</em> OR <em>A</em>]: deduce (<em>C</em> OR <em>A</em>) IMPLIES (<em>C</em> OR <em>B</em>). <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(a)" data-unlocked-by="9.1(a)" data-unlocks="Iff BiconditionalIntroduction BiconditionalElimination1 BiconditionalElimination2">
<div class="name">SUBSTITUTION</div>
<div class="notes">
<UL>
<li>The logical connective IFF (short for "IF AND ONLY IF") is also known as the <A HREF="https://en.wikipedia.org/wiki/Logical_biconditional" target="_blank">biconditional</A>.</li>
<li>As the laws of biconditional assert, the statement <I>A</I> IFF <I>B</I> is equivalent to the statements <I>A</I> IMPLIES <I>B</I> and <I>B</I> IMPLIES <I>A</I> both being true.</li>
<li>Another way of thinking about it is that the statement <I>A</I> IFF <I>B</I> asserts that <I>A</I> and <I>B</I> are <I>equally</I> true.</li>
<li>To use the laws, either click on a statement of the form <I>A</I> IFF <I>B</I> to be able to apply biconditional elimination to deduce <I>A</I> IMPLIES <I>B</I> or <I>B</I> IMPLIES <I>A</I>, or drag <I>A</I> IMPLIES <I>B</I> and <I>B</I> IMPLIES <I>A</I> together to form <I>A</I> IFF <I>B</I> (or <I>B</I> IFF <I>A</I>) via the law of biconditional introduction.</li>
</UL>
</div>
<ol class="proof">
<li><span><em>A</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IFF <em>B</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em>, <em>A</em> IMPLIES <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Modus_ponens" target="_blank">MODUS PONENS</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(b)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR AND (left)</div>
<div class="notes">
Thanks to Wilson Cheang and Alan Lu for a short proof from a previous version of the text.
</div>
<ol class="proof">
<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>C</em>: deduce <em>A</em> IMPLIES <em>C</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>, <em>A</em> IMPLIES <em>C</em>: deduce <em>C</em> AND <em>B</em>. <i>[EXERCISE 8.6(a)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(c)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR AND (right)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>B</em> IFF <em>C</em>: deduce <em>B</em> IMPLIES <em>C</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> AND <em>B</em>, <em>B</em> IMPLIES <em>C</em>: deduce <em>A</em> AND <em>C</em>. <i>[EXERCISE 8.6(b)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(d)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR OR (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>C</em>: deduce <em>A</em> IMPLIES <em>C</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>A</em> IMPLIES <em>C</em>: deduce <em>C</em> OR <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (left)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(e)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR OR (right)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> OR <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>B</em> IFF <em>C</em>: deduce <em>B</em> IMPLIES <em>C</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> OR <em>B</em>, <em>B</em> IMPLIES <em>C</em>: deduce <em>A</em> OR <em>C</em>. <i>[<a href="https://en.wikipedia.org/wiki/Constructive_dilemma" target="_blank">CONSTRUCTIVE DILEMMA</a> (right)]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(f)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR IMPLIES (left)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span><em>A</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>C</em>: deduce <em>C</em> IMPLIES <em>A</em>. <i>[BICONDITIONAL ELIMINATION (right)]</i></span></li>
<li><span>From <em>C</em> IMPLIES <em>A</em>, <em>A</em> IMPLIES <em>B</em>: deduce <em>C</em> IMPLIES <em>B</em>. <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.1(g)" data-unlocked-by="10.1(a)">
<div class="name">SUBSTITUTION FOR IMPLIES (right)</div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IMPLIES <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>B</em> IFF <em>C</em>: deduce <em>B</em> IMPLIES <em>C</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>, <em>B</em> IMPLIES <em>C</em>: deduce <em>A</em> IMPLIES <em>C</em>. <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</a>]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.2(a)" data-unlocked-by="10.1(a)">
<div class="name">IFF IS <A HREF="https://en.wikipedia.org/wiki/Symmetric_relation" target="_blank">SYMMETRIC</A></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IFF <em>B</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> IFF <em>B</em>: deduce <em>B</em> IMPLIES <em>A</em>. <i>[BICONDITIONAL ELIMINATION (right)]</i></span></li>
<li><span>From <em>B</em> IMPLIES <em>A</em>, <em>A</em> IMPLIES <em>B</em>: deduce <em>B</em> IFF <em>A</em>. <i>[BICONDITIONAL INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.2(b)" data-unlocked-by="10.1(a)">
<div class="name">IFF IS <A HREF="https://en.wikipedia.org/wiki/Transitive_relation" target="_blank">TRANSITIVE</A></div>
<div class="notes">
</div>
<ol class="proof">
<li><span><em>A</em> IFF <em>B</em>. <i>[given]</i></span></li>
<li><span><em>B</em> IFF <em>C</em>. <i>[given]</i></span></li>
<li><span>From <em>A</em> IFF <em>B</em>: deduce <em>A</em> IMPLIES <em>B</em>. <i>[BICONDITIONAL ELIMINATION (left)]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>, <em>B</em> IFF <em>C</em>: deduce <em>A</em> IMPLIES <em>C</em>. <i>[SUBSTITUTION FOR IMPLIES (right)]</i></span></li>
<li><span>From <em>A</em> IFF <em>B</em>: deduce <em>B</em> IMPLIES <em>A</em>. <i>[BICONDITIONAL ELIMINATION (right)]</i></span></li>
<li><span>From <em>B</em> IMPLIES <em>A</em>, <em>B</em> IFF <em>C</em>: deduce <em>C</em> IMPLIES <em>A</em>. <i>[SUBSTITUTION FOR IMPLIES (left)]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>C</em>, <em>C</em> IMPLIES <em>A</em>: deduce <em>A</em> IFF <em>C</em>. <i>[BICONDITIONAL INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.2(c)" data-unlocked-by="10.1(a)">
<div class="name">IFF IS <A HREF="https://en.wikipedia.org/wiki/Reflexive_relation" target="_blank">REFLEXIVE</A></div>
<div class="notes">
"<I>if it was so, it might be; and if it were so, it would be; but as it isn't, it ain't. That's logic.</I>" - Tweedledee, "Through the Looking Glass"
<UL>
<LI>The facts that IFF is symmetric, transitive, and reflexive can be combined into the single assertion that IFF is an <A HREF="https://en.wikipedia.org/wiki/Equivalence_relation">equivalence relation</A>.</LI>
</UL>
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> IMPLIES <em>A</em>. <i>[IMPLIES IS <a href="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</a>]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>A</em>, <em>A</em> IMPLIES <em>A</em>: deduce <em>A</em> IFF <em>A</em>. <i>[BICONDITIONAL INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.3" data-unlocked-by="10.1(a)">
<div class="name">BICONDITIONAL INTRODUCTION (ASSUMPTION FORM)</div>
<div class="notes">
This form of biconditional introduction is convenient in some later exercises, as it can shorten proofs slightly.
</div>
<ol class="proof">
<li><span><em>A</em> [assuming <em>B</em>]. <i>[given]</i></span></li>
<li><span><em>B</em> [assuming <em>A</em>]. <i>[given]</i></span></li>
<li><span>From <em>A</em> [assuming <em>B</em>]: deduce <em>B</em> IMPLIES <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>B</em> [assuming <em>A</em>]: deduce <em>A</em> IMPLIES <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>From <em>A</em> IMPLIES <em>B</em>, <em>B</em> IMPLIES <em>A</em>: deduce <em>A</em> IFF <em>B</em>. <i>[BICONDITIONAL INTRODUCTION]</i></span></li>
<li><span>QED!</span></li>
</ol>
</div>
<div class="exercise" id="EXERCISE-10.4" data-unlocked-by="10.1(a)">
<div class="name">OR IS <A HREF="https://en.wikipedia.org/wiki/Idempotence" target="_blank">IDEMPOTENT</A> (biconditional form)</div>