df-or
Show Code edit

## Definition of OR

##

## Define disjunction (logical 'or'). This is our first use of the

## biconditional connective in a definition; we use it 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 #(-> (-. ph) ps)# for #(\/ ph ps)#,

## we end up with an instance of previously proved identity theorem. This

## is the justification for the definition, along with the fact that it

## introduces a new symbol \/.

##

defthm (df-or wff (\/ ph ps) () () (<-> (\/ ph ps) (-> (-. ph) ps))

(-> (-. ph) ps) biid

(<-> (-> (-. ph) ps) (-> (-. ph) ps))

)