Notes to Propositional Function
1. Here is Church's inductive definition of the ramified hierarchy
- i is a type;
- If t1, …, tn are types then <t1, …, tn>/m is a type, where m is a natural number greater than or equal to 1.
An expression of type <t1, …, tn>/m is a propositional function that takes arguments of types t1,…, tnto a proposition of the order N, where N = m + the highest order of t1,…, tn (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.