Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfbi  Unicode version 
Description: Define the biconditional
(logical 'iff').
The definition dfbi 179 in this section is our first definition, which
introduces and 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 (dfor 361 is its first use), as it allows us 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. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet. Instead, we use a more general form of definition, described as follows. In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df3an 939) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements. The justification for our definition is that if we mechanically replace (the definiendum i.e. the thing being defined) with (the definiens i.e. the defining expression) in the definition, the definition becomes the previously proved theorem bijust 177. It is impossible to use dfbi 179 to prove any statement expressed in the original language that can't be proved from the original axioms, because if we simply replace each instance of dfbi 179 in the proof with the corresponding bijust 177 instance, we will end up with a proof from the original axioms. Note that from Metamath's point of view, a definition is just another axiom  i.e. an assertion we claim to be true  but from our high level point of view, we are not strengthening the language. 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 a naming convention for human readability.)
?Error:
T.
^^
This math symbol is not active (i.e. was not declared in this scope).
After we define the constant true (dftru 1329) and the constant
?Error:
F.
^^
This math symbol is not active (i.e. was not declared in this scope).
false (dffal 1330), we will be able to prove these truth table
?Error:
T. <> T. ) <> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
values:
See dfbi1 186, dfbi2 611, and dfbi3 865
for theorems suggesting typical
textbook definitions of
?Error:
\/
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
/\
^^^
This math symbol is not active (i.e. was not declared in this scope).
Contrast with 
Ref  Expression 

dfbi 
Step  Hyp  Ref  Expression 

1  wph  . . . . 5  
2  wps  . . . . 5  
3  1, 2  wb 178  . . . 4 
4  1, 2  wi 4  . . . . . 6 
5  2, 1  wi 4  . . . . . . 7 
6  5  wn 3  . . . . . 6 
7  4, 6  wi 4  . . . . 5 
8  7  wn 3  . . . 4 
9  3, 8  wi 4  . . 3 
10  8, 3  wi 4  . . . 4 
11  10  wn 3  . . 3 
12  9, 11  wi 4  . 2 
13  12  wn 3  1 
Colors of variables: wff set class 
This definition is referenced by: bi1 180 bi3 181 dfbi1 186 dfbi1gb 187 
Copyright terms: Public domain  W3C validator 