 It turns out that in these theories, we may or may not be able to be fully committed to the principle of \(\beta\)-conversion. Indeed, in some property theories, the full principle of \(\beta\)-conversion leads to paradox, because one can replay a Russell-style argument when the full principle of \(\beta\)-conversion is in place. In such settings, one restricts the formation of \(\lambda\)-formulas by requiring that the body of a \(\lambda\)-term not contain further \(\lambda\)-terms or quantifiers. For further discussion, see (Orilia, 2000).