Many have observed, though, that it is not obvious in just what sense the induction principle, replacement, and so on, are "second-order principles". For, in their natural formulations in ordinary mathematical English

Whenever P is a well-defined determinate property of naturals, if it holds of 0, and whenever it holds of n, of n + 1 also, it holds of all naturals.they involve a notion, of a property being "well-defined" and "determinate", that has no apparent mathematical definition. So, we may say they are faithfully captured by their second-order formulations if we stipulate the higher-order quntifiers range over "well-defined and determinate" properties (and relations, functions and so on). But since this is not a mathematical notion we have achieved nothing, and it is not at all obvious what these principles so formulated have to do with their second-order formulations on the more usual set-theoretic semantics, at least in so far as the epistemological use we make of them is concerned. Perhaps more natural approach is to regard these principles not as formal principles at all, but as informal principles that have, strictly speaking, no definite set of consequences, that are not necessarily captured by any formalisation at all, but rather have an indefinite range of mathematical applications we regard as correct. This range is indefinite, since we can't beforehand restrict the totality of properties we recognise as determinate and well-defined to any mathematically defined definite totality -- it is dependent on our decisions on what properties we regard as determinate and well-defined, and there is no reason to think that there must always be some matter of fact on which such decisions turn. (And even if there are in fact always such matters of fact, and some determined totality of properties that are, in some idealised sense, recognisable by us as determined and well-defined, for Gödelian reasons we can never recognise this totality as such.)

Whenever R is a well-defined determinate functional binary relation between sets, for any set A, the image of A, i.e. the set {y | (Ex in A) R(x,y)}, exists.

So, disregarding the notion the "informal" induction principle or replacement are "second-order principles", we may describe the resulting picture in the following not very precise terms. Whenever, for whatever reason, we recognise some language defined with mathematical precision, a formal language, as meaningful, so that formulas in the language define well-defined and determinate properties, and sentences meaningful statements that are either true or false as a matter of mathematics, we get, from the "informal" principles, a principle of mathematical precision, by restricting "well-defined and determinate property" in these "informal" principles to range over properties definable in the formal language. Of course, the resulting mathematical principle does not cover all the applications of the informal principle recognisable by us as valid, since, given we recognise the formal language as meaningful, we must surely recognise the notion of a sentence in the language being true, and a formula being true of given objects, as determinate and well-defined (on the picture painted here, we regard this observation not as something to be argued for, but as a triviality, since it is not obvious what sort of meaningfuless of a formal language would license the conclusion of the applicability of the induction principle for the language that did not involve accepting the determinateness and well-definedness of the formal language); but, by well-known results in mathematical logic, these notions are not expressible in the formal language itself.

So far, so standard. There is, however, a small glitch in our development. Recall the replacement schema as formalised in ZFC

(*) (x)(E!y)R(x,y) implies (x)(Ey)(z)(z in y iff (Ew in x)R(x,z))On the face of it, it's easy to see every instance of the scheme is true given the informal replacement principle and the meaningfulness of the language of set theory. Alas, the instances of the schema (*) are in fact universal closures of sentence obtained by replacing R with formulas possibly with more free variables than just two. That is, they have in fact the form

(*') (a1)(a2) ... (an)(x)(E!y)R(x,y,a1, ..., an) implies (x)(Ey)(z)(z in y iff (Ew in x)R(x,z, a1, ..., an))The same of course applies to the induction schema, its instances, and their justification given the informal induction principle (except that the language of arithmetic has a name for every natural, so in so far as we're dealing with naturals only the problem has a rather trivial solution, using substitutional quantification). The problem here is that a formula R(x,y, z1, ..., zn) in the language of set theory does not define a well-defined determinate functional binary relation of sets -- it does not define a binary relation at all. We need some further argument to justify the truth of (*') given the informal replacement principle and the meaningfulness of the language of set theory. One would be to argue that the language of set theory augmented with a constant for every set is meaningful, and formulas in it express properties. For this language, there is no difference between schemas (*) and (*'). Alas, if we go this way, we must explain what it means for a language the size of a proper class to be meaningful, why we should recognise the extended language of set theory as such given the usual conception of the world of sets (the cumulative hierarchy, sets as arbitrary extensional collections, and so on), why the meanigfulness of such language guarantees that all formulas define determinate well-defined properties (are there a proper class of properties?), and so on and so forth. Fortunately, we may shift the burden directly to the informal principles themselves, so we get

Whenever P is a well-defined determinate m-ary relation between a natural and j = m-1 objecs of any sort, if given some objects a1, ..., aj if it holds of 0 and a1, ..., aj, and whenever it holds of n and a1, ..., aj, of n + 1 and a1, ..., aj also, it holds of every natural n and a1, ..., aj.These principles are just as evident (on the relevant mathematical picture) as the originals, and have the nice property that they in fact directly yield the corresponding formal schemata. (We have used the notion of natural in the formulation of the induction principle, in referring to relations of arbitrary arity. This is not in itself worrying, since there is no pretence that the induction principle serves in a definition of what a natural is in any non-circular sense. Rather, it functions as a part of explanation or explication of this notion, and in our conceptual and philosophical analysis of the justification of various mathematical principles. Such an analysis need not in any way justify the correctness of that justification, or refrain from making use of concepts justified or explained by what is under analysis.)

Whenever R is a well-defined determinate functional 2+n-ary relation between two sets and n objects a1, ..., an, given any objects a1, ..., an, for any set A, the image of A under R(x, y, a1, ..., an), i.e. the set {y | (Ex in A) R(x, y, a1, ..., an)}, exists.