-
Notifications
You must be signed in to change notification settings - Fork 88
/
mmset.raw.html
6057 lines (5500 loc) · 255 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"
"https://www.w3.org/TR/html4/loose.dtd">
<!-- The file mmset.html is generated from mmset.raw.html -
see the regen-from-raw script for details -->
<HTML LANG="EN-US">
<!-- To convert mmset.raw.html to mmset.html, use the metamath.exe command:
markup mmset.raw.html mmset.html /alt_html /symbols /css /labels
-->
<!-- Warning (4-Aug-2021): The link https://validator.w3.org/check?uri=referer
on the bottom right of this page no longer works correctly (it checks the wrong
page, so you may be tricked into thinking there are no errors). Instead, paste
the URL of this page directly into https://validator.w3.org/ or use their
upload feature. -->
<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 ~ aleph0 ).
</FONT>
</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></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="https://us.metamath.org/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>
-->
</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="mmfrege.html">Frege Notation</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>7-Nov-2020</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>
Miscellaneous <A HREF="mmnotes.txt">notes</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]
<BR>
—Bertrand Russell,
<I>The Autobiography of Bertrand Russell, the Early Years</I>
</FONT>
</CENTER>
-->
<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>I have been ever since definitely less capable of dealing with difficult
abstractions than I was before.</I>
— Bertrand Russell
</FONT>
</CENTER>
-->
<!--
<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 26,000 completely worked out proofs in its
main sections (and over 41,000 counting "mathboxes", which are annexes where
contributors can develop additional topics), 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>
<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>
<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>
<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."
</P>
<!--
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.
-->
<!--
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>
<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>
<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>
<CENTER>
<FONT COLOR="#006633">
<I>The lyf so short, the craft so long to lerne </I>
<BR>
—Geoffrey Chaucer
</FONT>
</CENTER>
<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>
<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.
</P>
<!--
<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> conditions, which accompany certain
axioms and are inherited by theorems, forbid unsound substitutions.]
</FONT>
</P>
<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>
<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>
<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>
<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>
<!-- <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>
<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>
<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>
<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>
<P>
<IMG SRC='_orange3circ.gif' WIDTH=19 HEIGHT=19 ALT='(3)'>
In the Expression column of the Assertion box of ~ oveq2i , there are four
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>
<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>
<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>
<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>
<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>
<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>
<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 ~ idALT . To follow the proof
of ~ idALT , 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 ~ idALT 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 ~ idALT , substitute "` ph `" for ` ch `
and "` ( ph -> ph ) `" for ` ps ` .
</LI>
</MENU>
<P id="legal_syntax">
<B><FONT COLOR="#006633">Legal syntax</FONT></B>
There is a further requirement for Metamath 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>
<!--
<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>
-->
<P>
Similarly, blue wff variables and red setvar variables can be substituted only
with expressions that qualify as those types.
</P>
<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. This also states precisely what is being
substituted, preventing any ambiguity.
</P>