Functional predicate
In formal logic, the term "mapping" is sometimes distinguished from "function" in that a mapping is a logical symbol, whereas a function is a model of such a symbol in set theory. Formally, the symbol F in a formal language is a mapping if, given any symbol X representing an object in the language, F(X) is again a symbol representing an object in that language. In typed logic, F is a mapping with domain type T and codomain type U if, given any symbol X representing an object of type T, F(X) is a symbol representing an object of type U. One can similarly define mappings of more than one variable, analogous to functions of more than one variable. A mapping in zero variables is simply a constant symbol.
Now consider a model of the formal language, with the types T and U modelled by sets [T] and [U] and each symbol X of type T modelled by an element [X] in [T]. Then F can be modelled by the set
- [F] := {([X],[F(X)]) : [X] in [T]},
which is simply a function with domain [T] and codomain [U]. It is a requirement of a consistent model that [F(X)] = [F(Y)] whenever [X] = [Y].
One can replace a mapping with a predicate in two variables (or replace a mapping in n variables with a predicate in n + 1 variables), along with an axiom. Specifically, if F has domain type T and codomain type U, then it can be replaced with a predicate P of type (T,U). Intuitively, P(X,Y) means F(X) = Y. Then whenever F(X) would appear in a statment, you can replace it with a new symbol Y of type U and include another statement P(X,Y).To be able to make the same deductions, you need an additional axiom:
Conversely, given any predicate P satisfying that axiom, you get a defined mapping F, where F(X) is the unique Y such that P(X,Y) holds. For this reason, many treatments of formal logic do not deal explicitly with mappings but instead use only predicates.