 By induction on derivations in MSO one easily proves that each theorem of MSO is mapped to some theorem of PFO. Moreover, it is easy to define a “reverse” translation that maps formulas of \(L_{\textrm{PFO}}\) to formulas of \(L_{\textrm{MSO}}\) and to prove that this translation maps theorems of the former to theorems of the latter. This shows that PFO and MSO are equi-interpretable. A similar result can be proved about PFO+ and an extension MSO+ of MSO which allows predicates of (first-level) concepts, provided MSO+ contains an axiom schema to the effect that coextensive concepts are indiscernible.