  For forming propositions we use this type structure: thus \(R(a_1 ,\ldots ,a_n)\) is a proposition if \(R\) is of type \((A_1 ,\ldots ,A_n)\) and \(a_i\) is of type \(A_i\) for \(i = 1,\ldots ,n\). This restriction makes it impossible to form a proposition of the form \(P(P)\): the type of \(P\) should be of the form \((A)\), and \(P\) can only be applied to arguments of type \(A\), and thus cannot be applied to itself since \(A\) is not the same as \((A)\).