Propositional Levels and Predicativity

Thm* A  B  (C:Prop. (A  C)  (B  C)  C)
Thm* a,b:A. a = b  (P:(AProp). P(a)  P(b))

we cannot adopt these as definitions, although it is not unusual to do so in some other accounts of higher-order logic. The reason is that we have adopted a "predicative" semantics (a term of Bertrand Russell's of uncertain etymology) which avoids defining a proposition by quantifying over a domain that includes the proposition to be defined. Basically, in a predicative logic, to assign meaning to a quantificational expression one must "already" have given meaning to all the expressions that might be used as witnesses. So, assigning a meaning to "C:Prop. (A  C)  (B  C)  C" requires already having assigned a meaning to every member of Prop, which therefore could not include "C:Prop. (A  C)  (B  C)  C" itself as a member. Thus, there is no type of all propositions in predicative type theory.

The solution adopted here is to stratify the propositions into a hierarchy Prop{i} where "i" is some positive number. Then

Thm* A,B:Prop{i}. (C:Prop{i}. (A  C)  (B  C)  C)  Prop{i'}
Thm* A:Type{i}, a,b:A. (P:(AProp{i}). P(a)  P(b))  Prop{i'}

where Prop{i'} is the next level of propositions above Prop{i}. The propositional levels are treated identically to the type levels explained in Universes and in Type Functionality Sequents. But disjunction and equality do not raise the propositional level, so the "iffs" of their higher-order characterizations cannot be converted to definitions:

Thm* A,B:Prop{i}. (A  B)  Prop{i}
Thm* T:Type{i}, a,b:T. (a = b  T)  Prop{i}

As with Universe Levels we normally elide the proposition level from display when it just a single level variable used throughout the expression. See Propositions for examples.

Quantification over types raises the propositional level, just as does quantification over propositions, indeed, "Type{[level]}" and "Prop{[level]}" are interchangeable as far as determining levels is concerned.

Thm* Prop{i}  Type{i'}
Thm* Prop{i}  Prop{i'}

Because the universes and propositional types are cumulative, one can often state theorems with a single level variable. For example,

Thm* A:Type{k}, P:(AProp{j}). (x:A. P(x))  Prop{[k | j]}

which says that the existential is a proposition at the maximum of the two levels of its domain and predicate, follows simply from the at-first-sight less general

Thm* A:Type{i}, P:(AProp{i}). (x:A. P(x))  Prop{i}

since if A  Type{k} and P  AProp{j} then A  Type{[k | j]} and P  AProp{[k | j]}, putting (x:A. P(x))  Prop{[k | j]}. Of course, eliding the single level variable from the display of the last theorem gives us our usual

Thm* A:Type, P:(AProp). (x:A. P(x))  Prop

See also Russell's Orders.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html