## Notes to Propositional Function

1. Here is Church's inductive definition of the ramified hierarchy

*i*is a type;- If
*t*_{1}, …,*t*_{n}are types then <*t*_{1}, …,*t*_{n}>/*m*is a type, where*m*is a natural number greater than or equal to 1.

An expression of type
<*t*_{1}, …, *t*_{n}>/*m*
is a propositional function that takes arguments of types
*t*_{1},…, *t*_{n}to a proposition of
the order * N*, where *N* = *m* + the highest
order of *t*_{1},…, *t*_{n} (the order
of *i* is 0). Since
*m* must be at least 1, the order of proposition that
results from applying a propositional function to
*p* must be at least one greater than the order of *p*.