 where \(\phi(x)\) is any formula (in which \(x\) may or may not be free) that does not contain any second-order quantifiers, but possibly free second-order variables. In T(PA), quantification over sets can be defined as quantification over formulas with one free variable and membership as the truth of the formula as applied to a number. 