forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
mmnotes.txt
9166 lines (7243 loc) · 417 KB
/
mmnotes.txt
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
mmnotes.txt - Notes
-------------------
These are informal notes on some of the recent proofs and other topics.
(7-Dec-2020) Partial unbundling of ax-7, ax-8, ax-9 (notes by Benoit Jubin)
---------------------------------------------------------------------------
This note discusses the recent partial unbundling of the axiom of
equality ax-7 and the predicate axioms ax-8 and ax-9 in set.mm.
The axiom of equality asserts that equality is a right-Euclidean binary relation
on variables:
ax-7 |- ( x = y -> ( x = z -> y = z ) )
It can be weakened by adding a DV (disjoint variable) condition on x and y:
ax7v |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y)
and this scheme can itself be weakened by adding extra DV conditions:
ax7v1 |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y) , DV(x,z)
ax7v2 |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y) , DV(y,z)
We prove, in ax7, that either ax7v or the conjunction of ax7v1 and ax7v2
(together with earlier axioms) suffices to recover ax-7. The proofs are
represented in the following simplified diagram (equid is reflexivity and
equcomiv is unbundled symmetry):
--> ax7v1 --> equid --
/ \
ax-7 --> ax7v -- --> equcomiv --> ax7
\ /
--> ax7v2 ------------
The predicate axioms ax-8 and ax-9 can be similarly weakened, and the proofs are
actually simpler, now that the equality predicate has been proved to be an
equivalence relation on variables. This is a general result. If an n-ary
predicate P is added to the langugage, then one has to add the following n
predicate axioms for P:
ax-P1 |- ( x = y -> ( P(x, z_2, ..., z_n) -> P(y, z_2, ..., z_n) ) )
...
ax-Pn |- ( x = y -> ( P(z_1, ..., z_{n-1}, x) -> P(z_1, ..., z_{n-1}, y) ) )
Any of these axioms can be weakened by adding the DV condition DV(x,y), and it
is also sufficient to replace it by the conjunction of the two schemes:
ax-Piv1 |- ( x = y ->
( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) ) , x fresh
ax-Piv2 |- ( x = y ->
( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) ) , y fresh
where "fresh" means "disjoint from all other variables". The proof is similar
to ax8 and ax9 and simply consists in introducing a fresh variable, say t, and
from
|- ( x = t -> ( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., t, ..., z_n) ) )
|- ( t = y -> ( P(z_1, ..., t, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) )
|- ( x = y -> E. t ( x = t /\ t = y ) )
one can prove axPi.
Note that ax-7 can also be seen as the first predicate axiom for the binary
predicate of equality. This is why it does not appear in Tarski's FOL system,
being a special case of his scheme ( x = y -> ( ph -> ps ) ) where ph is an
atomic formula and ps is obtained from ph by substituting an occurrence of x
for y. The above paragraphs prove that this scheme can be weakened by adding
the DV condition DV(x,y).
===============================================================================
(21-Dec-2017) Processing of $[ ... $] file inclusions
-----------------------------------------------------
See also the following Google Group posts:
Description and example:
https://groups.google.com/d/msg/metamath/4B85VKSg4j4/8UrpcqR4AwAJ
"Newbie questions":
https://groups.google.com/d/msg/metamath/7uJBdCd9tbc/dwP2jQ3GAgAJ
"Condensed version of set.mm?":
https://groups.google.com/d/msg/metamath/3aSZ5D9FxZk/MfrFfGiaAAAJ
Original proposal:
https://groups.google.com/d/msg/metamath/eI0PE0nPOm0/8O9s1sGlAQAJ
(Updated 31-Dec-2017: 1. 'write source.../no_delete' is now 'write
source.../keep_includes'. 2. Added 'set home_directory' command; see
'help set home_directory'.)
(Updated 1-Jan-2018: Changed 'set home_directory' to 'set root_directory'.)
(Updated 1-Nov-2019: Added Google Group links above.)
1. Enhanced "write source" command
----------------------------------
The "write source" command in metamath.exe will be enhanced with a
"/split" qualifier, which will write included files separately. The name
of the main (starting) file will be the "write source" argument (as it
is now), and the names of included files will be taken from the original
file inclusions.
2. New markup-type directives related to file inclusions
--------------------------------------------------------
Recall the file inclusion command, "$[ file.mm $]", given in the
Metamath spec. The spec will be clarified so that, for basic .mm file
verification, this command should be ignored when it occurs inside of a
comment (and it should exist only at the outermost scope, as well).
The metamath.exe program will perform additional actions based on
special markup comments starting "Begin $[", "End $[", and "Skip $[".
These are not part of the Metamath spec and can be ignored by basic
verifiers. The metamath.exe program allows the .mm file to be written
as a whole or to be split up into modules (with "write source ...
/split"), and this markup controls how the modules will be created. In
particular, the markup allows us to go back and forth seamlessly between
split .mm files and a single unsplit .mm file.
These markup comments are normally created automatically whenever a .mm
file containing includes is written by "write source" without the
"/split" qualifier. They can also be inserted by hand to delineate how
the .mm file should be split into modules. They are converted back to
file inclusions when "write source" is used with the "/split" qualifier.
"$( Begin $[ file.mm $] $)" - indicates where an included file starts
"$( End $[ file.mm $] $)" - indicates where an included file ends
"$( Skip $[ file.mm $] $)" - indicates there was a file inclusion
at this location in the split files, that wasn't used because
file.mm was already included earlier.
To summarize: Split files will have only "$[ file.mm $]" inclusions,
like before. An unsplit file will have only these three special comments.
(Per the Metamath spec, recall that when a file is included more than
once, only the first inclusion will happen with subsequent ones ignored.
This feature allows us to create subsections of a .mm file that are
themselves stand-alone .mm files. We need the "Skip" directive to mark
the location of ignored inclusions.)
The "read" command will accept either a single file or split files or
any combination (e.g. when the main file includes a file that originally
also contained includes but was separately written without "/split").
Files can contain any combination of inclusion directives $[ $] and the
3 special comments, except that each "$( Begin $[..." must have a
matching "$( End $[...".
3. Behavior of "read" command
-----------------------------
The "read" command builds an internal buffer corresponding to an unsplit
file. If "write source" does not have the "/split" qualifier, this
buffer will become the new source file.
When "read" encounters an inclusion command or one of the 3 special
comments, the following actions are taken:
Case 3.1:
---------
"$[ file.mm $]"
If file.mm has not already been included, this directive will
be replaced with
"$( Begin $[ file.mm $] $) <file.mm content> $( End $[ file.mm $] $)"
If file.mm doesn't exist, an error will be reported.
If file.mm has already been included, this directive will
be replaced with "$( Skip $[ file.mm $] $)".
Case 3.2:
---------
"$( Begin $[ file.mm $] $) <file.mm content> $( End $[ file.mm $] $)"
If file.mm has not already been included, this directive will
be left alone i.e. will remain
"$( Begin $[ file.mm $] $) <file.mm content> $( End $[ file.mm $] $)"
If file.mm has already been included, this directive including the
<file.mm content> will be replaced with "$( Skip $[ file.mm $] $)".
Before discarding it, <file.mm content> will be compared to the content
of file.mm previously included, and if there is a mismatch, a warning
will be reported.
Case 3.3:
---------
"$( Skip $[ file.mm $] $)"
If file.mm has not already been included, this directive will
be replaced with
"$( Begin $[ file.mm $] $) <file.mm content> $( End $[ file.mm $] $)".
If file.mm doesn't exist, an error will be reported.
If file.mm has already been included, this directive will
be left alone i.e. will remain "$( Skip $[ file.mm $] $)".
Error handling:
---------------
Any comments that don't exactly match the 3 patterns will be silently
ignored i.e. will act as regular comments. For example,
"$( Skip $[ file.mm $)" and "$( skip $[ file.mm $] $)" will act as
ordinary comments. In general, it is difficult to draw a line between
what is a comment and what is a markup with a typo, so we take the most
conservative approach of not tolerating any deviation from the patterns.
This shouldn't be a major problem because most of the time the markup
will be generated automatically.
Error messages will be produced for "$( Begin $[.." without a matching
"$( End $[..." (i.e. with the same file name) and for included files
that are missing.
4. Behavior of "write source" command
-------------------------------------
When "write source" is given without the "/split" qualifier, the
internal buffer (as described above) is written out unchanged. When
accompanied by the "/split" qualifier, the following actions are taken.
Case 4.1:
---------
"$[ file.mm $]"
(This directive should never exist in the internal buffer unless
there is a bug.)
Case 4.2:
---------
"$( Begin $[ file.mm $] $) <file.mm content> $( End $[ file.mm $] $)"
file.mm will be created containing "<file.mm content>". The directive
will be changed to "$[ file.mm $]" in the parent file.
Case 4.3:
---------
"$( Skip $[ file.mm $] $)"
This directive will be changed to "$[ file.mm $]" in the
parent file.
5. File creation and deletion
-----------------------------
When "write source" is used with "/split", the main file and all
included files (if they exist) will be overwritten. As with the
existing "write source", the old versions will be renamed with a "~1"
suffix (and any existing "~1" renamed to "~2" and so on through "~9",
whose existing version will be deleted).
When "write source" is used without "/split", the main file will be
overwritten, and any existing included files will be deleted. More
precisely, by "deleted" we mean that an existing included file will be
renamed to "~1", any existing "~1" renamed to "~2", etc. until "~9",
which will be actually deleted. The purpose of doing this is to prevent
accidental edits of included files after the main file is written
without "/split" and thus causing confusing diverging versions.
A new qualifier, "/no_versioning", will be added to "write source" to
turn off the "~n" versioning if it isn't wanted. (Personally,
versioning has helped me recover from mistakes, and it's easy enough to
"rm *~*" at the end of a work session.)
Another new qualifier, "/keep_includes", will be added to "write source" to
turn off the file deletion when "/split" is not specified. This can be
useful in odd situations. For example, suppose main.mm includes abc.mm
and (stand-alone) def.mm, and def.mm also includes abc.mm. When writing
out def.mm without "/split", by default abc.mm will be deleted, causing
main.mm to fail. (Another way to recover is to rewrite def.mm with
"/split". Or recover from abc.mm~1.)
5. Comments inside of includes
------------------------------
A comment inside of a file inclusion, such as
"$[ file.mm $( pred calc $) $]", will be silently deleted when it is
converted to the nonsplit version e.g. "$( Skip $[ file.mm $] $)".
Instead, put the comment before or after the inclusion, such as
"$[ file.mm $] $( pred calc $)".
6. Directories
--------------
Officially, directories aren't supported. In practice, an included file
in a subdirectory can be specified by its path relative to the current
working directory (the directory from which metamath.exe is launched).
However, it is strongly recommended to use "-" in the file name rather
than directory levels, e.g. set-mbox-nm.mm, and this will be a
requirement for set.mm at this time.
A new command was added to change the working directory assumed by the
program. See 'help set root_directory'.
Therefore, if included files are present, you shouldn't read set.mm from
another directory with a command such as "read test/set.mm", because
included files will _not_ be assumed to be in test/. Instead, you
should either launch metamath.exe from the test/ directory, or you
should 'set root_directory test' so that you can type "read set.mm".
(Usually the error messages will let you know right away when your
included files aren't found where expected.)
The reason we don't just extract and use the "test/" prefix of set.mm
automatically is that if we decide to support directories relative to
the root directory, it will be legitimate to "read mbox/mbox-nm.mm",
where mbox/ is a project subdirectory under the root directory.
(End of "(21-Dec-2017) Proposed pocessing of $[ ... $] file inclusions")
(14-May-2017) Dates in set.mm
-----------------------------
Dates below proofs, such as "$( [5-Nov-2016] )$", are now ignored by
metamath.exe (version 0.143, 14-May-2017). Only the dates in
"(Contributed by...", "(Revised by...", and "(Proof shortened by...)"
are used for the Most Recent Proofs page and elsewhere.
If a "(Contributed by...)" markup tag is not present in a theorem's
comment _and_ the proof is complete, then "save new_proof" or
"save proof" will add "(Contributed by ?who?, dd-mmm-yyyy.)" to the
theorem's comment, where dd-mmm-yyyy is today's date.
You can either change the "?who?" to your name in an editor, or you can
use the new command "set contributor" to specify it before "save
new_proof" or "save proof". See "help set contributor".
If you are manually pasting proofs into set.mm, say from mmj2, then at
the end of the day you can run "save proof */compressed/fast" to add
missing contributor dates, followed by a global replacement of "?who?"
with your name.
"verify markup" in Version 0.143 includes some additional error checking,
which will cause warnings on older versions of set.mm. However, it
no longer checks the dates below proofs.
The dates below proofs will be deleted soon in set.mm. If someone
is using them outside of the metamath program, let me know so I can
postpone the deletion. The old code to check them can be re-enabled
by uncommenting "#define DATE_BELOW_PROOF" in mmdata.h.
For converting old .mm files to the new "(Contributed by...)" tag, the
program has the following behavior: the date used is the (earlier) date
below the proof if it exists, otherwise it is today's date. Thus an old
.mm file can be converted with "read xxx.mm", "save proof
*/compressed/fast", and "write source xxx.mm". Note that if there are
two dates below the proof, the second one is used, and the first one is
intended for a "(Revised by...)" or "(Proof shortened by...)" tag that
must be inserted by hand. Searching for "] $) $( [" will identify cases
with two dates that must be handled with manual editing.
Tip: if you want to revert to the old way of checking (and inserting)
dates below proofs, uncomment the "#define DATE_BELOW_PROOF" in mmdata.h
before compiling.
(11-May-2016) New markup for isolating statements and protecting proofs
-----------------------------------------------------------------------
(Updated 10-Jul-2016: changed "show restricted" to "show discouraged";
added "set discouragement off"; see below.)
Two optional markup tags have been defined for use inside of
statement description comments:
"(Proof modification is discouraged.)"
"(New usage is discouraged.)"
The metamath program has been updated to discourage accidental proof
modification or accidental usage of statements with these tags.
These tags have been added to set.mm in the complex number construction,
axiomatic studies, and obsolete sections, as well as to specific
theorems that normally should be avoided or should not have their proof
changed for various reasons. I also added them to some mathboxes (AS
and JBN) having theorems or notation that are unconventional.
Most users will never encounter the effect of "discouraged" tags since
they are in areas that are normally not touched or used.
"write source.../rewrap" will prevent the new tags from being broken
across lines. This is intended to make editing tasks easier. For
example, if you are doing a major revision to a "discouraged" section
such as the complex number construction, you can change the tags
temporarily (like changing "is discouraged" to "xx discouraged"
throughout the section) then change them back when done.
The following commands recognize "(Proof modification is discouraged.)":
"prove", "save new_proof"
The following commands recognize "(New usage is discouraged.)":
"assign", "replace", "improve", "minimize_with"
In the description below, the term "restricted" means a statement's
comment has one or both of the new tags.
Originally, I was going to ask an override question when encountering a
restricted statement, but I decided against that because prompts become
unpredictable, making the user's "flow" awkward and scripts more
difficult to write. Instead, the user can specify "/override" in the
command to accomplish this.
A warning or error message is issued when there is a potential use or
modification of a restricted statement. An error message means the
requested action wasn't performed (because the user didn't specify
"/override"), and a warning message means the action was performed but
the user should be aware that the action is "discouraged". To make the
messages more visible, they have a blank line before and after them, and
they always begin with ">>>" for emphasis.
The behavior of individual commands is as follows.
"prove" - Without "/override", will give an error message and prevent
entering the Proof Assistant when a proof is restricted i.e. when the
statement's comment contains "(Proof modification is discouraged.)".
With "/override", a warning is issued, but the user may enter the Proof
Assistant.
"save new_proof" - Without "/override", will give an error message and
prevent saving. With "/override", a warning is issued, but the save is
allowed.
"assign", "replace" - Without /override, will give an error message and
not allow an assignment with a restricted statement i.e. when the
assigned statement's comment contains "(New usage is discouraged.).
With /override, will give a warning message but will do the assignment.
"improve", "minimize_with" - Without /override, will silently skip
restricted statements during their scans. With /override, will consider
all statements and will give a warning if any restricted statements are
used.
Here is an example of a session with idALT, which has the comment tag
"(Proof modification is discouraged.)".
MM> prove idALT
>>> ?Error: Modification of this statement's proof is discouraged.
>>> You must use PROVE ... / OVERRIDE to work on it.
MM> prove idALT/override
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT idALT"):
101 idALT $p |- ( ph -> ph ) $= ... $.
Note: The proof you are starting with is already complete.
>>> ?Warning: Modification of this statement's proof is discouraged.
MM-PA> minimize_with id
Bytes refer to compressed proof size, steps to uncompressed length.
Proof of "idALT" decreased from 51 to 9 bytes using "id".
MM-PA> save new_proof/compressed
>>> ?Error: Attempt to overwrite a proof whose modification is discouraged.
>>> Use SAVE NEW_PROOF ... / OVERRIDE if you really want to do this.
MM-PA> save new_proof/compressed/override
>>> ?Warning: You are overwriting a proof whose modification is discouraged.
The new proof of "idALT" has been saved internally.
Remember to use WRITE SOURCE to save changes permanently.
MM-PA>
Here is an example of a session trying to use re1tbw2 (ax-1 twin) which
has "(New usage is discouraged.)".
MM> prove r19.12
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT r19.12"):
$d x y $. $d y A $. $d x B $.
7283 r19.12 $p |- ( E. x e. A A. y e. B ph -> A. y e. B E. x e. A ph ) $= ...
$.
Note: The proof you are starting with is already complete.
MM-PA> show new_proof /from 70/to 70
70 ralrimi.2=ax-1 $a |- ( E. x e. A A. y e. B ph -> ( y e. B -> E. x e.
A A. y e. B ph ) )
MM-PA> delete step 70
A 12-step subproof at step 70 was deleted. Steps 70:112 are now 59:101.
59 ralrimi.2=? $? |- ( E. x e. A A. y e. B ph -> ( y e. B -> E. x
e. A A. y e. B ph ) )
MM-PA> assign last re1tbw2
>>> ?Error: Attempt to assign a statement whose usage is discouraged.
>>> Use ASSIGN ... / OVERRIDE if you really want to do this.
MM-PA> assign last re1tbw2/override
>>> ?Warning: You are assigning a statement whose usage is discouraged.
MM-PA> undo
Undid: ASSIGN LAST re1tbw2 / OVERRIDE
59 ralrimi.2=? $? |- ( E. x e. A A. y e. B ph -> ( y e. B -> E. x
e. A A. y e. B ph ) )
MM-PA> improve all
A proof of length 12 was found for step 59.
Steps 59 and above have been renumbered.
CONGRATULATIONS! The proof is complete. Use SAVE NEW_PROOF to save it.
Note: The Proof Assistant does not detect $d violations. After saving
the proof, you should verify it with VERIFY PROOF.
Note that "improve all", which scans backwards, skipped over re1tbw2 and
picked up ax-1:
MM-PA> show new_proof /from 70/to 70
70 ralrimi.2=ax-1 $a |- ( E. x e. A A. y e. B ph -> ( y e. B -> E. x e.
A A. y e. B ph ) )
MM-PA> undo
Undid: IMPROVE ALL
59 ralrimi.2=? $? |- ( E. x e. A A. y e. B ph -> ( y e. B -> E. x
e. A A. y e. B ph ) )
With "/override", it does not skip re1tbw2 but assigns it since it is the
first match encountered (before ax-1 in the backward scan):
MM-PA> improve all/override
>>> ?Warning: Overriding discouraged usage of statement "re1tbw2".
A proof of length 12 was found for step 59.
Steps 59 and above have been renumbered.
CONGRATULATIONS! The proof is complete. Use SAVE NEW_PROOF to save it.
Note: The Proof Assistant does not detect $d violations. After saving
the proof, you should verify it with VERIFY PROOF.
MM-PA>
If you want to see which statements in a specific section have
restrictions, use "search.../comment" e.g.
MM> search ax-1~bitr 'is discouraged'/comment
101 idALT $p "...uted by NM, 5-Aug-1993.) (Proof modification is discouraged.)"
659 dfbi1gb $p "...ry Bush, 10-Mar-2004.) (Proof modification is discouraged.)"
Program note: The new markup tags are looked up via the function
getMarkupFlag() in mmdata.c. Since string searches are slow, the result
of the first search in each statement comment is memoized (saved) so
that subsequent searches can be effectively instant.
Two commands were added primarily for database maintenance:
"show discouraged" will list all of the
statements with "is discouraged" restrictions and their uses in the
database (in case of discouraged usage) or the number of steps (in case
of a proof whose modification is discouraged). It is verbose and
primarily intended to assist a script to compare a modified database
with an earlier version. It will not be of interest to most users.
MM> help show discouraged
Syntax: SHOW DISCOURAGED
This command shows the usage and proof statistics for statements with
"(Proof modification is discouraged.)" and "(New usage is
discouraged.)" markup tags in their description comments. The output
is intended to be used by scripts that compare a modified .mm file
to a previous version.
MM> show discouraged
...
SHOW DISCOURAGED: Proof modification of "tru2OLD" is discouraged (9 steps).
SHOW DISCOURAGED: New usage of "tru2OLD" is discouraged (0 uses).
SHOW DISCOURAGED: New usage of "ee22" is discouraged (2 uses).
SHOW DISCOURAGED: "ee22" is used by "ee21".
SHOW DISCOURAGED: "ee22" is used by "ee33".
...
"set discouragement off" will turn off the blocking of commands caused
to "...is discouraged" markup tags. It does the equivalent of always
specifying "/override" on those commands. It is intended as a
convenience during maintenance of a "discouraged" area of the database
that the user is very familiar with, such as the construction of complex
numbers. It is not recommended for most users.
MM> help set discouragement
Syntax: SET DISCOURAGEMENT OFF or SET DISCOURAGEMENT ON
By default this is set to ON, which means that statements whose
description comments have the markup tags "(New usage is discouraged.)"
or "(Proof modification is discouraged.)" will be blocked from usage
or proof modification. When this setting is OFF, those actions are no
longer blocked. This setting is intended only for the convenience of
advanced users who are intimately familiar with the database, for use
when maintaining "discouraged" statements. SHOW SETTINGS will show you
the current value.
MM> set discouragement off
"(...is discouraged.)" markup tags are no longer honored.
>>> ?Warning: This setting is intended for advanced users only. Please turn
>>> it back ON if you are not intimately familiar with this database.
MM> set discouragement on
"(...is discouraged.)" markup tags are now honored.
(10-Mar-2016) metamath program version 0.125
--------------------------------------------
The following changes were made:
1. A new qualifier, '/fast', was added to 'save proof' and 'show proof'.
See the 9-Mar-2016 entry below for an application.
2. Long formulas are no longer wrapped by 'write source.../rewrap' but
should be wrapped by hand to fit in less than 80 columns. The wrapping
was removed because a human can better judge where to split formulas for
readability. Comments and indentation are still reformatted as before.
3. Added space between adjacent "}" and "{" in the HTML output.
4. A bug in the /explicit/packed proof format was fixed. See 'help save
proof' for a list of all formats.
5. To reference a statement by statement number in 'show statement',
'show proof', etc., prefix the number with "#". For example, 'show
statement #58' will show a1i. This was added to assist program
debugging but may occasionally be useful for other purposes. The
complete list of statement lookup formats in shown in 'help search'.
(9-Mar-2016) Procedure to change a variable name in a theorem
--------------------------------------------------------------
The metamath program has been updated in Version 0.125 (10-Mar-2016)
with a new qualifier, '/fast', that merely changes the proof format
without compressing or uncompressing the proof. This makes format
conversions very fast for making database changes. The format of the
entire database can be changed from /compressed to /explicit/packed, and
vice-versa, in about a minute each way.
The /explicit/packed format is described here:
https://groups.google.com/d/msg/metamath/xCUNA2ttHew/RXSNzdovBAAJ
You can also look at 'help save proof' in the metamath program.
The basic rules we will be using are:
1. When the proofs are saved in explicit format, you can change $f and
$e order.
2. When the proofs are saved in compressed format, you can change the
name of a variable to another if the two variables have adjacent $f's.
======= The conversion procedure: =======
To retrofit the new symbol variables added to set.mm to your theorems,
for example changing "P" to ".+", you can use the following procedure.
First, save all proofs in explict format:
./metamath set.mm
MM> save proof */explicit/packed/fast
MM> write source set.mm
MM> exit
(Hint: 'save proof *' lists all proofs it is saving. To suppress this
output, type "q" at the scrolling question after the first page. It will
not really quit; instead, the proof saving will complete silently.)
Next, edit set.mm to place the $f for the "P" adjacent to (either immediately
before or immediately after) the $f for the ".+". Then resave the proofs
in compressed format:
./metamath set.mm
MM> save proof */compressed/fast
MM> write source set.mm
MM> exit
In your text editor, substitute P for .+ in the theorem you want to
change. Make sure you include the $p and any $d and $e statements
associated with the theorem. If the $d and $e statements affect other
theorems in the same block, you will also have to make the P to .+
substitution in those $p's as well.
You are now done with the change. However, you probably want to restore
the original $f order to make your database compatible with the standard
set.mm. You can postpone doing this until you have finished making all
of your variable name changes as above. First, save all proofs in
explict format:
./metamath set.mm
MM> save proof */explicit/packed/fast
MM> write source set.mm
MM> exit
Next, edit set.mm to restore the original $f order. It may be easiest
just to copy and paste the $f section from the standard set.mm.
Finally, you probably want to save all proofs in compressed format
since the file size will be smaller and easier to work with:
./metamath set.mm
MM> save proof */compressed/fast
MM> write source set.mm
MM> exit
(28-Feb-2015) Stefan O'Rear's notes on recent proofs
----------------------------------------------------
# New definitions
df-har: The Hartogs function, which restricts to cardinal successor on initial
ordinals. Since the latter is somewhat important in higher set theory, I
expect this to get used a bit. One question about the math symbol: standard
notation for ( har ` x ) is \aleph(x), but I didn't want to overlap the math
symbol used for df-aleph, so I left this as Latin text for now.
df-nzr: Nonzero rings: A number of properties of linear independence fail for
the zero ring, so I gave a name to all others.
df-wdom: Weak dominance, i.e. dominance considered using onto functions instead
of 1-1. The starred symbol seems to be relatively standard. I'm quite pleased
with how ~ wdomd turned out.
df-lindf,df-linds: Definition of a linearly independent family resp. set of
vectors in a module. Was initially trying to do this with just one definition
but two seems to work much better with corner cases.
# Highlights
hsmex: The class of sets hereditarily smaller than a given set exists; a
formalization of the proof in
http://math.boisestate.edu/~holmes/holmes/hereditary.pdf . With AC this is
simpler as it follows from the existence of arbitrarily large regular
cardinals. Intermediate steps use Hartogs numbers and onto functions quite
heavily, so df-har and df-wdom were added to support this; it also uses
iterated unions (ituni*) and order types (otos*), but the former is not a
standard concept and the latter has several definitional issues, so both are
temporary definitions for now.
marypha1,marypha2: P. Hall's marriage theorem, a surprisingly annoying
combinatorial result which is in the dependency chain for the vector space
dimension theorem.
kelac2,dfac21i: Recover the axiom of choice from Tychonoff's theorem (which we
don't have yet). Required a number of additional results on box-shaped subsets
of cross products, such as boxriin and boxcuts.
In an attempt to unify the empty and nonempty cases, we are now considering
"relative intersections" of the form ( A i^i |^| B ) and ( A i^i |^|_ x e. I B
), assuming that all elements of B are subsets of A, we get the type-theoretic
behavior that an empty intersection is the domain of discourse of a particular
structure, and not the class _V. Several theorems are added to support this
usage, and the related ( fi ` ( { A } u. B ) ).
lmisfree: There have been a number of recent questions about the correctness of
various definitions of basis. This hopefully helps to clarify the situation by
proving my earlier conjecture that what we have is exactly what is needed to
witness an isomorphism onto a free module. Notable intermediate steps here are
islbs (splits our notion of basis into the spanning and independence parts),
islindf4 ("no nontrivial representations of zero"), and lbslcic (only the
cardinality of the index set matters).
Along the way this required separating independent sets and families from the
previous notion of bases; a new "independent sets and families" section
contains the basic properties there.
domunfican: A cancellation law for cardinal arithmetic which came up in
marypha1 but may be of independent interest.
# Possible future directions
Probably a lot of polynomial stuff soon, with maybe a vector space dimension
theorem thrown in for good measure. A rough priority order, and less final the
farther you go:
1. Fraction ring/field development; rational function fields
2. Recursive decomposition of polynomials
3. AA = ( CCfld IntgRing QQ) and re-re-define _ZZ = ( CCfld IntgRing ZZ ) $.
4. Relating integral elements to finitely generated modules.
5. Hilbert basis theorem
6. Integral closures are rings; aaaddcl/aamulcl.
7. Cowen-Engeler lemma (Schechter UF2); finite choice principles from
ultrafilters
8. M. Hall's marriage theorem
9. The next natural property of independent sets: the exchange theorem and the
finite dimension theorem for vector spaces
10. General dimension theorem from ultrafilters
11. Gauss' lemma on polynomials; ZZ = ( _ZZ i^i QQ )
12. Polynomial rings are UFDs
(17-Feb-2015) Mario Carneiro's notes on recent proofs
-----------------------------------------------------
Notes:
ifbothda: Common argumentation style for dealing with if, may be good
to know
disjen, disjenex: When constructing the reals, we needed extra elements
not in CC for +oo and -oo, and for that purpose we used ~P U. CC, ~P ~P
U. CC. This works great if you only want a few new elements, but for
arbitrarily many elements this approach doesn't work. So this theorem
generalizes this sort of construction to show that you can build an
arbitrarily large class of sets disjoint from a given base class A.
domss2, domssex2, domssex: One application of disjen is that you can
turn any injection F : A -1-1-> B around into G : B -1-1-onto-> C
where A C_ C, and which is the identity on elements of A. I'm thinking
about taking advantage of this in the field extensions for Cp, since
this way you don't need a canonical injection into the extension but can
actually build the extension around the original field so that it is
literally a subfield of the extension. It could also be used, if
desired, as a means of building compatible extensions in the
construction of the reals (so that om = NN0).
ghmker: the kernel of a group homomorphism is a normal subgroup
crngpropd, subrgpropd, lmodpropd, lsspropd, lsppropd, assapropd:
property theorems
tgcnp, tgcn, subbascn: checking continuity on a subbase or basis for a
topology
ptval: Product topology. Important theorems are pttop, ptuni, ptbasfi,
ptpjcn, ptcnp, ptcn.
pt1hmeo, ptunhmeo: combining these judiciously allows you to show that
indexed product topologies are homeomorphic to iterated binary product
topologies, which for example can be used to prove ptcmpfi, which is
basically Tychonoff for finite index sets.
metdsval, metds0, metdseq0, metdscn: Properties of the function d(x,A)
which gives the distance from a point to a nonempty set.
lebnum, lebnumii: The Lebesgue number lemma, a nice result about open
covers in a metric space and a key step in the proof of the covering map
lifting theorem.
df-pi1: Converted to structure builders, eliminated df-pi1b
pcopt2, pcorev2: commuted versions of pcopt, pcorev. Took me a while
to realize that left identity -> right identity and left inverse ->
right inverse does not actually follow from the other proofs, since at
this level we have only a groupoid, not a group.
pi1xfr: A path induces a group isomorphism on fundamental groups.
df-dv: Added a second argument to _D for the ambient space. There is a
drop-in replacement from ( _D ` F ) to ( RR _D F ), and ( CC _D F ) is
the complex derivative of F. The left argument can be any subset of CC,
but since the derivative is not a function if S has isolated points, I
restrict this to S e. { RR , CC } for the primary convenience theorems.
df-lgs: The Legendre symbol, a tour-de-force of something interesting
coming out of a ridiculous amount of case analysis. This definition is
actually the Kronecker symbol, which extends the Jacobi symbol which
extends the Legendre symbol to all integers. The main theorem to be
done in this area is of course the law of quadratic reciprocity, but
currently I'm stuck proving Euler's criterion which is waiting on
polynomials over Z/pZ. So far the basic theorems prove that ( A /L N )
e. {-1,0,1}, ( A /L N ) =/= 0 iff A,N are coprime, and it is
distributive under multiplication in both arguments.
kur14: The Kuratowski closure-complement theorem, which I mentioned in
another email.
df-pcon, df-scon: Path connected spaces and simply connected spaces. I
hope to use SCon to prove some kind of Cauchy integral theorem, but
we'll see.
txpcon, ptpcon: products of path-connected spaces are path-connected
(ptpcon is actually an AC-equivalent)
pconpi1: The fundamental groups of a path-connected space are
isomorphic
sconpi1: A space is simply connected iff its fundamental group is
trivial
cvxpcon, cvxscon: a convex subset of CC is simply connected blcvx,
blscon: a disk in CC is convex and simply connected
df-cvm: Definition of a covering map.
cvmlift: The Path Lifting Theorem for covering maps
df-rpm, df-ufd: define a prime element of a ring and a UFD
psr1val: Basic theorems for univariate polynomials
(9-Jan-2015) mpbi*an* hypothesis order change
---------------------------------------------
At the suggestion of a couple of people, I changed the hypothesis order
in mpbi*an* (7 theorems) so that the major hypothesis now occurs last
instead of first, in order to make them less annoying to use. The
theorems changed were:
mpbiran mpbiran2 mpbir2an mpbi2and mpbir2and mpbir3an mpbir3and
This change affects over 1000 proofs. The old versions are still there
suffixed with "OLD" and will remain for 1 year.
To update your mathbox etc.,
1. Make sure your mathbox is compatible with the the set.mm just prior
to this change, temporarily available here:
http://us2.metamath.org:88/metamath/set.mm.2015-01-08.bz2
1. In a text editor, suffix all references to mpbi*an* in your proofs
with OLD (e.g. mpbiran to mpbiranOLD). This will make your proofs
compatible with the current set.mm.
2. Update the current set.mm with your mathbox.
3. For each proof using mpbi*an*OLD, do the following in the metamath
program:
./metamath set.mm
...
MM> prove abc
MM-PA> minimize mpbi*an*/except *OLD/allow_growth
MM-PA> save new_proof/compressed
MM-PA> exit
..,
MM> write source set.mm
MM> exit
(11-Jun-2014) Mario Carneiro's revisions
----------------------------------------
Mario Carneiro finished a major revision of set.mm. Here are his notes:
syl3anbrc, mpbir3and: simple logic stuff
fvunsn: eliminate D e. _V hypothesis
caoprcld, caoprassg, caoprcomg: deduction form
winafpi: dedth demonstration
avglt1, avglt2, avgle1, avgle2: average ordering theorem colleciton
peano2fzr: recurring lemma
fzfid: very common use due to deduction-form sum theorems
seqcl2 thru seq1p: deduction form
sercaopr2: the 'correct' general form of sercaopr
seqz: absorbing element in a sequence (note that there are now theorems
seq1 and seqz, since the old tokens are gone)
cseq1 thru ser1add, seq1shftid, seqzm1 thru ser0p1i: deleted - all the
theorems in this section have equivalents in the new seq section,
although it is often a 4-5 to 1 mapping, since the deduction framework
makes it easier to have ease of use and full generality at the same time
df-exp: revised to include negative integer exponents. The theorems for
nonnegative exponents are exactly the same as before, but for negative
exponents ( A ^ -u N ) we need the assumption A=/=0 so that we don't
divide by zero. Relevant new theorems are:
expneg, expneg2, expnegz, expn1: definition of ( A ^ -u N ) is 1 / ( A
^ N )
expcl2lem: closure under positive and negative exponents
rpexpcl: the only existing closure theorem that was changed as a result
reexpclz, expclz: closure for reals and complexes to integer exponents,
when the argument is nonzero
1exp, expne0i, expgt0, expm1, expsub, expordi thru expword2i:
generalized to negative exponents
mulexpz, expaddz: the main "hard" theorems in this section, generalizing
the exponent addition laws to integers. The main reason to keep both the
new versions and the old (mulexp, expadd) is because the new theorems
generalize the exponent at the cost of the extra hypothesis A =/= 0.
discr, discr1: deduction form, generalized to all A e. RR, shortened proof
rexanuz: the new upper integer form of cvganz, and used as the basis for
most other manipulations on upper integer sets to replace cau* and cvg*
theorems
rexfiuz: finite set generalization of rexanuz