 (Readers less interested in technical issues may want to skim this section.) Boolos observed that it is possible to interpret monadic second-order logic in the theory  PFO.[9]  Let MSO be some standard axiomatization of (full impredicative) monadic second-order logic in some suitable language \(L_{\textrm{MSO}}\) (Shapiro 1991: ch. 3; Boolos et al. 2002: ch. 22). Boolos first defines a translation \(\Tr'\) that maps any formula of \(L_{\textrm{MSO}}\) to some formula of \(L_{\textrm{PFO}}\). This definition, which proceeds by induction on the complexity of the formulas of \(L_{\textrm{MSO}}\), has as its only non-trivial clauses the following two, which are concerned with the second-order variables: