Home| Home |
Metamath Proof Explorer |
| Contents of this page |
A Theorem fine is Deduction, For it allows work-reduction: To show "A implies B", Assume A and prove B; Quite often a simpler production. --Stefan Bilaniuk A Problem Course in Mathematical Logic, 2003 [external] |
is placed in
front of the final assertion, and the hypothesis itself is eliminated).
Example: Look at the proof of
renegclt. In step 5, there is a reference
to the deduction renegcl,
"
". A special substitution instance of
renegcl
is used to feed the last hypothesis of
the deduction theorem dedth, which in turn
converts it to the theorem
" 
" in step 6. The somewhat
bizarre-looking steps leading up to 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 renegcl at
step 5.
On this page we attempt to show you how this technical stuff works if you
are interested. We also discuss the conditional operator
"
" that you
will find in these proofs.
| con3i | 
|
This means that if we have proved a theorem of the form
(where
and
are any wffs), then
we can conclude the theorem
.
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."
An example of a theorem is the law of contraposition:
| con3th |
|
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.
|
|
and we want to then prove a theorem of the form
|
|
Doing this is not as simple as you might think. The deduction says,
"if we can prove
then we can prove
,"
which is in some
sense weaker than saying
"
implies
."
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 theorem and a related version that
we use are all about.
On the other hand, if we have the theorem, it is easy to recover the deduction using modus ponens ax-mp. An example of this is the derivation of the inference a2i from the axiom ax-2.
In ordinary mathematics, no one actually carries out the algorithm, since (in its most basic form) it causes an exponential explosion of the number of proof steps as more hypotheses are eliminated. Instead, the Standard Deduction Theorem is viewed simply as a high-level "metaaxiom" or "metatheorem" that is applied directly. In other words, mathematicians rarely show the actual proof of a theorem but only that it can be proved.
Here, we want to show you actual proofs. 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.
Incorporating a high-level metatheorem such as the Standard Deduction Theorem into our method of displaying proofs would require you to learn additional concepts beyond simple substitution of expressions for variables, in order to follow the proofs and verify for yourself they are correct. For example, the use of the Standard Deduction Theorem requires you to understand certain subtle restrictions when working with predicate calculus. (Specifically, if the Axiom of Generalization was used in the proof of the original deduction to quantify a free variable in its hypothesis, the Standard Deduction Theorem may fail.)
An example of such a subtlety is as follows. When 
and 
are distinct variables, the following
(silly) deduction can be proved in set theory:
|
The reason this deduction holds is that the hypothesis, which effectively
states "for all and ,
is true," can never be proved as a stand-alone theorem, in
fact it is provably false, so any conclusion whatsover follows from it.
However, if we blindly apply the Standard Deduction Theorem, the theorem
form of the deduction ("if two things are equal then they are not equal") is
obviously absurd:
| Incorrect:
|
Part of the purpose of Metamath is to let you plainly see, with as few underlying concepts as possible, how mathematics can be derived directly from the axioms, and not indirectly according to some hidden rules buried inside a program or understood only by logicians. 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.
The Weak Deduction Theorem is used often 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.
What are its limitations?
Specifically, if a special case of the hypothesis can be proved as a
stand-alone theorem, then we can generalize this special case in a way
that allows us to eliminate the hypothesis from the deduction and
introduce it as an antecedent to arrive at the desired theorem. It
cannot be used in all cases - for example, it cannot be used when the
hypothesis is a contradiction such as 
. However, in the case
of the contraposition deduction above, by substituting for in the hypothesis
, we obtain the trivially proved identity theorem id,
.
This special case can be used (together with some auxilliary lemmas) to
eliminate the hypothesis and introduce it as an antecedent.
Does its limitation cause us inconvenience? In Metamath's set theory development, a modified version for classes (see the set theory version 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 specifies that a class variable must be a nonzero real number, the special case of 1 will satisfy the hypothesis.
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 Axiom of Choice are sometimes like this. In such a case, the Weak Deduction Theorem cannot be used. However, so far our I have not encountered an example where direct derivation of the theorem form has been impractical.
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.
A better suggestion: If you are familiar with a little set theory, just skip ahead directly to the Weak Deduction Theorem in set theory. We never use the Weak Deduction Theorem in propositional calculus except for the contrived example con3th created for the next section.
The auxilliary lemmas we need for the Weak Deduction Theorem in propositional calculus are elimh and dedt. The first takes the special case (such as id 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 dedt, and magically the desired theorem pops out as the conclusion of dedt, with the original hypothesis transformed into an antecedent. Below we show these auxilliary lemmas.
| elimh |      
|
| dedt |
|
In lemma elimh, the wff
is the hypothesis of the original deduction. The wff
is the special case
(such as id in our example above) of
that hypothesis.
is the wff variable of the deduction's hypothesis that is replaced
with wff variable
to result in the special case.
The first two
hypotheses of elimh are trivially-proved technical hypotheses
that specify substitutions. The first one tells elimh
that when the wff
is substituted for the wff variable
in wff
(the hypothesis of the original deduction), the result is wff
.
The "substitution" of
for
(in wff
to result in wff
)
specified by the
second hypothesis of elimh
is special - not
all occurrences of wff variable
are replaced, but only the ones at the
variable positions replaced in the first elimh
hypothesis (the example in the next section should help clarify this).
The conclusion of elimh 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 dedt.
In lemma dedt, the wff
is the hypothesis of the original deduction, and the
wff
is the conclusion
of the original deduction.
The first hypothesis of dedt
tells it that when the wff
is substituted for the wff variable
in wff
, the result is
wff
.
The conclusion of dedt, the wff
,
is the desired theorem.
It may be hard to understand intuitively how the Weak Deduction Theorem works just by looking at elimh and dedt. In a later section, we give a proof 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.
Steps 1 through 6 of con3th 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 binegd and birimd. We use the term "substitution" loosely, since for the "special case" wff (step 6) we don't replace all occurrences of the variable but only those positioned where the original replacement was made to create the "special case".
Step 4
proves that the substitution of
for
in the contraposition hypothesis wff
results in
.
This is assigned to the first hypothesis of
elimh.
Step 6
proves that the substitution of
for the second
in the special case wff
results in
.
This is assigned to the second hypothesis of
elimh.
Step 3
proves that the substitution of
for
in the contraposition conclusion wff
results in
.
This is assigned to the first hypothesis of
dedt.
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 con3th was contrived just for the purpose of this example. Compare the more efficient direct proof of the same theorem in con3.
Where the Weak Deduction Theorem becomes very useful, if not essential, is in set theory. For set theory, special versions of elimh and dedt, called elimhyp and dedth respectively, are devised that work with substitutions into classes instead of wffs.
To make things more efficient, we introduce a special notation
df-if called a "conditional operator"
that combines a wff and two classes to produce another class.
Read as "if
is true then
the value is else
the value is ."
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 other many
applications in addition to its use with the Weak Deduction Theorem.)
Next, there are two basic lemmas involving the conditional operator that we use for the Weak Deduction Theorem. The lemma elimhyp 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 dedth to produce the final theorem.
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 satisfied 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] -> elimhyp -> [known deduction] -> dedth -> [deduction converted to theorem].
An auxilliary lemma, keephyp, can be used if we wish to eliminate some hypotheses but keep others.
| df-if |
 
 |
| elimhyp |
|
| dedth |
|
| keephyp |
|
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 dedth then clicking on the "Theorem list" link.
| renegcl |
|
which means, if I can prove that A is a real number (belongs to the set of reals), then I can prove that its negative is a real number. (The proof of renegcl 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):
| renegclt |
|
which means that
"
is a real
number" implies "the negative of
is a real number". In the proof, we made use of elimel, which is a frequently used special case
of elimhyp. Also, we made use of the special
case that zero is a real number ax0re to
eliminate the hypothesis of elimel (and thus
elimhyp from which it is derived).
In this example, we did not make use of keephyp. For an example that uses it (via keepel), see the proof of recidz.
,
^ means
,
etc.
In propositional calculus, the deduction theorem for one hypothesis
states:
If A |- B then |- A -> B
(We will ignore the converse, being a trivial application of modus
ponens.)
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 (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.) 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
|- 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
|- F -> (G(A) <-> G((A ^ F) v (B ^ ~F))) (10)
From (9) and (10) we finally obtain
|- F -> G Q.E.D.
Example: Suppose we have a proof for (A -> B) |- (~B -> ~A) and also a
proof of |- (B -> B), which is a special case of the hypothesis. Let
F(A) = (A -> B) and G(A) = (~B -> ~A). Then F(B) = (B -> B), and the
theorem gives us |- (A -> B) -> (~B -> ~A).
The theorem provides us with the algorithm for constructing the proof in
detail if we wish. For example the proof step corresponding to (7)
becomes |- (A ^ (A -> B)) v (B ^ ~(A -> B))) -> B. It is easy to see
that the number of steps in the final proof is equal to the number of
steps in the proof of the original deduction and the special case, plus
(primarily) a number of steps proportional to formula length used to
derive (3), (4), and (10).
The theorem can be extended to eliminate multiple hypotheses, as well as
variants that keep some hypotheses while eliminating others. |