 Alternative simpler formulations, which retain only the notion of classes, classes of classes, etc., were formulated by Gödel and Tarski. Actually this simpler version was used by Gödel in his 1931 paper on formally undecidable propositions. The discovery of the undecidable propositions may have been motivated by a heuristic argument that it is unlikely that one can extend the completeness theorem of first-order logic to type theory (see the end of his Lecture at Königsberg 1930 in Gödel Collected Work, Volume III, Awodey and Carus 2001 and Goldfarb 2005).  Tarski had a version of the definability theorem expressed in type theory (see Hodges 2008). See Schiemer and Reck 2013. 