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