The category of propositions, Prop

proposition!category Prop In order to relate this account of typed logic to the type theory of section 3 and to programming section , I would like to consider the collection of all propositions and refer to it as Prop.⁹ But we know already from Principia that the concept of proposition is indefinitely extensible. Here is how Whitehead and Russell put the matter.

``...vicious circles...[arise] from supposing that a collection of objects may contain members which can only be defined by means of the collection as a whole. Thus, for example, the collection of propositions will be supposed to contain a proposition stating that `all propositions are either true or false.' It would seem, however, that such a statement could not be legitimate unless `all propositions' referred to some already definite collection, which it cannot do if new propositions are created by statements about `all propositions.' We shall, therefore, have to say that statements about `all propositions' are meaningless. By saying that a set has `no total,' we mean, primarily, that no significant statement can be made about `all its members.' In such cases, it is necessary to break up our set into smaller sets, each of which is capable of a total. This is what the theory of types aims at effecting.''

So we must be very careful about introducing this notion. There are predicative approaches to this which lead to level restrictions as in Principia and allow writing Prop_i as the ``smaller collections'' into which Prop is broken ([80,28]).¹⁰ There are impredicative approaches that allow Prop but restrict the logic in other ways ([50]). Ultimately we will impose level restrictions on Prop and relate it to another indefinitely extensible concept which we denote as Type. These restrictions and relationships will occupy us in section 3.

>From the beginning I want to recognize that we intend to treat collections of propositions as mathematical objects -- some collections will be types, some will be too ``comprehensive'' to be types. We will call these large collections categories or classes or kinds or large types to use names suggestive of ``large collections.''

The use of Propproposition!category Prop as a concept in this account of logic, while not common in logic texts, provides an orientation to the subject which will gradually reveal problems that I think are both philosophically and practically important. So I adopt it here. We recognize at the onset that Prop will not denote all propositions. We will be developing an understanding of how to talk about such open-ended notions in a meaningful way. This development will confirm that at the very least we can name them. The issue is what else can we say?