ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-bi GIF version

Definition df-bi 116
Description: This is our first definition, which introduces and defines the biconditional connective , also called biimplication. 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, as it allows us to use logic to manipulate definitions directly. For an example of such a definition, see df-3or 968. 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 969) 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 biijust 631. It is impossible to use df-bi 116 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 116 in the proof with the corresponding biijust 631 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 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 for human readability.)

df-bi 116 itself is a conjunction of two implications (to avoid using the biconditional in its own definition), but once we have the biconditional, we can prove dfbi2 386 which uses the biconditional instead.

Other definitions of the biconditional, such as dfbi3dc 1386, only hold for decidable propositions, not all propositions. (Contributed by NM, 5-Aug-1993.) (Revised by Jim Kingdon, 24-Nov-2017.)

Assertion
Ref Expression
df-bi (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))

Detailed syntax breakdown of Definition df-bi
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 wps . . . 4 wff 𝜓
31, 2wb 104 . . 3 wff (𝜑𝜓)
41, 2wi 4 . . . 4 wff (𝜑𝜓)
52, 1wi 4 . . . 4 wff (𝜓𝜑)
64, 5wa 103 . . 3 wff ((𝜑𝜓) ∧ (𝜓𝜑))
73, 6wi 4 . 2 wff ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
86, 3wi 4 . 2 wff (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓))
97, 8wa 103 1 wff (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
Colors of variables: wff set class
This definition is referenced by:  biimp  117  bi3  118  biimpr  129  dfbi2  386  sb4bor  1822
  Copyright terms: Public domain W3C validator