Functional predicate
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.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.