Propositions and Universes

In so-called ``classical'' accounts of logic, a proposition has a truth value in . Consequently, propositions can be treated as boolean expressions. This boolean-valued account is more restrictive than the one we need in order to discuss computability issues, so we adopt a more abstract account of propositions. We want to consider both the sense and the truth of a proposition. In particular we are interested in their computational sense.

We will, of course, talk about the truth value of a proposition as well as its sense. The type of all propositions needed in this article is denoted . Nuprl can express ``higher order logic'' as well, in which case ``larger'' propositions are needed. See Jackson [20] or [9] for fuller accounts of higher order logic.

There are two distinguished atomic propositions, the canonically true one and the canonically false one. Given propositions we can form compounds in the usual way:

A propositional function on a type is any map Given such a , then we can form the propositions:

``for all of type holds,''
``for some of type holds.''

Also associated with every type is the atomic equality proposition, in . The definition of this equality is given with each type.

In classical logic the boolean value is considered the same as the true proposition and is identified with . But the proposition we associate with a boolean expression is this atomic equality: in . Given we denote the corresponding proposition as True(). Clearly we know True() iff and True() iff . Sometimes we denote True() by for short. We call this up arrow ``assert.''

The types we need belong to a universe, . If and are types then we have seen that and are also types.