Higher-Order Propositions

Thm* A,B:Prop. (A  B)  Prop

Here we shall consider various more substantial examples of such "higher-order" propositions. First, observe that the when quantification over propositions and properties (proposition valued functions) is permitted, then the other standard connectives and equality can all be characterized purely in terms of universal quantification and implication:

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

Thm* A  (C:Prop. A  C)
Thm* True  (C:Prop. C  C)
Thm* (A  B)  (C:Prop. ((A  B)  (B  A)  C)  C)

The simplicity of these characterizations leads one to consider simply adopting them as definitions in the first place, and indeed it is not unusual to do so in standard developments of higher-order logic. But we cannot do so because we have constrained ourselves to a so-called "predicative" logic (a term of Bertrand Russell's of uncertain etymology), which requires layering propositions into a hierarchy in a way that precludes us from giving the desired definitions. See Prop Levels and Predicativity.

Here's another example asserting the definability of properties by structural recursion on lists, given base case Q  Prop and step method R  A(A List)PropProp:

Thm* R:(A(A List)PropProp). 
Thm* P:((A List)Prop). 
Thm* (P(nil)  Q) & (a:A, x:A List. P(a.x)  R(a,x,P(x)))

Equality on the type Prop.

Just as Type is a type of Intensional Types, so members of Prop are treated intensionally. One natural alternative would be to identify propositional expressions with their truth-values, which is to identify any two propositions P and Q such that P  Q. At the other extreme, one might identify propositions strictly by their syntactic identity, or perhaps modulo change of bound variables. In Nuprl, the "equality" on Prop is analogous to that on Type. For the most part, propositional expressions are equal when their corresponding constituent expressions are equal in the appropriate types. And of course, like any other Nuprl type, expanding an Operator Definition or rewriting by Computation steps results in an equal expression.

One case of particular note is that (a = b  T) = (a' = b'  T')  Prop just when T = T'  Type, and a = a'  T, and b = b'  T.
Thus, (a  T) = (a'  T')  Prop just when T = T'  Type, and a = a'  T.

See Prop Levels and Predicativity.

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