Definition df-bi in this section is our first definition, which
introduces and defines the biconditional connective used to denote
logical equivalence. We define a wff of the form as an
abbreviation for .
Unlike most traditional developments, we have chosen not to have a separate
symbol such as "Df." to mean "is defined as". Instead, we will later use the
biconditional connective for this purpose (df-an is its first use), as it
allows to use logic to manipulate definitions directly. This greatly
simplifies many proofs since it eliminates the need for a separate mechanism
for introducing and eliminating definitions.
A note on definitions: definitions are required to be eliminable (that is, a
theorem stated in terms of the defined symbol can also be stated without it)
and conservative (that is, a theorem whose statement does not contain the
defined symbol can be proved without using that definition). This means that
a definition does not increase the expressive power nor the deductive power,
respectively, of a theory. On the other hand, definitions are often useful
to write shorter proofs, so in (i)set.mm we will generally not try to avoid
them. This is why, for instance, some theorems which do not contain
disjunction in their statement are placed after the section on disjunction
because a shorter proof using disjunction is possible.