| Description: Define conjunction
(logical 'and'). Definition of [Margaris] p.
49. When
both the left and right operand are true, the result is true; when either
is false, the result is false. For example, it is true that
(2 = 2 ∧ 3 = 3). After we define the constant
true ⊤
(df-tru 1634) and the constant false ⊥ (df-fal 1637), we will be able
to prove these truth table values: ((⊤ ∧
⊤) ↔ ⊤)
(truantru 1654), ((⊤ ∧ ⊥)
↔ ⊥) (truanfal 1655),
((⊥ ∧ ⊤) ↔ ⊥) (falantru 1656), and
((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1657).
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 251.
This is the justification
for the definition, along with the fact that it introduces a new symbol
∧. Contrast with ∨
(df-or 837), → (wi 4), ⊼
(df-nan 1596), and ⊻ (df-xor 1613) . (Contributed by NM,
5-Jan-1993.) |
