# Functional predicate

## From Wikipedia, the free encyclopedia

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.
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 function symbols of more than one variable, analogous to functions of more than one variable; a function symbol 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]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},$

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*].