Notes to Propositional Function

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

1. i is a type;
2. If t₁, …, t_n are types then <t₁, …, t_n>/m is a type, where m is a natural number greater than or equal to 1.

An expression of type <t₁, …, t_n>/m is a propositional function that takes arguments of types t₁,…, t_nto a proposition of the order N, where N = m + the highest order of t₁,…, 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.