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

1. \(i\) is a type;
2. If \(t_1 , \ldots ,t_n\) are types then \(\langle t_1 , \ldots ,t_n\rangle /m\) is a type, where \(m\) is a natural number greater than or equal to 1.

An expression of type \(\langle t_1 , \ldots ,t_n\rangle /m\) is a propositional function that takes arguments of types \(t_1 ,\ldots ,t_n\)to a proposition of the order \(N\), where \(N = m +\) the highest order of \(t_1 ,\ldots ,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\).