| Description: Deduction introducing an
embedded antecedent. (The proof was revised by
Stefan Allan, 20-Mar-2006.)
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 (wa 104) 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 9.
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 53 versus
pm2.43i 49 versus pm2.43d 50). (Contributed by NM, 5-Aug-1993.)
(Revised by NM, 20-Mar-2006.) |
