Functional predicate
In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to object term to produce another object term. Functional predicates are also sometimes called mappings, but that term has other meanings as well. In a model, a function symbol will be modelled by a function.
Specifically, the symbol F in a formal language is a functional symbol 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 functional symbol 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 functional predicate with an ordinary predicate in two variables (or replace a functional predicate in n variables with an ordinary predicate in n + 1 variables), along with a proposition. 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 proposition:
Conversely, given any predicate P satisfying that proposition, you get a functional predicate 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 function symbols but instead use only relation symbols (ordinary predicates); alternatively, one can treat a functional predicate as a special kind of predicate, specifically one that satisfies the proposition above.