Description: Define disjunction
(logical 'or'). Definition of [Margaris] p.
49. When
the left operand, right operand, or both are true, the result is true;
when both sides are false, the result is false. For example, it is true
that   (ex-or 25927). After we define the constant
true (df-tru 1458) and the constant false (df-fal 1461), we
will be able to prove these truth table values:

(truortru 1481), 
(truorfal 1482), 
(falortru 1483), and

(falorfal 1484).
This is our first use of the biconditional connective in a definition; we
use the biconditional connective in place of the traditional
"<=def=>",
which means the same thing, except that we can manipulate the
biconditional connective directly in proofs rather than having to rely on
an informal definition substitution rule. Note that if we mechanically
substitute   for   , we end up
with an
instance of previously proved theorem biid 244.
This is the justification
for the definition, along with the fact that it introduces a new symbol
. Contrast
with (df-an 377), (wi 4),
(df-nan 1395), and (df-xor 1416) . (Contributed by NM,
27-Dec-1992.) |