New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-or GIF version

Definition df-or 359
 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 (2 = 3 ∨ 4 = 4) (see ex-or in set.mm). After we define the constant true ⊤ (df-tru 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ∨ ⊤ ) ↔ ⊤ ) (truortru 1340), (( ⊤ ∨ ⊥ ) ↔ ⊤ ) (truorfal 1341), (( ⊥ ∨ ⊤ ) ↔ ⊤ ) (falortru 1342), and (( ⊥ ∨ ⊥ ) ↔ ⊥ ) (falorfal 1343). 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 227. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Contrast with ∧ (df-an 360), → (wi 4), ⊼ (df-nan 1288), and ⊻ (df-xor 1305) . (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-or ((φ ψ) ↔ (¬ φψ))

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
31, 2wo 357 . 2 wff (φ ψ)
41wn 3 . . 3 wff ¬ φ
54, 2wi 4 . 2 wff φψ)
63, 5wb 176 1 wff ((φ ψ) ↔ (¬ φψ))
 Colors of variables: wff setvar class This definition is referenced by:  pm4.64  361  pm2.53  362  pm2.54  363  ori  364  orri  365  ord  366  imor  401  mtord  641  orbi2d  682  orimdi  820  ordi  834  pm5.17  858  pm5.6  878  orbidi  898  cador  1391  cadan  1392  19.30  1604  19.43  1605  nfor  1836  19.32  1875  dfsb3  2056  sbor  2066  axi12  2333  neor  2600  r19.30  2756  r19.32v  2757  r19.43  2766  dfif2  3664  ltfintrilem1  4465  evenodddisjlem1  4515  fce  6188
 Copyright terms: Public domain W3C validator