| Description: Deduction introducing an
embedded antecedent.
Naming convention: We often call a theorem a
"deduction" and suffix
its label with "d" whenever the hypotheses and conclusion are
each
prefixed with the same antecedent. This allows us to use the theorem in
places where (in traditional textbook formalizations) the standard
Deduction Theorem would be used; here  would be replaced with a
conjunction (df-an 360) of the hypotheses of the would-be deduction.
By
contrast, we tend to call the simpler version with no common antecedent
an "inference" and suffix its label with "i";
compare theorem a1i 10.
Finally, a "theorem" would be the form with no hypotheses; in
this case
the "theorem" form would be the original axiom ax-1 6.
We usually show
the theorem form without a suffix on its label (e.g. pm2.43 47 vs.
pm2.43i 43 vs. pm2.43d 44). When an inference is converted to a theorem
by eliminating an "is a set" hypothesis, we sometimes suffix
the theorem
form with "g" (for "more general") as in uniex 4317 vs. uniexg 4316.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan,
20-Mar-2006.) |
