forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmmdeduction.raw.html
1088 lines (897 loc) · 45 KB
/
mmdeduction.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=UTF-8">
<TITLE>The Weak Deduction Theorem - Metamath Proof Explorer</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<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="mmset.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Proof Explorer Home"
TITLE="Metamath Proof Explorer 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</B></FONT><BR>
<FONT SIZE="+2" COLOR="#006633"><B>The Weak Deduction Theorem</B>
</FONT>
</TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP>
</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> >
<A HREF="mmset.html">MPE Home</A> >
The Weak Deduction Theorem
</FONT>
</TD>
</TR>
</TABLE>
<HR NOSHADE SIZE=1>
<TABLE WIDTH="100%" BORDER=0><TR><TD WIDTH="50%">
<B><FONT COLOR="#006633">Contents of this page</FONT></B>
<MENU>
<LI> <A HREF="#quick">A Quick Hint</A></LI>
<LI> <A HREF="#dedvsth">Deductions vs. Theorems</A></LI>
<LI> <A HREF="#convert">Converting Deductions to Theorems</A></LI>
<LI> <A HREF="#standard">The Standard Deduction Theorem</A></LI>
<LI> <A HREF="#weak">Weak Deduction Theorem</A></LI>
<LI> <A HREF="#meta">Logic,
Metalogic, and Metametalogic</A>
<!-- -->
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>New</FONT> <FONT
SIZE=-1><I>2-Dec-2008</I></FONT>
<!-- -->
</LI>
<LI> <A HREF="#prop">The Weak Deduction Theorem in Propositional Calculus</A></LI>
<LI> <A HREF="#propex">Propositional Calculus Example</A></LI>
<LI> <A HREF="#set">The Weak Deduction Theorem in Set Theory</A></LI>
<LI> <A HREF="#setex">Set Theory Example</A></LI>
<LI> <A HREF="#proof">Informal Proof of the Weak Deduction Theorem</A></LI>
<LI> <A HREF="#special">Another Special Case of the Deduction Theorem</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>New</FONT> <FONT
SIZE=-1><I>2-Mar-2008</I></FONT>
-->
</LI>
</MENU>
</TD><TD WIDTH="10%"></TD><TD ALIGN=right>
<FONT COLOR="#006633"><I>
A Theorem fine is Deduction,<BR>
For it allows work-reduction:<BR>
To show "A implies B",<BR>
Assume A and prove B;<BR>
Quite often a simpler production.<BR>
</I><BR>
--Stefan Bilaniuk<BR>
<A HREF="http://euclid.trentu.ca/math/sb/pcml/welcome.html"
><I>A Problem Course in Mathematical Logic</I>, 2003</A> [external]
</FONT>
</TD></TR></TABLE>
<P><HR NOSHADE SIZE=1><A NAME="quick"></A><B><FONT COLOR="#006633">A Quick
Hint</FONT></B> If you came to this page because you
found a proof referencing the Weak Deduction Theorem <A
HREF="dedth.html">dedth</A> (or one of its variants dedth<I>xx</I>),
here is how to follow the proof without getting into the details
described on this page: just
click on the theorem referenced in the step
just before the reference to <A HREF="dedth.html">dedth</A>
and ignore everything else. All that <A HREF="dedth.html">dedth</A>
does is turn a
hypothesis into an antecedent (i.e. the hypothesis followed by ` -> ` is placed in
front of the assertion, and the hypothesis itself is eliminated).
<B>Example:</B> Look at the proof of
<A HREF="renegcl.html">renegcl</A>. In step 5, there is a reference
to the deduction <A HREF="renegcli.html">renegcli</A>,
"` |- A e. RR ` ` => `
` |- -u A e. RR `". A special substitution instance of
<A HREF="renegcli.html">renegcli</A>
is used to feed the last hypothesis of
the deduction theorem <A HREF="dedth.html">dedth</A>, which in turn
converts it to the theorem
"` |- ( A e. `
` RR -> -u A e. RR ) `" in step 6. The somewhat
strange-looking steps before step 5 are just some technical stuff that
makes this magic work, and they can be ignored for a quick
overview of the proof. To continue following the "important" part of
the proof, click on the reference to <A HREF="renegcli.html">renegcli</A> at
step 5.
<P>On this page we attempt to show you how this technical stuff works if you
are interested. We also discuss the
<A HREF="#set">conditional operator</A>
"` if ( ph , A , B ) `" that you
will find in these proofs.
<P>
In many situations today MPE no longer uses the approach described here.
We instead tend to use
<A HREF="mmnatded.html">deduction form and natural deduction</A>.
However, the approach described here is still valid, and it may be
interesting to you.
<!--
<P>Why does Metamath need these complicated-looking steps to convert an
inference (deduction) into a closed theorem, when other systems of logic
typically have a (metalogical) rule that allows you to do it in one
step? The answer is that these steps are part of the price for
Metamath's philosophical goal to show all proofs <I>directly</I> from
the axiom system in its database and not have to rely on higher-level
metatheorems derived outside of that axiom system. From a practical
point of view, this minimalist philosophy also makes automated proof
verification extremely simple: the only metalogical rule needed to
construct a proof from the axioms is the substitution of an expression
for a variable.
-->
<P><HR NOSHADE SIZE=1><A NAME="dedvsth"></A><B><FONT
COLOR="#006633">Deductions vs. Theorems</FONT></B> A
<B>deduction</B> (also called an <B>inference</B>) is a kind of
statement that needs some hypotheses to be true in order for its
conclusion to be true. A <B>theorem</B>, on the other hand, has no
hypotheses. (Informally we may call both of them theorems, but on this
page we will stick to the strict definition.) An example of a
deduction is the contraposition inference:
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><A HREF="con3i.html">con3i</A></TD><TD>` |- ( ph -> ps ) ` ` => `
` |- ( -. ps `
` -> -. ph ) ` </TD></TR>
</TABLE></CENTER>
<P>This means that if we have proved a theorem of the form
` |- ( ph -> ps ) `
(where
` ph `
and
` ps `
are any wffs), then
we can conclude the theorem
` |- ( -. ps `
` -> -. ph ) ` .
Here, the symbol
"` |- `"
is just a place-holder that can be read
as "a proof exists for". The big arrow connecting the hypothesis and
conclusion isn't a formal mathematical symbol; I put it there
to suggest informally the relationship between hypothesis and conclusion.
To gain an informal feel for what the contraposition inference says,
suppose we agree with the English statement, "If it is raining, there are clouds
in the sky." From contraposition we can conclude,
"If there are no clouds in the sky, it is not raining."
<P>An example of a theorem is the law of contraposition:
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><A HREF="con3th.html">con3th</A></TD><TD>
` |- ( ( ph -> ps ) -> `
` ( -. ps -> `
` -. ph ) ) ` </TD></TR>
</TABLE></CENTER>
<P>This looks almost the same as the deduction, except the hypothesis
and conclusion are connected together with the formal mathematical
symbol for "implies". We don't have to prove a hypothesis;
instead it is a stand-alone statement that is unconditionally true.
Even though it looks similar, it is "stronger" than the
deduction in a fundamental way.
<P><HR NOSHADE SIZE=1><A NAME="convert"></A><B><FONT
COLOR="#006633">Converting Deductions to Theorems</FONT></B>
It sometimes happens that we have proved a deduction
of the form
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD>` |- si ` ` => ` ` |- ta ` </TD></TR>
</TABLE></CENTER>
<P>and we want to then prove a theorem of the form
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD> ` |- ( si -> ta ) ` </TD></TR>
</TABLE></CENTER>
<P>Doing this is not as simple as you might think. The deduction says,
"if we can prove
` si `
then we can prove
` ta ` ,"
which is in some
sense weaker<FONT SIZE=-1>*</FONT> than saying
"` si `
implies
` ta ` ."
Now, there is no axiom of logic that
permits us to directly obtain the theorem given the deduction.
However, it is possible to make use of information contained in the
deduction or its proof to assist us with the proof of the theorem, and
this is what the standard deduction (meta)theorem and a related version that
we use are all about.
<P>On the other hand, if we have the theorem, it is easy to recover the
deduction using modus ponens <A HREF="ax-mp.html">ax-mp</A>. An example
of this is the derivation of the inference <A HREF="simpli.html">simpli</A>
from the theorem <A HREF="simpl.html">simpl</A>.
<P><FONT SIZE=-1>*For example, the
conversion of a deduction to its theorem form does not hold in general
for <A HREF="../qlegif/mmql.html#prop">quantum propositional calculus</A>,
which is a weak subset of classical propositional calculus.
In fact, it has been shown that adding the Standard Deduction Theorem
(below) to quantum propositional calculus turns it into classical
propositional calculus!</FONT>
<P><HR NOSHADE SIZE=1><A NAME="standard"></A><B><FONT
COLOR="#006633">The Standard Deduction Theorem</FONT></B>
In traditional logic books, there is a metatheorem
called the <B>Standard Deduction Theorem</B> (discovered independently
by Herbrand and Tarski around 1930; I added "Standard" to distinguish it
from our "Weak" version below) that provides an algorithm for
constructing a proof of a theorem from the proof of its corresponding
deduction. See, for example, Margaris, <I>First Order Mathematical
Logic,</I> p. 56. To construct a proof for a theorem, the algorithm
looks at each step in the proof of the original deduction and rewrites
the step with several steps wherein the hypothesis is eliminated and
becomes an antecedent.
<P>In ordinary mathematics, no one actually carries out the algorithm,
because (in its most basic form) it involves an exponential explosion of
the number of proof steps as more hypotheses are eliminated. Instead,
the Standard Deduction Theorem is invoked simply to claim that it can be
done in principle, without actually doing it.
<!--
<P>On these Metamath web pages, we want to show you actual proofs rather
than just telling you that a proof is possible. It is kind of like the
difference between saying, "according to advanced number theory,
this large integer is composite", versus "here are the factors
of this large integer." Only a few people could verify the former,
whereas almost anyone could verify the latter, even though they are both
valid ways of proving that an integer is composite.
The use of a high-level metatheorem such as the Standard Deduction
Theorem in our proofs would require you to learn metamathematical
concepts beyond the simple substitution of expressions for variables, in
order to verify for yourself that they are rigorously correct.
-->
<P><A NAME="bad"></A>Actually, the Standard Deduction Theorem is not
quite as simple as it might first appear. There is a subtle restriction
that must be taken into account when working with predicate calculus.
If the Axiom of Generalization <A HREF="ax-gen.html">ax-gen</A> was used
in the proof of the original deduction (or anywhere in the potentially
large tree of lemmas building up to it) to quantify over a free variable
contained in one of its hypotheses, then converting that hypothesis to
an antecedent may fail.
The following example shows why. When ` x ` and ` y ` are distinct variables, the following
(silly) deduction can be <A HREF="dtrucor.html">proved</A> in set theory:
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD>` |- x `
` = `
` y ` ` => `
` |- x `
` =/= `
` y ` </TD></TR>
</TABLE></CENTER>
<P>The reason this deduction holds is that the hypothesis, which
effectively states (using <A HREF="ax-gen.html">ax-gen</A>) "for all
` x ` and ` y ` , ` x = y ` is true," can never be proved as a stand-alone theorem. In
fact it is provably false (by <A HREF="dtru.html">dtru</A>), so any
conclusion whatsoever follows from it. However, if we naively apply the
Standard Deduction Theorem and blindly convert the hypothesis to an
antecedent, the theorem form of this deduction:
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><B><I>Wrong!</I></B>
` |- ( x `
` = `
` y -> `
` x `
` =/= `
` y ) `
</TD></TR>
</TABLE></CENTER>
<P>("if two things are equal
then they are not equal") is obviously
<A HREF="dtrucor2.html">absurd</A>!
<P><I>Note.</I> The way we have presented the Standard Deduction
Theorem above is slightly different from that in most textbooks, which
use a list of hypotheses to the left of the the turnstile symbol ` |- ` . This is
discussed further in the <A HREF="#meta">Logic, Metalogic,..."</A>
section below.
<P><HR NOSHADE SIZE=1><A NAME="weak"></A><B><FONT COLOR="#006633">Weak
Deduction Theorem</FONT></B>
One of the goals of Metamath is to let you plainly see, with as few
underlying concepts as possible, how mathematics can be derived
<I>directly</I> from the axioms, and not indirectly according to some
hidden rules buried inside a program or understood only by logicians.
If we added the Standard Deduction Theorem to the language and proof
verifier, that would greatly complicate both and largely defeat
Metamath's goal of simplicity.
<!--
In addition, Metamath is intended in principle to be independent of any
particular system of logic, including quantum logic where
the Standard Deduction Theorem fails. If the Standard Deduction
Theorem were built in as a high-level rule, it would defeat this
purpose. -->
In principle, we could show direct proofs by expanding out the proof
steps generated by the algorithm of the Standard Deduction Theorem, but
it is not feasible in practice because the number of proof steps quickly
becomes huge, even astronomical. Since the algorithm is driven by proof
of the deduction, we would have to go through that proof all over
again—starting from axioms—in order to obtain the theorem
form. In terms of proof length, there would be no savings over just
proving the theorem directly instead of first proving the deduction
form.
<P>There is a much more efficient method for proving a theorem from a
deduction that can be used in many (but not all) cases. We call it the
<B>Weak Deduction Theorem</B>. (There is also an unrelated "Weak
Deduction Theorem" in the field of relevance logic, so to avoid
confusion we could call ours the "Weak Deduction Theorem for Classical
Logic.") Unlike the Standard Deduction Theorem, the Weak Deduction
Theorem produces the theorem directly from a special substitution
instance of the deduction, using a small, fixed number of steps roughly
proportional to the length of the final theorem. The number of
additional steps is completely independent of the size of the original
proof, so in practice it can be applied to very advanced theorems
without a corresponding increase in proof size. There are also no
restrictions on the use of the Axiom of Generalization that may cause us
to stumble: how the original deduction was proved is irrelevant.
<P>The Weak Deduction Theorem is used frequently in the Metamath Proof
Explorer, especially in set theory, in order to make formal proofs more
compact. Here we describe it in some detail since it is not necessarily
intuitive, nor has it ever been published.
<P>What are its limitations? Specifically, we must be able to prove a
special case of the deduction's hypothesis as a stand-alone theorem.
This means it cannot be used in all cases—for example, it cannot be
used when the hypothesis is a contradiction such as ` ( ph /\ -. ph ) ` .
However, in the case of the contraposition deduction above, by
substituting ` ph ` for ` ps ` in the hypothesis ` |- ( ph `
` -> ps ) ` , we obtain the trivially proved
identity theorem <A HREF="id.html">id</A>, ` |- ( ph -> ph ) ` . This
special case can be used (together with some auxilliary lemmas) to
eliminate the hypothesis and introduce it as an antecedent.
<P>Does this limitation cause us inconvenience? In Metamath's set
theory development, a modified version for class variables (see the <A
HREF="#set">set theory version</A> below) is used extensively. For most
practical deductions we can almost always display an easy-to-prove
special case of a hypothesis, since otherwise the deduction tends not to
be of much use. For example, if the hypothesis requires a class
variable to be a nonzero real number, the special case of the number 1
will satisfy the hypothesis.
<P>An exception is a deduction for which we can never display an actual
example satisfying its hypothesis but can show only the existence of a
set satisfying it. Theorems involving the <A HREF="ac5.html">Axiom of
Choice</A> are sometimes like this. In such a case, the Weak Deduction
Theorem cannot be used. Therefore we must settle for a longer direct
proof of the theorem form, but so far I haven't encountered a case where
this has been impractical.
<P>Is this to say that the Standard Deduction Theorem is of little use?
Definitely not! When outlining proofs prior to entering and verifying
them with the Metamath program, I informally use the Standard Deduction
Theorem implicitly and extensively just like any mathematician would.
When satisfied with the informal outline, I then work out the details
necessary to create a (hopefully short) formal proof either directly or
with the help of the Weak Deduction Theorem.
<!-- The nitpicking and
absolutely rigorous formal proofs of Metamath are often quite different
from the informal high-level reasoning that mathematicians use in
practice. High-level informal reasoning is essential for achieving
practical results in mathematics, but it is also dangerously subject to
the possibility of an error for those who are inexperienced, and the
complete elimination of this possibility is part of what Metamath is
about. -->
<P>By the way, the Standard and Weak Deduction Theorems are not
"theorems" in the sense described in the "Deductions vs. Theorems"
section above but are "metatheorems" (or more precisely
"metametatheorems," since all Metamath theorems are actually theorem
schemes) whose proofs require metamathematics outside of the axiom
system. Specifically, they are both algorithms for generating actual
proofs. However, once the Weak Deduction Theorem generates a proof,
questions about the justification and rigor of its metamathematics
become irrelevant, because the proof it produces is independently
verified by the Metamath proof verifier. Where a proof came from,
whether written by a human or generated by some algorithm, is of no
importance to the verifier. The same cannot be said about the Standard
Deduction Theorem in the way it is normally used, since it does not
produce a practical proof that can be verified directly but only shows
that a proof is possible in principle.
<P><HR NOSHADE SIZE=1><A NAME="meta"></A><B><FONT COLOR="#006633">Logic,
Metalogic, and Metametalogic</FONT></B>
In logic textbooks, the treatment of the Standard Deduction Theorem is
slightly different from how we presented it above. They typically
show deductions in the following way: the set of hypotheses is shown
to the left of the turnstile ` |- ` , and the conclusion from them to the right. For
example, the deduction <A HREF="con3i.html">con3i</A> in <A
HREF="#dedvsth">Deductions vs. Theorems</A> would be represented as
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><A HREF="con3i.html">con3i</A></TD><TD>` { ( ph -> ps ) } `
` |- ( -. ps -> -. ph ) ` </TD></TR>
</TABLE></CENTER>
<P>In order to talk conveniently about deductions in general, the set of
hypotheses may represented by a metavariable such as ` _G ` that
ranges over sets of wffs, with a conclusion represented by a
metavariable such as ` ta ` ranging over wffs:
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD>` _G `
` |- ta ` </TD></TR>
</TABLE></CENTER>
<P> For example, Theorem 7 in [<A
HREF="mmset.html#Margaris">Margaris</A>] p. 76 states (using our
notation),
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD>If ` _G |- ta ` ,
then ` _G `
` |- A. x ta ` , provided that ` x ` is not free in ` _G ` .</TD></TR>
</TABLE></CENTER>
<P>There are actually three kinds of implications in this statement.
First we have any implication arrow ` -> ` (not shown) that might be present in the wff
represented by ` ta ` . At the next higher level, we have the connection between
` _G `
and ` ta ` that is
represented by the turnstile ` |- ` . Finally at the top-most level, we have the
connection between the two deductions of the theorem, represented by the
English phrase "If...then". We might think of these three as belonging
to the logic, the metalogic, and the metametalogic respectively.
<!-- (If we
want to have fun with words, in Metamath an implication arrow ` -> ` is actually part
of a <A HREF="mmset.html#schemes">scheme</A> and thus at the level of
metalogic. So the two higher levels are really metametalogic and
metametametalogic!)
-->
<P>The expression between the "if" and "then" above is usually called a
"premise" rather then a "hypothesis". The Standard Deduction Theorem
does not provide for the elimination of premises, only of hypotheses.
Viewed in this way, there is actually a fundamental difference between
the Standard Deduction Theorem and the Weak Deduction Theorem: the
former applies to hypotheses, and the latter applies to premises. In
other words, they apply to different "meta" levels.
<P>The set.mm database doesn't have a way of representing deductions in
the way we have just described. However, the "natural deduction"
database <A
HREF="http://wiki.planetmath.org/cgi-bin/wiki.pl/Natural_deduction_based_metamath_system">nat.mm</A>
[external], developed by Frédéric Liné, shows how
this can be done in the Metamath language. Under such a system,
Margaris's theorem would be represented in the database with a
premise ($e statement) for the expression "` _G |- ta `" and with a
provable conclusion ($p statement) for the expression "` _G |- A. x ta `".
<!--
<P>Looking at it this way, the Weak Deduction Theorem is actually quite
different in nature from the Standard Deduction Theorem. It converts a
hypothesis at the metametalogic level to an antecedent at the logic
level, skipping the metalogic level entirely.
-->
<!-- Indeed, there is an
important intrinsic difference that can be seen immediately: the
hypotheses for the Weak Deduction Theorem are asserted to be provable
statements (due to their turnstiles), whereas the hypotheses of the
Standard Deduction Theorem do not have to be provable. -->
<P><HR NOSHADE SIZE=1><A NAME="prop"></A><B><FONT COLOR="#006633">The Weak
Deduction Theorem in Propositional Calculus</FONT></B>
<I>Suggestion:</I> This section describes the technical details of our
Weak Deduction Theorem and is unfortunately quite complex. If you want
to understand how it works, you will be less confused if you first
carefully study the <A HREF="#proof">informal proof</A> below. Then you
may want to take a quick look at the <A HREF="#propex">propositional
calculus example</A> in the next section before continuing with this
section, in order to see a concrete example that achieves our goal.
<P><I>Another suggestion:</I> If you are familiar with a little set
theory, you may want to skip ahead directly to the <A HREF="#set">Weak
Deduction Theorem in set theory</A>, which may be easier to understand.
We never use the Weak Deduction Theorem in propositional calculus except
in the contrived example <A HREF="con3th.html">con3th</A> created for
the next section.
<P>The auxilliary lemmas we need for the Weak Deduction Theorem in
propositional calculus are <A HREF="elimh.html">elimh</A> and <A
HREF="dedt.html">dedt</A>. The first takes the special case (such as <A
HREF="id.html">id</A> above) as its third hypothesis and builds a
strange-looking theorem from it. This strange-looking theorem is a
substitution instance of the hypothesis we want to convert to an
antecedent. We then apply the strange-looking theorem to the hypothesis
of the deduction, resulting in a (still strange-looking) substitution
instance of its conclusion. Finally, we take this result and apply it
to the second hypothesis of <A HREF="dedt.html">dedt</A>, and magically
the desired theorem pops out as the conclusion of <A
HREF="dedt.html">dedt</A>, with the original hypothesis transformed into
an antecedent. Below we show these auxilliary lemmas.
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"> <CAPTION><B>Auxilliary
lemmas for the Weak Deduction Theorem</B></CAPTION>
<TR ALIGN=LEFT><TD><A HREF="elimh.html">elimh</A></TD><TD>` |- ( ( ph <-> ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) ) -> ( ch <-> ta ) ) ` ` & ` ` |- ( ( ps <-> ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) ) -> ( th <-> ta ) ) ` ` & ` ` |- th ` ` => `
` |- ta ` </TD></TR>
<TR ALIGN=LEFT><TD><A HREF="dedt.html">dedt</A></TD><TD>` |- ( ( ph <-> ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) ) -> ( th <-> ta ) ) ` ` & ` ` |- ta `
` => `
` |- ( ch -> `
` th ) ` </TD></TR>
</TABLE></CENTER>
<P>In lemma <A HREF="elimh.html">elimh</A>, the wff
` ch `
is the hypothesis of the original deduction. The wff
` th `
is the special case
(such as <A HREF="id.html">id</A> in our example above) of
that hypothesis.
` ph `
is the wff variable of the deduction's hypothesis that is replaced
with wff variable
` ps `
to result in the special case.
The first two
hypotheses of <A HREF="elimh.html">elimh</A> are trivially-proved
technical hypotheses
that specify the substitution
instances we need. The first one tells <A HREF="elimh.html">elimh</A>
that when the wff
` ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) `
is substituted for the wff variable
` ph `
in wff
` ch `
(the hypothesis of the original deduction), the result is wff
` ta ` .
The "substitution" of
` ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) `
for
` ps `
(in wff
` th `
to result in wff
` ta `)
specified by the
second hypothesis of <A HREF="elimh.html">elimh</A>
is special—not
all occurrences of wff variable
` ps `
are replaced, but only the ones at the
variable positions replaced in the first <A HREF="elimh.html">elimh</A>
hypothesis (step 6 of
the example in the next section will help clarify this).
<P>The conclusion of <A HREF="elimh.html">elimh</A> is applied to the
hypothesis of a matching substitution instance of
the original deduction, which in turn produces as its conclusion a
wff that is applied to the second hypothesis of lemma <A
HREF="dedt.html">dedt</A>.
<P>In lemma <A HREF="dedt.html">dedt</A>, the wff
` ch `
is the hypothesis of the original deduction, and the
wff
` th ` is the conclusion
of the original deduction.
The first hypothesis of <A HREF="dedt.html">dedt</A>
tells it that when the wff
` ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) `
is substituted for the wff variable
` ph `
in wff
` th ` , the result is
wff
` ta ` .
The conclusion of <A HREF="dedt.html">dedt</A>, the wff
` ( ch -> `
` th ) ` ,
is the desired theorem.
<P>It may be hard to understand intuitively how the Weak Deduction
Theorem works just by looking at <A HREF="elimh.html">elimh</A> and <A
HREF="dedt.html">dedt</A>. In a later section, we give a <A
HREF="#proof">proof</A> that presents the algorithm in detail and should
be easier to understand. Our two
lemmas just encapsulate the algorithm into a form convenient to
use.
<P><HR NOSHADE SIZE=1><A NAME="propex"></A><B><FONT
COLOR="#006633">A Propositional Calculus Example</FONT></B>
Let's examine the application of these lemmas in the
contraposition theorem <A HREF="con3th.html">con3th</A> (look at its
proof). Step 7 applies the special case <A HREF="id.html">id</A> to the
third hypothesis of <A HREF="elimh.html">elimh</A>, resulting in step 8.
Step 8 is applied to the hypothesis of the contraposition deduction <A
HREF="con3i.html">con3i</A> to result in step 9. Finally, step 9 is
applied to the second hypothesis of <A HREF="dedt.html">dedt</A>,
resulting in the contraposition theorem.
<P>Steps 1 through 6 of <A HREF="con3th.html">con3th</A> build the
technical substitution instances that we need. In general these
substitution instances are quite easy to prove by repeatedly applying
"formula-builder" lemmas such as <A HREF="negbid.html">negbid</A> and <A
HREF="imbi1d.html">imbi1d</A>. Note that we use the term "substitution"
in a nonstandard way in the description of step 6 below, since not all
occurrences of the thing being substituted for are replaced.
<P>Step 4
proves that the substitution of
` ( ( ps /\ ( ph -> ps ) ) \/ ( ph /\ -. ( ph `
` -> ps ) ) ) `
for
` ps `
in the contraposition hypothesis wff
` ( ph -> ps ) `
results in
` ( ph -> ( ( ps /\ ( ph `
` -> ps ) ) \/ ( ph /\ -. ( ph -> ps ) ) ) ) ` .
This is assigned to the first hypothesis of
<A HREF="elimh.html">elimh</A>.
<P>Step 6
proves that the substitution of
` ( ( ps /\ ( ph -> ps ) ) \/ ( ph /\ -. ( ph `
` -> ps ) ) ) `
for the <I>only the second</I>
` ph `
in the special case wff
` ( ph -> ph ) `
results in
` ( ph -> ( ( ps /\ ( ph `
` -> ps ) ) \/ ( ph /\ -. ( ph -> ps ) ) ) ) ` .
Unlike a "normal" substitution, we replaced only the second one because
that was the position where the substitution took place in step 4. This
is assigned to the second hypothesis of <A HREF="elimh.html">elimh</A>.
<P>Step 3
proves that the substitution of
` ( ( ps /\ ( ph -> ps ) ) \/ ( ph /\ -. ( ph `
` -> ps ) ) ) `
for
` ps `
in the contraposition conclusion wff
` ( -. ps -> -. ph ) `
results in
` ( -. ( ( ps /\ ( ph -> ps ) ) \/ ( ph /\ -. ( ph `
` -> ps ) ) ) -> -. ph ) ` .
This is assigned to the first hypothesis of
<A HREF="dedt.html">dedt</A>.
<P>In practice, the Weak Deduction Theorem isn't used very often in our
propositional calculus development because direct proofs that build on a
previously proved hierarchy of theorems are usually more efficient. In
fact, our proof of the contraposition theorem <A
HREF="con3th.html">con3th</A> was contrived just for the purpose of this
example. Compare the more efficient direct proof of the same theorem
in <A HREF="con3.html">con3</A>.
<P><HR NOSHADE SIZE=1><A NAME="set"></A><B><FONT COLOR="#006633">The Weak
Deduction Theorem in Set Theory</FONT></B> <P>Where the
Weak Deduction Theorem becomes very useful, if not essential, is in set
theory. For set theory, special versions of <A
HREF="elimh.html">elimh</A> and <A HREF="dedt.html">dedt</A>, called <A
HREF="elimhyp.html">elimhyp</A> and <A HREF="dedth.html">dedth</A>
respectively, work with substitutions into classes
instead of wffs.
<P>To make things more efficient, we introduce a special notation
called the "conditional operator,"
"` if ( ph , A , B ) ` ,"
which combines a wff and two classes to produce another class.
See definition <A HREF="df-if.html">df-if</A>.
Read "` if ( ph , A , B ) `" as "if
` ph `
is true then
the value is ` A ` else
the value is ` B ` ."
It is
just an abbreviation for a more complicated class expression like other
such abbreviations (class union, etc.). This abbreviation makes working
with the Weak Deduction Theorem a little easier, and like all
definitions, in principle it can be eliminated by expanding out the
abbreviation at each occurrence in a proof. (It also has many other
applications in addition to its use with the Weak Deduction Theorem.)
<P>Next, there are two basic lemmas involving the conditional operator
that we use for the Weak Deduction Theorem. The
lemma <A HREF="elimhyp.html">elimhyp</A> is intended to take a provable
special case of the hypothesis to be eliminated and transform it into a
special substitution instance of that hypothesis. This in turn is fed
into the deduction to be eliminated, and the deduction's output is then
fed into the lemma <A HREF="dedth.html">dedth</A> to produce the final
theorem.
<P>The last hypothesis of each of the following lemmas is the important
one. The other hypotheses just specify the substitution instances we
need and are are always easily constructed using simple equality laws.
Using each last hypothesis as the "input" to each lemma, the proof of a
theorem from a deduction follows this outline: [provable special case]
-> <A HREF="elimhyp.html">elimhyp</A> -> [known deduction] ->
<A HREF="dedth.html">dedth</A> -> [deduction converted to theorem].
<P>An auxilliary lemma, <A HREF="keephyp.html">keephyp</A>,
can be used if we wish to eliminate some hypotheses but keep others.
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"> <CAPTION><B>Definition of
the conditional operator, and three key lemmas</B></CAPTION>
<TR ALIGN=LEFT><TD><A HREF="df-if.html">df-if</A></TD><TD>
` |- if ( ph , A , B ) = { x | `
` ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } ` </TD></TR>
<TR ALIGN=LEFT><TD><A HREF="elimhyp.html">elimhyp</A></TD><TD>` |- ( A = if ( ph , A , B ) -> ( ph <-> ps ) ) ` ` & ` ` |- ( B = if ( ph , A , B ) -> ( ch <-> ps ) ) ` ` & ` ` |- ch ` ` => `
` |- ps ` </TD></TR>
<TR ALIGN=LEFT><TD><A HREF="dedth.html">dedth</A></TD><TD>` |- ( A = if ( ph , A , B ) -> ( ps <-> ch ) ) ` ` & ` ` |- ch ` ` => `
` |- ( ph -> `
` ps ) ` </TD></TR>
<TR ALIGN=LEFT><TD><A HREF="keephyp.html">keephyp</A></TD><TD>` |- ( A = if ( ph , A , B ) -> ( ps <-> th ) ) ` ` & ` ` |- ( B = if ( ph , A , B ) -> ( ch <-> th ) ) ` ` & ` ` |- ps ` ` & ` ` |- ch ` ` => `
` |- th ` </TD></TR>
</TABLE></CENTER>
<P>In addition to the above lemmas, a number of variations are also
proved for convenient use. These allow us to eliminate several
hypotheses simultaneously, to eliminate hypotheses where multiple class
variables must be substituted simultaneously with specific classes in
order to obtain the provable special case, and to eliminate hypotheses
that occur in frequently-used specific forms. They can be browsed by
clicking on <A HREF="dedth.html">dedth</A> then clicking on the "Related
theorems" link. It is easiest to learn how they work by looking at
examples of their use, which can be found in the "This theorem is
referenced by" links on their web pages.
<P><HR NOSHADE SIZE=1><A NAME="setex"></A><B><FONT COLOR="#006633">A Set
Theory Example</FONT></B> Probably the easiest way to
become familiar with the Weak Deduction Theorem is by studying a few of
the many places it is used in set theory.
<P>Here is an example of the class version of the Weak Deduction Theorem
in action. In the set.mm database you will find that we have proved the
result
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><A HREF="renegcli.html">renegcli</A></TD><TD>` |- A e. RR ` ` => ` ` |- -u A e. RR ` </TD></TR>
</TABLE></CENTER>
<P>which means, if you have a proof that <I><FONT
COLOR="#CC33CC">A</FONT></I> is a real number (belongs to the set of
reals), then you will also have a proof that its negative is a
real number. (The proof of <A HREF="renegcli.html">renegcli</A> is not
relevant to us right now, and you can ignore it.) The application of
the Weak Deduction Theorem yields (and this is the proof you'll want to
look at):
<P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA">
<TR ALIGN=LEFT><TD><A HREF="renegcl.html">renegcl</A></TD><TD>
` |- ( A e. `
` RR -> -u A e. RR ) ` </TD></TR>
</TABLE></CENTER>
<P>which means that
"` A `
is a real
number" implies "the negative of
` A `
is a real number". In the proof, we made use of <A
HREF="elimel.html">elimel</A>, which is a frequently used special case
of <A HREF="elimhyp.html">elimhyp</A>. Also, we made use of the special
case that one is a real number <A HREF="1re.html">1re</A> to
eliminate the hypothesis of <A HREF="elimel.html">elimel</A> (and thus
<A HREF="elimhyp.html">elimhyp</A> from which it is derived).
<P>In this example, we did not make use of <A
HREF="keephyp.html">keephyp</A>. For an example that uses it (via <A
HREF="keepel.html">keepel</A>), see the proof of <A
HREF="divcan2zi.html">divcan2zi</A>.
<P><HR NOSHADE SIZE=1><A NAME="proof"></A><B><FONT COLOR="#006633">Informal
Proof of the Weak
Deduction Theorem</FONT></B> Here we show a
high-level proof of the Weak Deduction Theorem. The proof contains
the detailed construction that converts a hypothesis into an antecedent.
Our lemmas <A HREF="elimh.html">elimh</A> and <A
HREF="dedt.html">dedt</A> implement this construction into a more
compact form for practical application. This proof was adapted from an
email I wrote, and I left it in its original ASCII form, where
<TT>~</TT> means
` -. ` ,
<TT>^</TT> means
` /\ ` ,
etc.
<!-- <P><CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#FAEEFF"><TR><TD ALIGN=LEFT> -->
<P><CENTER><TABLE BORDER CELLSPACING=0 CELLPADDING=5 BGCOLOR="#F0F0F0"><TR><TD ALIGN=LEFT>
<PRE>
In propositional calculus, the deduction theorem for one hypothesis
states (where A and B are wffs):
If A |- B then |- A -> B
(We will ignore the converse, being a trivial application of modus
ponens. In the description that follows, all letters refer to fixed wffs
or to variables ranging over wffs—"wff variables"—as indicated.)
Here we show a different kind of construction for the deduction theorem
that, unlike the standard Tarski/Herbrand deduction theorem, doesn't
require rewriting the proof of the deduction but simply adds a fixed
number of steps (roughly proportional to formula length) to a proof for
A |- B to result in a proof for |- A -> B.
It is an unusual application of classical logic in that it involves a
kind of self-reference wherein a formula is substituted into itself.
It is important to note that this version does not replace the standard
one because it is weaker. In particular, we can't eliminate a hypothesis
that is a contradiction: for example we can't use the theorem to derive
|- (¬A ^ A) -> B from ¬A ^ A |- B. We must be able to prove separately
a special case of the hypothesis. For example, if we are given
(A -> B) |- (¬B -> ¬A) and want to prove |- (A -> B) -> (¬B -> ¬A), the
theorem will give us the proof provided we also have a proof for the
special case |- (B -> B), where wff "(B -> B)" is the hypothesis
"(A -> B)" with B substituted for A.
Now for the theorem. For our notation, we state axioms, theorems, and
proof steps as _schemes_ where the variables range over wffs. If F is a
wff, and A is a wff variable contained in F, let us denote F by F(A).
If G is another wff, then F(G) is the wff obtained by substituting all
occurrences of wff variable A with wff G. (More precisely, we first
replace variable A in F with a new wff variable not occurring elsewhere,
then we substitute G for that new wff variable. This eliminates any
ambiguity when G itself contains A.) For example, if F == F(A) = A v B
and G = A ^ C, we have F(G) = (A ^ C) v B. Also, F(F(A)) = F(F) =
(A v B) v B, F(F(F(A))) = ((A v B) v B) v B, etc. I hope this notation
is clear.
Theorem
-------
Assume F |- G. Denote F by F(A) where A is some wff variable in F, and
assume there is a wff B such that |- F(B). Then, in classical logic,
|- F -> G.
Proof
-----
We will use F and F(A) interchangeably, and we also will denote G by
G(A).
In classical logic we have
|- F -> (A <-> ((A ^ F) v (B ^ ¬F))) (1)
|- ¬F -> (B <-> ((A ^ F) v (B ^ ¬F))) (2)
Also in classical logic, for any wffs P,Q,R,S,T we have
If |- P -> (Q <-> R) then |- P -> (¬Q <-> ¬R)
If |- P -> (Q <-> R) and |- P -> (S <-> T)
then |- P -> ((Q -> S) <-> (R -> T))
corresponding to the primitive connectives ¬ and ->. Using these, and
(1) and (2) as the basis, we derive by induction on the formula length
of F (with ^, v, etc. implicitly expanded into ¬ and -> primitives)
|- F -> (F(A) <-> F((A ^ F) v (B ^ ¬F))) (3)
|- ¬F -> (F(B) <-> F((A ^ F) v (B ^ ¬F))) (4)
From (3) we have (since F = F(A) by definition)
|- F -> F((A ^ F) v (B ^ ¬F)) (5)
Since |- F(B) by hypothesis, from (4) we have
|- ¬F -> F((A ^ F) v (B ^ ¬F)) (6)
Combining (5) and (6), we obtain
|- F((A ^ F) v (B ^ ¬F)) (7)
By hypothesis F(A) |- G(A). Substituting ((A ^ F) v (B ^ ¬F)) for A
gives
F((A ^ F) v (B ^ ¬F)) |- G((A ^ F) v (B ^ ¬F)) (8)
Since (7) satisfies the hypothesis of (8) we have
|- G((A ^ F) v (B ^ ¬F)) (9)
By induction on the formula length of G, from (1) we derive