Description: This is our first
definition, which defines the biconditional connective
 . 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, as it
allows us to use logic to manipulate definitions directly (df-or 197
is
its first use). Here we use the biconditional connective to define
itself, a feat which requires a little care. We define    
as   but we don't yet have a
notation that can express this directly, so we use a more complicated
expression using the language that we have so far. The justification
for our definition is that if we mechanically substitute the second wff
for the first in the definition, the definition becomes an instance of
previously proved theorem bijust 126. Note that from Metamath's point of
view, a definition is just another axiom; but from our high level point
of view, we are are not strengthening the language since if we
mechanically eliminate the new symbol we will not end up with
any theorems we could not prove before. To indicate this fact we prefix
definition labels with "df-" instead of "ax-". (This
prefixing is an
informal convention that means nothing to the Metamath proof verifier;
it is just for human readability.) See bii 140 and
bi 396
for theorems
suggesting the typical textbook definition of . |
Home
