Notes to Propositional Function

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

  1. i is a type;
  2. 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.

Copyright © 2011 by
Edwin Mares <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free