The idea behind ramified type theory is to introduce a hierarchy of propositions as well. On this view, propositions and propositional functions have an order. If a propositional function is applied to a proposition of a particular order, then it yields a proposition of a higher order. And every function must have a higher order than its arguments. Thus, we avoid the liar paradox by banning a proposition from occurring within itself. If a proposition p occurs within another proposition, as the argument of a function such as x is false, then the resulting proposition is of a higher order than p.