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?