This articleneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Function symbol" – news ·newspapers ·books ·scholar ·JSTOR(September 2025) (Learn how and when to remove this message)

Informal systems particularlymathematical logic, afunction symbol is anon-logical symbol which represents afunction ormapping on thedomain of discourse, though, formally, does not need to represent anything at all. Function symbols are a basic component informal languages to formterms. Specifically, if the symbol${\displaystyle F}$ is a function symbol, then given any constant symbol${\displaystyle X}$ representing an object in the language,${\displaystyle F(X)}$ also represents an object in the language. Similarly, if${\displaystyle T}$ is some term in the language,${\displaystyle F(T)}$ is also a term. As such, theinterpretation of a function symbol must be defined over the whole domain of discourse. Function symbols are aprimitive notion, and are therefore not defined in terms of other, more basic concepts.

Intyped logic,F is a functional symbol withdomain typeT andcodomain typeU if, given any symbolX representing an object of typeT,F(X) is a symbol representing an object of typeU.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 typesT andU modelled bysets [T] and [U] and each symbolX of typeT modelled by an element [X] in [T].ThenF can be modelled by the set

${\displaystyle [F]:=\{([X],[F(X)]):[X]\in [\mathbf{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].

In a treatment ofpredicate logic that allows one to introduce new predicate symbols, one will also want to be able to introduce new function symbols. Given the function symbolsF andG, one can introduce a new function symbolF ∘G, thecomposition ofF andG, satisfying (F ∘G)(X) =F(G(X)),for allX.Of course, the right side of this equation doesn't make sense in typed logic unless the domain type ofF matches the codomain type ofG, so this is required for the composition to be defined.

One also gets certain function symbols automatically.In untyped logic, there is anidentity predicate id that satisfies id(X) =X for allX.In typed logic, given any typeT, there is an identity predicate id_T with domain and codomain typeT; it satisfies id_T(X) =X for allX of typeT.Similarly, ifT is asubtype ofU, then there is an inclusion predicate of domain typeT and codomain typeU that satisfies the same equation; there are additional function symbols associated with other ways of constructing new types out of old ones.

Additionally, one can define functional predicates after proving an appropriatetheorem.(If you're working in aformal system that doesn't allow you to introduce new symbols after proving theorems, then you will have to use relation symbols to get around this, as in the next section.)Specifically, if you can prove that for everyX (or everyX of a certain type),there exists auniqueY satisfying some conditionP, then you can introduce a function symbolF to indicate this. This is called anextension by definition. Note thatP will itself be a relationalpredicate involving bothX andY.So if there is such a predicateP and a theorem:

For allX of typeT, for some uniqueY of typeU,P(X,Y),

then you can introduce a function symbolF of domain typeT and codomain typeU that satisfies:

For allX of typeT, for allY of typeU,P(X,Y)if and only ifY =F(X).

Many treatments of predicate logic don't allow functional predicates, only relationalpredicates.This is useful, for example, in the context of provingmetalogical theorems (such asGödel's incompleteness theorems), where one doesn't want to allow the introduction of new functional symbols (nor any other new symbols, for that matter).But there is a method of replacing functional symbols with relational symbols wherever the former may occur; furthermore, this is algorithmic and thus suitable for applying most metalogical theorems to the result.

Specifically, ifF has domain typeT andcodomain typeU, then it can be replaced with a predicateP of type (T,U).Intuitively,P(X,Y) meansF(X) =Y.Then wheneverF(X) would appear in a statement, you can replace it with a new symbolY of typeU and include another statementP(X,Y).To be able to make the same deductions, you need an additional proposition:

For allX of typeT, for someuniqueY of typeU,P(X,Y).

(Of course, this is the same proposition that had to be proven as a theorem before introducing a new function symbol in the previous section.)

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 aspecial kind of predicate, specifically one that satisfies the proposition above.This may seem to be a problem if you wish to specify a propositionschema that applies only to functional predicatesF; how do you know ahead of time whether it satisfies that condition?To get an equivalent formulation of the schema, first replace anything of the formF(X) with a new variableY.Thenuniversally quantify over eachY immediately after the correspondingX is introduced (that is, afterX is quantified over, or at the beginning of the statement ifX is free), and guard the quantification withP(X,Y).Finally, make the entire statement amaterial consequence of the uniqueness condition for a functional predicate above.

Let us take as an example theaxiom schema of replacement inZermelo–Fraenkel set theory.(This example usesmathematical symbols.)This schema states (in one form), for any functional predicateF in one variable:

${\displaystyle \mathrm{\forall }A,\mathrm{\exists }B,\mathrm{\forall }C,C\in A\to F(C)\in B.}$

First, we must replaceF(C) with some other variableD:

${\displaystyle \mathrm{\forall }A,\mathrm{\exists }B,\mathrm{\forall }C,C\in A\to D\in B.}$

Of course, this statement isn't correct;D must be quantified over just afterC:

${\displaystyle \mathrm{\forall }A,\mathrm{\exists }B,\mathrm{\forall }C,\mathrm{\forall }D,C\in A\to D\in B.}$

We still must introduceP to guard this quantification:

${\displaystyle \mathrm{\forall }A,\mathrm{\exists }B,\mathrm{\forall }C,\mathrm{\forall }D,P(C,D)\to (C\in A\to D\in B).}$

This is almost correct, but it applies to too many predicates; what we actually want is:

${\displaystyle (\mathrm{\forall }X,\mathrm{\exists }!Y,P(X,Y))\to (\mathrm{\forall }A,\mathrm{\exists }B,\mathrm{\forall }C,\mathrm{\forall }D,P(C,D)\to (C\in A\to D\in B)).}$

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. Alternatively, one may interpret the original statement as a statement in such a formal language; it was merely an abbreviation for the statement produced at the end.

Anuninterpreted function^[1] is one that has no other property than its name andn-ary form. The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus afree object, or the empty theory, being thetheory having an empty set ofsentences (in analogy to aninitial algebra). Theories with a non-empty set of equations are known asequational theories. Thesatisfiability problem for free theories is solved bysyntactic unification; algorithms for the latter are used by interpreters for various computer languages, such asProlog. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, seeUnification (computer science).

As an example of uninterpreted functions forSMT-LIB, if this input is given to anSMT solver:

(declare-fun f (Int) Int)(assert (= (f 10) 1))

the SMT solver would return "This input is satisfiable". That happens becausef is an uninterpreted function (i.e., all that is known aboutf is itssignature), so it is possible thatf(10) = 1. But by applying the input below:

(declare-fun f (Int) Int)(assert (= (f 10) 1))(assert (= (f 10) 42))

the SMT solver would return "This input is unsatisfiable". That happens becausef, being a function, can never return different values for the same input.

Thedecision problem for free theories is particularly important, because many theories can be reduced by it.^[2]

Free theories can be solved by searching forcommon subexpressions to form thecongruence closure.^{[clarification needed]} Solvers includesatisfiability modulo theories solvers.

• Algebraic data type
• Initial algebra
• Logical connective
• Logical constant
• Term algebra
• Theory of pure equality

• Model theory

• Articles with short description
• Short description is different from Wikidata
• Articles needing additional references from September 2025
• All articles needing additional references
• Wikipedia articles needing clarification from May 2014