forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmmset.raw.html
5549 lines (4710 loc) · 248 KB
/
mmset.raw.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML LANG="EN-US">
<HEAD>
<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<TITLE>Proof Explorer - Home Page - Metamath</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<!--
<style type="text/css">
@media screen { /* hide from IE3 */ a[href]:hover { background: #ffa } }
</style>
<style type="text/css"> a:hover { background: #A6CAF0 } </style>
<style type="text/css"> a:hover { background: #B2FFE8 } </style>
<style type="text/css"> a:hover { background: #E2F2DE } </style>
<style type="text/css"> a:hover { background: #C9FFBC } </style>
<style type="text/css"> a:hover { background: #D6D6FF }
<style type="text/css"> TABLE,TD { border-style: ridge } </style>
-->
<STYLE TYPE="text/css">
<!--
/* Math symbol image will be shifted down 4 pixels to align with normal
text for compatibility with various browsers. The old ALIGN=TOP for
math symbol images did not align in all browsers and should be deleted.
All other images must override this shift with STYLE="margin-bottom:0px".
(2-Oct-2015 nm) */
img { margin-bottom: -4px }
-->
</STYLE>
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP><A HREF="../index.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Home"
TITLE="Metamath Home"
HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
</TD>
<TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Proof Explorer Home Page</B></FONT>
</TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif> <A HREF="wn.html">First ></A><BR><A
HREF="grothprim.html">Last ></A></FONT>
</TD>
</TR>
<TR>
<TD COLSPAN=3 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../mm.html">Mirrors</A> >
<A HREF="../index.html">Home</A> >
MPE Home >
<A HREF="mmtheorems.html">Th. List</A> >
<A HREF="mmrecent.html">Recent</A>
</FONT>
</TD>
</TR>
</TABLE>
<!--
<TABLE BORDER=0 WIDTH="100%"><TR>
<TD NOWRAP ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2 FACE=sans-serif><A
HREF="../index.html"><IMG SRC="mm.gif" BORDER=0 ALT="Metamath Home"
HEIGHT=32 WIDTH=32 ALIGN=LEFT STYLE="margin-bottom:0px"><IMG
SRC="spacer.gif" BORDER=0 ALT="" HEIGHT=32 WIDTH=2 ALIGN=LEFT
STYLE="margin-bottom:0px">Metamath<BR>Home</A></FONT></TD>
<TD ALIGN=CENTER VALIGN=TOP>
<FONT COLOR="#006633"><FONT SIZE="+3"><B>Metamath Proof Explorer Home Page
</B></FONT></FONT></TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif> <A HREF="wn.html">First ></A><BR><A
HREF="grothprim.html">Last ></A></FONT></TD>
</TR></TABLE>
-->
<HR SIZE=1 NOSHADE>
<FONT SIZE=-1><FONT COLOR="#006633">The aleph null above is the symbol
for the first infinite cardinal number, discovered by Georg Cantor in
1873 (see theorem </FONT> ~ aleph0 </FONT><FONT COLOR="#006633">).</FONT>
<HR NOSHADE SIZE=1>
<FONT SIZE=-1><FONT COLOR="#006633">
This is the starting page for the Metamath Proof Explorer subproject
(set.mm database).
See the main </FONT><A
HREF="../index.html">Metamath Home Page</A><FONT COLOR="#006633"> for
an overview of Metamath and download links.
If you wish to contribute your own proofs to the Metamath project, see
<A HREF="../index.html#contribute">How can I contribute to Metamath?</A>
</FONT></FONT>
<HR NOSHADE SIZE=1>
<TABLE BORDER=0 WIDTH="100%"><TR><TD VALIGN=TOP WIDTH="50%">
<B><FONT COLOR="#006633">Contents of this page</FONT></B>
<MENU>
<LI> <A HREF="#overview">Metamath Proof Explorer
Overview</A></LI>
<LI> <A HREF="#proofs">How Metamath Proofs Work</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>23-Apr-2006</I></FONT>
-->
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>20-May-2003</I></FONT>
-->
</LI>
<LI> <A HREF="#axioms">The Axioms</A>
<FONT SIZE=-1>(<A HREF="#scaxioms">Propositional Calculus</A>,
<A HREF="#pcaxioms">Predicate Calculus</A>,
<A HREF="#staxioms">Set Theory</A>,
<A HREF="#groth">The Tarski-Grothendieck Axiom</A>)</FONT>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised </FONT> <FONT
SIZE=-1><I>22-June-2009 (the Tarski-Grothendieck Axiom)</I></FONT>
-->
</LI>
<LI> <A HREF="#class">The Theory of Classes</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>13-Dec-2015</I></FONT>
</LI>
<LI> <A HREF="#theorems">A Theorem Sampler</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>19-May-2003</I></FONT>
-->
</LI>
<LI> <A HREF="#trivia">2 + 2 = 4 Trivia</A>
<FONT SIZE=-1>(<A HREF="#2p2e4length">more</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>22-Dec-2018</I></FONT>)
</FONT>
</LI>
<LI> <A HREF="#axiomnote">Appendix 1: A Note on the Axioms</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>10-Jul-2015</I></FONT>
-->
</LI>
<LI> <A HREF="#traditional">Appendix 2: Traditional
Textbook Axioms of Predicate Calculus</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>6-Oct-2005</I></FONT>
-->
</LI>
<LI> <A HREF="#distinct">Appendix 3: Distinct Variables</A>
<FONT SIZE=-1>(<A HREF="#dv-history">History</A>,
<A HREF="#dv-notes">Notes</A>)</FONT>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>21-Dec-2016</I></FONT>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>16-Jun-2008 (added Note 4)</I></FONT>
-->
</LI>
<LI> <A HREF="#definitions">Appendix 4: A Note on Definitions</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>11-Nov-2014</I></FONT>
-->
</LI>
<LI> <A HREF="#assume">Appendix 5: How to Find Out What Axioms a Proof
Depends On</A></LI>
<LI> <A HREF="#function">Appendix 6: Notation for Function and Operation
Values</A></LI>
<LI> <A HREF="#subsys">Appendix 7: Some Predicate Calculus
Subsystems</A>
</LI>
<LI> <A HREF="#oldaxioms">Appendix 8: Axiom Numbering
Before December 2018</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>26-Dec-2018</I></FONT>
</LI>
<LI> <A HREF="#read">Reading Suggestions</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>23-Aug-2006</I></FONT>
-->
</LI>
<LI> <A HREF="#bib">Bibliography</A></LI>
<LI> <A HREF="#textonly">Browsers and Fonts</A></LI>
<!--
<LI> <A HREF="#textonly">Viewing with a Text Browser</A></LI>
<LI> <A HREF="#unicode">Browsing with the Unicode Font</A>
<LI> <A HREF="#copyright">Copyright Terms</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>8-Aug-2003</I></FONT>
</LI>
-->
</MENU>
</TD>
<TD VALIGN=TOP>
<B><FONT COLOR="#006633">Related pages</FONT></B>
<MENU>
<!--
<LI> <A HREF="mmtheorems.html#mmtc">Table of Contents and Theorem List</A></LI>
-->
<LI> <A HREF="mmtheorems.html">Theorem List (Table of Contents)</A> </LI>
<LI>
<A HREF="mmrecent.html">Most Recent Proofs (this mirror)</A>
(<A HREF="http://us2.metamath.org:88/mpeuni/mmrecent.html">latest</A>)
</LI>
<LI>
<A HREF="conventions.html">Conventions and Style</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>15-Jan-2017</I></FONT>
</LI>
<LI> <A HREF="mmbiblio.html">Bibliographic Cross-Reference</A> </LI>
<LI> <A HREF="mmdefinitions.html">Definition List (3MB)</A> </LI>
<LI>
<A HREF="mmnatded.html">Deduction Form and Natural Deduction</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>7-Feb-2017</I></FONT>
<FONT SIZE=-1>(<A HREF="natded.html">Natural Deduction Rules</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>9-Feb-2017</I></FONT>)</FONT>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT>
<FONT SIZE=-1><I>2-Mar-2008</I></FONT>
-->
</LI>
<LI>
<A HREF="mmdeduction.html">Weak Deduction Theorem</A> (an older method)
</LI>
<LI>
<A HREF="mmcomplex.html">Real and Complex Numbers</A>
</LI>
<LI>
<A HREF="mmtopstr.html">Algebraic and Topological Structures</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>24-Nov-2018</I></FONT>
</LI>
<LI>
<A HREF="mmzfcnd.html">ZFC Axioms With No Distinct Variables</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>12-Apr-2008</I></FONT>
-->
</LI>
<LI>
<A HREF="mmascii.html">ASCII Symbol Equivalents for Text-Only Browsers</A>
</LI>
<LI>
<A HREF="../index.html#contribute">How can I contribute to Metamath?</A>
</LI>
<!-- <LI> <A HREF="mmhil.html">Hilbert Space Explorer Home Page</A></LI> -->
</MENU>
<B><FONT COLOR="#006633">External links</FONT></B>
<MENU>
<LI>
<A HREF="/~https://github.com/metamath/set.mm">GitHub repository</A>
(contains the database as well as help on contributing)
</LI>
<!--
<LI>
<A HREF="http://math.vanderbilt.edu/~~schectex/ccc/choice.html">
A home page for THE AXIOM OF CHOICE</A>
[retrieved 21-Dec-2016] has some interesting set theory information.
</LI>
-->
</MENU>
<FONT SIZE=-1><B><FONT COLOR="#006633">To search this site</FONT></B>
you can use <A HREF="http://www.google.com/">Google</A> [retrieved 21-Dec-2016]
restricted to a mirror site. For example, to find references to
infinity enter "infinity site:us.metamath.org".
<B><FONT COLOR="#006633">More efficient searching</FONT></B> <!-- for
particular symbols and patterns --> is possible with direct use of the <A
HREF="../index.html#mmprog">Metamath program</A>, once you get used to
its <A HREF="mmascii.html">ASCII tokens</A>. See the wildcard features
in "help search" and "help show statement".
</FONT></TD>
</TR></TABLE>
<P><HR NOSHADE SIZE=1><A NAME="overview"></A><B><FONT
COLOR="#006633">Metamath Proof Explorer
Overview</FONT></B>
<!--
<P><CENTER><FONT COLOR="#006633"><I>My intellect never quite recovered
from the strain of writing </I>[Principia
Mathematica]<I>.</I><BR> —Bertrand Russell, <I>The Autobiography of
Bertrand Russell, the Early Years</I></FONT></CENTER>
-->
<!--
"I have been ever since definitely less capable of dealing with
difficult abstractions than I was before"
-->
<!--
<P><CENTER><FONT COLOR="#006633"><I>...today we know
that it is possible, logically speaking, to derive
almost all of present-day mathematics from a single source, the Theory
of Sets.</I><BR> —Nicolas Bourbaki </FONT></CENTER>
-->
<P><CENTER><FONT COLOR="#006633"><I>From <A HREF="pm54.43.html">this
proposition</A> it will follow, when arithmetical addition has been
defined, that 1+1=2.</I><BR> —<I>Principia Mathematica</I>, Volume
I, page 360.</FONT></CENTER>
<!--
<P><CENTER><FONT COLOR="#006633"><I>Mathematics is a game played
according to certain simple rules with meaningless marks on
paper.</I><BR> —David Hilbert</FONT></CENTER>
-->
<P><CENTER><TABLE WIDTH="90%"><TR><TD ALIGN=CENTER> <TABLE BORDER=0
CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA"><TR><TD ALIGN=CENTER>
David A. Wheeler has prepared an excellent 14-minute YouTube video, <A
HREF="https://www.youtube.com/watch?v=8WH4Rd4UKGE">Metamath Proof
Explorer: A Modern Principia Mathematica</A>, on the history of
formalization and the motivation for Metamath,
the proof of 2+2=4, and more. </TD></TR></TABLE>
</TD></TR></TABLE></CENTER>
<P>Inspired by Whitehead and Russell's monumental <I>Principia
Mathematica</I>, <!--(where 1+1=2 is finally proved on page 86 of Volume
II), --> the Metamath Proof Explorer has over 23,000 completely worked
out proofs, starting from the very foundation that mathematics is built
on and eventually arriving at familiar mathematical facts and beyond.
<!-- in logic and set theory. --> <!-- , interconnected with over a million
hyperlinked cross-references. --> Each proof is pieced together with
razor-sharp precision using a simple substitution rule that practically
anyone (with lots of patience) can follow, not just mathematicians. Every step
can be drilled down deeper and deeper into the labyrinth until axioms of
logic and set theory—the starting point for all of
mathematics—will ultimately be found at the bottom. You could
spend literally days exploring the astonishing tangle of logic leading,
say, from the seemingly mundane theorem <A HREF="#trivia">2+2=4</A> back
to these axioms.
<P>Essentially everything that is possible to know in mathematics can be
derived from a handful of axioms known as <I>Zermelo-Fraenkel set
theory,</I> which is the culmination of many years of effort to
isolate the essential nature of mathematics and is one of the most
profound achievements of mankind.
<P>The Metamath Proof Explorer starts with these axioms to build up its
proofs. There may be symbols that are unfamiliar to you, but we show in
detail how they are manipulated in the proofs, and in principle you
don't have to know what they mean. In fact, there is a philosophy
called <I>formalism</I> which says that mathematics is a game of symbols
with no intrinsic meaning. With that in mind, Metamath lets you watch
the game being played and the pieces manipulated according to simple and
precise rules, one step at a time. <!-- Amazingly, the rules - with which
essentially all of mathematics can be derived - are simpler than those
involved in a game of chess! -->
<P>As humans, we observe interesting patterns in these "meaningless"
symbol strings as they evolve from the axioms, and we attach meaning to
them. One result is the set of natural numbers, whose properties match
those we observe when we count everyday objects, and their extensions to
rational and real numbers. Of course, numbers were discovered centuries
before set theory, and historically they were "reversed engineered" back
to the axioms of set theory. The proof of <A HREF="#trivia">2 + 2 =
4</A> shows what was involved in that reverse engineering, representing
the work of many mathematicians from Dedekind to von Neumann. At the
other extreme of abstraction is the theory of infinite sets or
transfinite cardinal numbers. Some of the world's most brilliant
mathematicians have given us deep insight into this mysterious and
wondrous universe, which is sometimes called "Cantor's paradise."
<!-- At the other extreme of
abstraction is the theory of infinite sets or transfinite cardinal
numbers, sometimes called "Cantor's paradise." Some of the world's most
brilliant mathematicians have given us deep insight into this
mysterious and wondrous universe that, so far as we know, exists only in
the mind.
-->
<!--
paradise." Some of the world's most brilliant mathematicians have given
us deep insight into this mysterious and wondrous place that that
transcends the physical universe, giving us a glimpse into a higher
reality, perhaps even the mind of God.
-->
<P>Metamath's formal proofs are much more detailed than the proofs you
see in textbooks. They are broken down into the most explicit detail
possible so that you can see exactly what is going on. Each proof step
represents a microscopic increment towards the final goal. But each
step is derived from previous ones with a very simple rule, and you can
verify for yourself the correctness of any proof with very little skill.
All you need is patience. With no prior knowledge of advanced
mathematics or even any mathematics at all, you can jump into the middle
of any proof, from the most elementary to the most advanced, and
understand immediately how the symbols were mechanically manipulated to
go from one proof step to another, even if you don't know what the symbols
themselves mean. In the next section we show you how.
<P><HR NOSHADE SIZE=1><A NAME="proofs"></A><B><FONT COLOR="#006633">How
Metamath Proofs Work</FONT></B>
<P> <CENTER><FONT COLOR="#006633"><I>A mathematical theory is not to be
considered complete until you have made it so clear that you can explain
it to the first man whom you meet on the street.</I><BR> —David
Hilbert</FONT></CENTER> <P>
<!--
<P> <CENTER><FONT COLOR="#006633"><I>Thus mathematics may be defined as
the subject in which we never know what we are talking about, nor
whether what we are saying is true.</I><BR> —Bertrand
Russell</FONT></CENTER> <P>
<P> <CENTER><FONT COLOR="#006633"><I>The lyf so short, the craft so long
to lerne </I><BR> —Chaucer</FONT></CENTER> <P>
<P> <CENTER><FONT COLOR="#006633"><I>The ultimate goal of mathematics is
to eliminate any need for intelligent thought.</I><BR> —Alfred North
Whitehead </FONT></CENTER> <P>
<P> <CENTER><FONT COLOR="#006633"><I>...mathematical proofs, like
diamonds, are hard as well as clear, and will be touched with nothing
but strict reasoning. </I><BR> —John Locke, <I>Second Reply to the
Bishop of Worcester</I></FONT></CENTER> <P>
<BLOCKQUOTE>
<FONT COLOR="#006633" SIZE=-1> He was 40 yeares old before he
looked on Geometry; which happened accidentally. Being in a Gentleman's
Library, Euclid's Elements lay open, and 'twas the 47 <I>El. libri</I>
I. He read the Proposition. <I>By G__,</I> sayd he (he would now and
then sweare an emphaticall Oath by way of emphasis) <I>this is
impossible!</I> So he reads the Demonstration of it, which referred him
back to such a Proposition; which Proposition he read. That referred
him back to another, which he also read. <I>Et sic deinceps</I> that at
the last he was demonstratively convinced of that trueth. This made him
in love with Geometry.</FONT>
<CENTER><FONT COLOR="#006633" SIZE=-1>—John Aubrey, "A Brief Life of
Thomas Hobbes, 1588-1679" in
<I>Brief Lives</I> (c. 1694) </FONT></CENTER>
</BLOCKQUOTE>
-->
<P><CENTER><TABLE WIDTH="90%"><TR><TD ALIGN=CENTER> <TABLE BORDER=0
CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA"><TR><TD ALIGN=CENTER><IMG
SRC="_nmegill.gif" WIDTH=16 HEIGHT=19
ALT="The Floating Head of Wisdom says: "
TITLE="The Floating Head of Wisdom says: ">
<FONT COLOR="#F7941D"> <B>Read this section
carefully to learn how to follow a Metamath proof.</B>
</FONT></TD></TR></TABLE></TD></TR></TABLE></CENTER>
<!---
<P><FONT SIZE="-1">[If you are a math novice (or not) and have trouble
understanding this section, <A HREF="../email.html">let me know</A> what
you find confusing so that I can try to improve it.
An important point sometimes misunderstood is
that Metamath is <I>not</I> a theorem prover—it does not
find these proofs on its own but just verifies the correctness of proofs
provided to it by its users.]</FONT>
-->
<P> <B><FONT COLOR="#006633">What you need to
know</FONT></B> The only rule you need to know in
order to follow the symbol manipulations
in a Metamath proof is <B>substitution</B>. Substitution
consists of replacing the symbols for variables with expressions
representing special cases of those variables. For example, in
high-school algebra you learned that <I>a</I> + <I>b</I> = <I>b</I> +
<I>a</I>, where <I>a</I> and <I>b</I> are variables (placeholders
for numbers). Two
substitution instances of this law are 5 + 3 = 3 + 5 and (<I>x</I> - 7)
+ <I>c</I> = <I>c</I> + (<I>x</I> - 7). That's the only mathematical
concept you need!
<!-- And if you don't know it, reread this paragraph
until you do! --> Substitution is just writing down a specific
example <!-- or a specialized version --> of a more general formula.
<!--
<B>Exercise:</B> How do we avoid confusion due to the fact that the
<I>b</I> in the second substitution instance also occurs in the original
formula? <B>Answer:</B> Rename the <I>b</I> of the original formula to
some other variable, say <I>d</I>, giving us <I>a</I> + <I>d</I> =
<I>d</I> + <I>a</I>. Then we replace the two occurrences of <I>a</I>
with (<I>b</I> - 7) and the two occurrences of <I>d</I> with <I>c</I>,
yielding the final answer (<I>b</I> - 7) + <I>c</I> = <I>c</I> +
(<I>b</I> - 7).
-->
<P><FONT SIZE="-1">[Note for logicians: The substitution in Metamath
proofs is, indeed, simply the direct replacement of a variable with an
expression. The more complex proper substitution of <A
HREF="#traditional">traditional logic</A> is a derived concept in
Metamath, broken down into multiple primitive steps. <A
HREF="#distinct">Distinct variable</A> provisos, which accompany certain
axioms and are inherited by theorems, forbid unsound
substitutions.]</FONT>
<P> <B><FONT COLOR="#006633">How it works</FONT></B>
To show you how this works in Metamath, we will break down and analyze a
proof step in the proof of 2 + 2 = 4. Once you grasp this example, you
will immediately be able to verify for yourself <I>any</I> proof in the
database—no further prerequisites are needed. You may not understand
what all (or any) of the symbols mean, but you can follow the rules for
how they are manipulated, like game pieces, to prove theorems.
<P><CENTER><TABLE WIDTH="90%"><TR><TD ALIGN=CENTER> <TABLE BORDER=0
CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA"><TR><TD ALIGN=CENTER>
An animated version of the 2+2=4 proof step in this section is
presented starting at 7m32s into David A. Wheeler's <A
HREF="https://www.youtube.com/watch?v=8WH4Rd4UKGE&t=7m32s">Metamath
Proof Explorer: A Modern Principia Mathematica</A>. </TD></TR></TABLE>
</TD></TR></TABLE></CENTER>
<P>Compare this with the years of study it might take to be able to
follow and verify a proof in an advanced math textbook. Typically such
proofs will omit many details, implicitly assuming you have a deep
knowledge of prior material. If you want to be a mathematician, you
will still need those years of study to achieve a high-level
understanding. Metamath will not provide you with that. But if you
just want the ability to convince yourself that a string of math symbols
that mathematicians call a "theorem" is a mechanical consequence of the axioms,
Metamath's proof method lets you accomplish that.
<P>Metamath's conceptual simplicity has a tradeoff, which is the often
large number of steps needed for a complete proof all the way back to
the axioms. But the proofs have been computer-verified, and you can
choose to study only the steps that interest you and still have complete
confidence that the rest are correct.
<P> <A NAME="figure1"></A>
<TABLE ALIGN=CENTER WIDTH="10%"><TR><TD>
<IMG BORDER=0 SRC="_proofstep.gif"
WIDTH=592 HEIGHT=369
ALT="Breakdown of a proof step. Credit: N. Megill 2003. Public domain."
TITLE="Breakdown of a proof step. Credit: N. Megill 2003. Public domain."
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD></TR>
<TR><TD ALIGN=CENTER><FONT SIZE="-1"><B>Figure 1.</B> Step 2 of the 2p2e4
proof references step 1, which in turn "feeds" the hypothesis of earlier
theorem oveq2i (which used to be called opreq2i). The conclusion (assertion)
of oveq2i then generates
step 2 of 2p2e4. Carefully note the substitutions (lassoed in thin orange
lines) that take place. <BR><BR>
<!-- <FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> --> <FONT
SIZE=-1><I>21-Mar-2007</I></FONT>
See also Paul Chapman's <A HREF="_mmbrows2p2e4.png">Metamath browser
screenshot</A>, which shows the substitutions
explicitly.</FONT></TD></TR>
</TABLE>
<P>In the figure above we show part of the proof of the theorem 2 + 2 =
4, called ~ 2p2e4 in the database. We
will show how we arrived at proof step 2, which is an intermediate
result stating that (2 + 2) = (2 + (1 + 1)). (This figure is from an
older version of this site that didn't show indentation levels, and it
is less cluttered for the purpose of this tutorial. The indentation
levels and the <A HREF="../index.html#pink">little <!-- pink --> colored
numbers</A> can make a higher-level view of the proof easier to grasp.)
<!-- <P><FONT COLOR="#F7941D" FACE=sans-serif><B>(1)</B></FONT> -->
-<P><IMG SRC='_orange1circ.gif' WIDTH=19 HEIGHT=19 ALT='(1)'>
Look at Step 2 of the proof.
In the Ref column, we see that it references a previously proved theorem,
~ oveq2i . The theorem oveq2i requires a
hypothesis, and in the Hyp column of Step 2 we indicate that Step 1 will
satisfy (match) this hypothesis.
<P><IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19 ALT='(2)'>
We make
substitutions into the variables of the hypothesis of oveq2i so that it
matches the string of symbols in
the Expression column for Step 1. To achieve this, we substitute
the expression "2" for variable
` A `
and the expression "(1 + 1)" for variable
` B ` .
The middle symbol in the hypothesis of oveq2i is
"=", which is a constant, and we are not allowed to substitute
anything for a constant. Constants must match exactly.
<P>Variables are always colored, and constants are always black (except
the gray turnstile ` |- ` ,
which you may ignore). This makes them easy to recognize.
<!--
The variables in our database have 3 possible colors, <FONT
COLOR="#0000FF">blue</FONT>, <FONT COLOR="#FF0000">red</FONT>, and <FONT
COLOR="#CC33CC">purple</FONT>, representing wffs, sets, and classes
respectively. Don't worry about what these terms mean right now. All
variables, regardless of color, follow the same substitution rule.
-->
In our example, the purple uppercase italic letters are variables,
whereas the symbols
"(", ")", "1", "2", "=", and "+" are constants.
<P>In this example, the constants are probably familiar symbols. In
other cases they may not be. You should focus only on whether the symbols
are variables or constants, not on what they "mean." Your only goal is
to determine what substitutions into the variables of the referenced
theorem are needed to make the symbol strings match.
<P><IMG SRC='_orange3circ.gif' WIDTH=19 HEIGHT=19 ALT='(3)'>
In the Expression column of the Assertion box of oveq2i, there are 4
variables,
` A ` ,
` B ` ,
` C ` ,
and
` F ` .
Because we have already made substitutions into the
hypothesis, variables
` A ` and
` B ` have been
committed to the assignments "2" and "(1 + 1)" respectively, and
we can't change these assignments. However, the new variables
` C `
and
` F `
are free to be assigned with any expression we want (subject to the
legal syntax
requirement described below). By substituting "2" for
` C ` and
"+" for
` F ` , we end up with
(2 + 2) = (2 + (1 + 1)) that we show in the Expression column
for Step 2 of the proof of 2p2e4.
<P><FONT SIZE="-1">[It may seem peculiar to substitute a + sign for a
variable, because you wouldn't do that in high-school algebra. We can
do this because the variables represent arbitrary objects called
"classes," not just numbers. See the description for operation value
~ df-ov (don't worry about right-hand
side of the definition, for now). A number and a + sign are both classes.
You have to free your mind to forget about high-school algebra—pretend
you have no idea what a number or "+" is—and just look at what happens
to the symbols, independent of any meaning. In fact (and ironically),
it may be better to look at a proof where all the symbols are
unfamiliar, perhaps ~ aleph1re , so that you
can observe the mechanical symbol substitutions without the distraction
of preconceived notions.]</FONT>
<P>When we first created the proof, why did we choose these particular
substitutions for ` C `
and ` F `?
The reason is simple—they make the proof work! But how did we know
these particular substitutions should be picked, and not others? That's
the hard part—we didn't know, nor did we know that oveq2i should be
referenced in the second proof step, nor did we know that Step 1 would
have the right expression to match the hypothesis of oveq2i. The
choices were made using intelligent guesses, that were then verified to
work. This is a skill a mathematician develops with experience. Some
of the proofs in our database were discovered by famous mathematicians.
The Metamath Proof Explorer recaptures their efforts and shows you in
complete detail the proof steps and substitutions already worked out.
This allows you to follow a proof even if you are not a mathematician,
and be convinced that its conclusion is a consequence of the axioms.
<P>Sometimes a referenced theorem (or axiom or definition) has no
hypotheses. In that case we omit <IMG SRC='_orange1circ.gif' WIDTH=19
HEIGHT=19 ALT='(1)'> and <IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19
ALT='(2)'> above and immediately proceed to <IMG SRC='_orange3circ.gif'
WIDTH=19 HEIGHT=19 ALT='(3)'>. When there are multiple hypotheses, we
repeat <IMG SRC='_orange1circ.gif' WIDTH=19 HEIGHT=19 ALT='(1)'> and
<IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19 ALT='(2)'> for each one.
<P><CENTER><TABLE WIDTH="90%"><TR><TD ALIGN=CENTER> <TABLE BORDER=0
CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA"><TR><TD ALIGN=CENTER><IMG
SRC="_nmegill.gif" WIDTH=16 HEIGHT=19
ALT="The Floating Head of Wisdom says: "
TITLE="The Floating Head of Wisdom says: ">
<FONT COLOR="#F7941D"> <B>Done!
You should now be
able to figure out any Metamath proof. In other words, you should be
able to draw a diagram like the one above for any proof step of any proof.</B>
</FONT></TD></TR></TABLE></TD></TR></TABLE></CENTER>
<P>You may want to practice the above procedure for a few other proof
steps to make sure you have grasped the idea.
<P>The rest of this section has some notes on substitutions that you may
find helpful and describes the additional requirements for correctness
not mentioned above. As you will observe if you study a few proofs, the
Metamath proof verifier has already ensured these requirements are met,
so ordinarily you don't have to worry about them.
<P>
<B><FONT COLOR="#006633">Notes on substitutions</FONT></B>
<MENU>
<LI>Substitutions are simultaneous. In other words each occurrence of a
given variable in a referenced theorem must be replaced with the same
expression. For example, there are two occurrences of
` F `
in the Assertion of oveq2i, and both occurrences must be replaced with
the same expression, which is "+" in the above example. </LI>
<LI>Substitutions are made into the variables of the referenced theorem
only, never into the variables of any proof step referenced
in the Hyp column (of the theorem being proved). <I>In other words you
should pretend that all variables in the theorem being proved are
constants for the purpose of figuring out the substitutions.</I> You can
see this by looking at examples such as theorem ~ id1 . To follow the proof
of ~ id1 , you should treat the symbol ` ph ` as if it were a
constant symbol, when you are figuring out the substitutions to make
into the variables of the referenced theorems (or axioms).</LI>
<LI>If the variables of a referenced theorem (or axiom) happen to have
the same names as those in the theorem being proved, you may want to
temporarily rename the variables in the referenced theorem (or axiom)
before substituting expressions for them, to avoid confusion. For
example, the proof of ~ id1 will be less confusing
if the occurrences of ` ph `
in the referenced axioms are renamed to something else.
Specifically, you can rewrite ~ ax-1 as say
` ( ch -> ( ps -> ch ) ) ` .
Then, to obtain step 2 of the proof of id1, substitute "` ph `" for ` ch `
and "` ( ph -> ph ) `" for ` ps ` .
</LI>
</MENU>
<P> <B><FONT COLOR="#006633">Legal syntax</FONT></B>
There is a further requirement for substitutions we have not described
yet. You can't substitute just any old string of symbols for a purple
class variable. Instead, the symbol string must qualify as a class
expression. For example, it would be illegal to substitute the
nonsensical "(1 +" for variable ` B ` above. However, "(1 + 1)" is legal.
Here is how you can tell. "1" is a legal class by ~ c1 . "+" is a
legal class by ~ caddc . Then, by making these
class substitutions into the class variables of ~ co , we see that "(1 + 1)"
is a legal class. But there is no such construction that would let us show
that the nonsensical "(1 +" is a legal class.
<!--
<P><FONT SIZE="-1">[On the other hand, the fact that 1 and + are both
classes means we are allowed to substitute them for any class variables
at all, even where they normally wouldn't go. For example, it is legal
to substitute + for <I><FONT COLOR="#CC33CC">C</FONT></I> and 1 for
<I><FONT COLOR="#CC33CC">F</FONT></I> in oveq2i above, resulting in the
seemingly nonsensical ( + 1 2 ) = ( + 1 ( 1 + 1 ) ). Believe it or not,
this is a perfectly valid theorem of set theory! However, it jumps out
of the subtheory of arithmetic and is of little use; it certainly
doesn't help us make progress towards a proof of ( 2 + 2 ) = 4.
-->
<!--
If this bothers
you, consider the following analogy: any random collection of syntactically
legal statements in a computer language constitute a valid program,
even though the program would be of little use.
-->
<!--
We can play around with such ideas for fun to prove silly but still
perfectly valid theorems
like ~ avril1 , which if nothing else provides an
interesting exercise for figuring out the substitutions involved in its
proof.]</FONT>
-->
<P>Similarly, blue wff variables and red setvar variables can be substituted
only with expressions that qualify as those types.
<P>In other words, we must "prove" that any expression we want to
substitute for a variable qualifies as a legal expression for that type
of variable, before we are allowed to make the substitution.
<P>The actual proofs stored in the database have additional steps that
construct, from syntax definitions, the expressions that are
substituted for variables. We suppress these construction steps on the
web pages because they would make the proofs very long and tedious.
However, the syntax breakdown is straightforward to check by hand if you
make use of the "Syntax hints" provided with each proof. Once you get
used to the syntax, you should be able to "see" its breakdown in your
head; in the meantime you can trust that the Metamath proof verifier did
its job.
<P>If you want to see for yourself the hidden steps that construct the
variable substitutions for each proof step, you can display them using
the Metamath program. For the proof above, use the commands "save proof
2p2e4 /normal" followed by "show proof 2p2e4 /all" in the Metamath
program. (Follow the instructions for downloading and running the <A
HREF="../index.html#mmprog">Metamath program</A>. Try it, it's easy!)
In the "/all" proof display, you will see that step 21 corresponds to
step 2 of the figure above. Steps 14-17 are the hidden steps showing
that "(1 + 1)" is a legal class as we described above. To see the
substitutions we talked about for step 2, you can type "show proof 2p2e4
/detailed_step 21".
<P>In the case of axioms and definitions, we <I>do</I> show their
detailed syntax breakdown, because there is free space on those web
pages not used for anything else. These can help you become familiar
with the syntax. For example, look at the definition of the number 2,
~ df-2 . You can see, at step 4, the demonstration
that "(1 + 1)" is a legal expression that qualifies as a class, i.e.
that can be substituted for a purple class variable.
<P> <B><FONT COLOR="#006633">Distinct variable
restrictions</FONT></B> Our final requirement for
substitutions is described in <A HREF="#distinct">Appendix 3: Distinct
Variables</A> below. These restrictions have no effect on how you
figure out the the substitutions that were made in a proof step. All
they do is prohibit certain substitutions that would otherwise be legal
based what we have described so far. Eventually you should learn how
they work in order to complete your understanding of the mechanics of
logic, but for now, you can trust that the Metamath proof verifier has
ensured that they have been met.
<P> <B><FONT COLOR="#006633">Class
variables</FONT></B> Our example of 2+2=4, with its
purple class variables, depends on a definitional mechanism that
extends the wff and setvar variables used in the axioms to greatly simplify
our presentation. After the axiom section below, we describe the <A
HREF="#class">theory of classes</A>, which you should read to understand
how these tie into the primitive concepts used by the axioms.
<P> <HR NOSHADE SIZE=1><A NAME="axioms"></A><B><FONT COLOR="#006633">The
Axioms </FONT></B>
<!--
<P><CENTER><FONT COLOR="#006633"><I>Everything should be made as simple
as possible, but not simpler.</I><BR> —attributed to Albert
Einstein</FONT></CENTER>
-->
<P><CENTER><FONT COLOR="#006633"><I>Perfection is when there is no longer
anything more to take away.</I><BR> —Antoine de
Saint-Exupery</FONT></CENTER>
<P><FONT SIZE="-1">[The material in this section is intended to be
self-contained. However, you may also find it helpful to review <A
HREF="../index.html#start">these suggestions</A>.
<!-- and take a quick look
at this <A HREF="../mmsolitaire/mms.html#q5">summary of symbols</A>. -->
A
more extensive but still informal overview is given in Chapter 3,
"Abstract Mathematics Revealed," of the <A
HREF="../downloads/metamath.pdf"><I>Metamath</I> book</A> (1.3 MB PDF
file; click on the fourth bookmark in your PDF reader).]</FONT><P>
An <B>axiom</B> is a fundamental assumption that provides a starting
point for reasoning.
The axioms for (essentially) all of mathematics can be conveniently
divided into three groups: <B>propositional calculus,</B> <B>predicate
calculus,</B> and <B>set theory</B>. Each axiom is a string of
mathematical symbols of two kinds: <B>constants</B>, also called
<B>connectives</B>, which we show in black; and <B>variables</B>, which
we show in color. The constants that occur in the axioms are
` ( ` ,
` ) ` ,
` -> ` ,
` -. ` ,
` = ` ,
` e. ` , and
` A. `
(left parenthesis, right parenthesis, implies, not, equals, is contained
in, for all).
<P>Variables are placeholders that can be substituted with other
expressions (strings of symbols). There are two kinds of variables in
the axioms, <B>setvar variables</B> (lowercase italic letters in
<FONT COLOR="#FF0000">red</FONT>) and
<B>wff ("well-formed formula") variables</B> (lowercase Greek letters
in <FONT
COLOR="#0000FF">blue</FONT>). A wff variable can be
substituted with any expression qualifying as a wff (see below).
A setvar variable can be substituted only with another setvar variable
(in other words with an expression of length one, whose only symbol is a
setvar variable) since there are no rules that let us construct more
complex expressions for them. We call these "setvar variables" rather
than just "set variables" to emphasize this restriction. The reason for
this restriction is that they often serve as bound or dummy variables in
expressions, i.e. the first argument of the ` A. ` quantifier connective
introduced below. It is the same reason that you can't substitute say 2
for x in "the integral of x dx" to result in "the integral of 2 d2",
which would be nonsense.
<P><FONT SIZE="-1">[In later proofs you will see a third kind of variable,
called a <B>class variable</B>, which is shown in <FONT
COLOR="#CC33CC">purple</FONT> (usually as uppercase italic letters) and
is a kind of generalization of the setvar variable that can be
substituted with expressions such as 2 or ` ( _pi + 3 ) `. The <A
HREF="#class">theory of classes</A> will be discussed in the next
section.]</FONT><P>
Following the tradition in the literature, we use italic Greek letters for
wff variables and lower-case italic letters for setvar variables.
<P><FONT SIZE="-1">[If you
use a monochrome display or printout, or are colorblind, the red variables are
lowercase italic
letters, the purple ones uppercase italic, and the blue ones
italic Greek. Sometimes we use mathematical symbols (such as +)
as class variables, and in that case they are distinguished by both the
purple color and a dotted underline. In all cases,
the colors are not necessary to disambiguate the symbols. You
can see the list of all symbols including variables on the
<A HREF="mmascii.html">ASCII Symbol Equivalents</A> page.]</FONT><P>
Any mathematical object whatsoever, such as the number 2, the
operation of taking a square root, or the surface of a sphere, is
considered to be a <B>set</B> in set theory. The red setvar variables
represent arbitrary sets such as these. (You can't substitute
the expressions for these sets directly into the setvars, as discussed
above, but must use the setvars as part of a formula that specifies the
properties of these sets indirectly. Our theory of classes in the
next section makes direct substitutions possible, giving us an
often more convenient mechanism for practical work.)
<P><I>A set can be equal to another set, can be contained in another
set, and can contain other sets.</I> <!-- ("Is contained in," "is a
member of," "is an element of," and "belongs to" mean the same thing.)
--> For example, the set of real numbers contains, of course, all of the