next up previous contents index
Next: Elementary Number Theory Up: Defining Logics Previous: Classical Logic

Other Logical Operators

A number of other logical concepts can be expressed in Nuprl. For example, the conditional  and is sometimes used when dealing with partial functions. This connective can be defined as <p:prop> cand  <q:prop> == (x:<p> # <q>). This results in an and connective which forces the evaluation of its first argument before the second argument.

As another example, sometimes it is useful to simplify the structure of a type considered as a proposition by ``squashing'' all of the proofs into one object. This squash  operator is defined as

        || <p:prop> || == {0 in int | <p> }.
Thus if <p> is true then || <p> || consists of a single object; all the different proofs have been identified. Note that this operator is built using the subset type constructor.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995