Definition df-bi 209

Description: Define the biconditional (logical "iff" or "if and only if"), also called biimplication.

Definition df-bi 209 in this section is our first definition, which introduces and defines the biconditional connective ↔. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)).

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 (df-an 398 is its first use), as it allows 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 df-3an 1095) 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 207. It is impossible to use df-bi 209 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 df-bi 209 in the proof with the corresponding bijust 207 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.)

After we define the constant true ⊤ (df-tru 1551) and the constant false ⊥ (df-fal 1561), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1577), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1579), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1578), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1580).

See dfbi1 215, dfbi2 476, and dfbi3 1056 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 215 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 477 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding.

Contrast with ∨ (df-or 855), → (wi 4), ⊼ (df-nan 1500), and ⊻ (df-xor 1520). In some sense ↔ returns true if two truth values are equal; = (df-cleq 2733) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.)

Assertion

Ref	Expression
df-bi	⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))

Detailed syntax breakdown of Definition df-bi

Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff 𝜑
2		wps	. . . . 5 wff 𝜓
3	1, 2	wb 208	. . . 4 wff (𝜑 ↔ 𝜓)
4	1, 2	wi 4	. . . . . 6 wff (𝜑 → 𝜓)
5	2, 1	wi 4	. . . . . . 7 wff (𝜓 → 𝜑)
6	5	wn 3	. . . . . 6 wff ¬ (𝜓 → 𝜑)
7	4, 6	wi 4	. . . . 5 wff ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))
8	7	wn 3	. . . 4 wff ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))
9	3, 8	wi 4	. . 3 wff ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
10	8, 3	wi 4	. . . 4 wff (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
11	10	wn 3	. . 3 wff ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
12	9, 11	wi 4	. 2 wff (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
13	12	wn 3	1 wff ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))

This definition is referenced by:  impbi  210  dfbi1  215  dfbi1ALT  216  biimp  217  dfbi1ALTa  45396  dfbi1ALTb  45398