def-bi Show Code edit
## Definition of Biconditional
##
## This is our first definition, which introduces and defines the
## biconditional connective {{{<->}}}. We define a wff of the form
## #(<-> ph ps)# as an abbreviation for
## #(-. (-> (-> ph ps) (-. (-> ps ph))))#.
##
## 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-or is its
## first use), as it allows us 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 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.
##
## See dfbi1, dfbi2, and dfbi3 for theorems suggesting typical
## textbook definitions of <->, showing that our definition has the
## properties we expect. Theorem dfbi shows this definition rewritten
## in an abbreviated form after conjunction is introduced.
##
defthm (def-bi wff (<-> ph ps) () ()
(/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
(-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps)))
(/\ (-> ph ps) (-> ps ph)) id
(-> (/\ (-> ph ps) (-> ps ph)) (/\ (-> ph ps) (-> ps ph)))
(/\ (-> ph ps) (-> ps ph)) id
(-> (/\ (-> ph ps) (-> ps ph)) (/\ (-> ph ps) (-> ps ph)))
(/\ (-> (/\ (-> ph ps) (-> ps ph)) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (/\ (-> ph ps) (-> ps ph))))
edit