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.

##

## 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))))