Thus instead of iterating reflection principles that are formulated entirely in the language of arithmetic, one can add by iteration new truth predicates and correspondingly new axioms for the new truth predicates. Thereby one might hope to make explicit all the assumptions that are implicit in the acceptance of a theory like PA. The resulting theory is called the reflective closure of the initial theory. Feferman (1991) has proposed the use of a single truth predicate and a single theory (KF), rather than a hierarchy of predicates and theories, in order to explicate the reflective closure of PA and other theories. (KF is discussed further in Section 4.4 below.)