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
?Error:
2 = 3 \/ 4 = 4 )
^
This math symbol is not active (i.e. was not declared in this scope).
that (2=3\/4=4) (ex-or21765). After we define the constant
?Error:
T.
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
F.
^^
This math symbol is not active (i.e. was not declared in this scope).
true (df-tru1329) and the constant false (df-fal1330), we
will be able to prove these truth table values:
?Error:
T. \/ T. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
T. \/ F. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
((\/)<->) (truortru1350), ((\/)<->)
?Error:
F. \/ T. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
(truorfal1351), ((\/)<->) (falortru1352), and
?Error:
F. \/ F. ) <-> F. )
^^
This math symbol is not active (i.e. was not declared in this scope).
((\/)<->) (falorfal1353).
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 biid229.
This is the justification
for the definition, along with the fact that it introduces a new symbol
?Error:
-/\
^^^
This math symbol is not active (i.e. was not declared in this scope).
\/. Contrast with /\ (df-an362), -> (wi4), -/\
?Error:
\/_
^^^
This math symbol is not active (i.e. was not declared in this scope).
(df-nan1298), and \/_ (df-xor1315) . (Contributed by NM,
5-Aug-1993.)
