Let T be a theory formalized in the classical first order predicate calculus with equality. If P(x) is a formula of T in which one and only one variable of T--here denoted by 'x'--occurs free, and if the following pair of statements are provable in T, then P(x) is said to be a defining formula of T.

(1) "There exists an x such that P(x)" and 
(2) "For any y and any z, P(y) and P(z) imply y=z"-where "y" and "z" denote variables of T.

Now if T were ZFC, for example, consider the formula of T which states "The continuum hypothesis implies that x is the set of all positive integers and the negation of the continuum hypothesis implies that x is the set of all negative integers". This is a defining formula of T and Sierpinski often used formulae of this type to define sets which were "non-effective" in some way. But many might ask whether such definitions are really "legitimate". They arise when the formula P(x) contains sub-formulae which are sentences of T (i.e. closed formulae in which no variables occur free). My question is, to what extent (if any) would such first order theories as Peano's Arithmetic or ZFC be weakened, if their defining formulae were not allowed to contain sub-formulae that are closed?