In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term.
Functional predicates are also sometimes called mappings, but that term has additional meanings in mathematics.
Specifically, if you can prove that for every X (or every X of a certain type), there exists a unique Y satisfying some condition P, then you can introduce a function symbol F to indicate this.
Because the elimination of functional predicates is both convenient for some purposes and possible, many treatments of formal logic do not deal explicitly with function symbols but instead use only relation symbols; another way to think of this is that a functional predicate is a special kind of predicate, specifically one that satisfies the proposition above.
This may seem to be a problem if you wish to specify a proposition schema that applies only to functional predicates F; how do you know ahead of time whether it satisfies that condition?
Finally, make the entire statement a material consequence of the uniqueness condition for a functional predicate above.
This schema states (in one form), for any functional predicate F in one variable: First, we must replace F(C) with some other variable D: Of course, this statement isn't correct; D must be quantified over just after C: We still must introduce P to guard this quantification: This is almost correct, but it applies to too many predicates; what we actually want is: This version of the axiom schema of replacement is now suitable for use in a formal language that doesn't allow the introduction of new function symbols.