Functional predicate
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 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 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
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].
Introducing new function symbols from old function symbols is easy; given function symbols F and G, there is a new function symbol F o G, the composition of F and G, satisfying (F o G)(X) = F(G(X)), for all X.
Of course, the right side of this equation doesn't make sense in typed logic unless the domain type of F matches the codomain type of G, so this is required for the composition to be defined.
One also gets certain function symbols automatically.
In untyped logic, there is an identity predicate id that satisfies id(X) = X for all X.
In typed logic, given any type T, there is an identity predicate idT with domain and codomain type T; it satisfies idT(X) = X for all X of type T.
Similarly, if T is a subtype
of U, then there is an inclusion predicate of domain type T and codomain type U 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 appropriate theorem
.
(If you're working in a formal 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 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.
Note that P will itself be a relational predicate involving both X and Y.
So if there is such a predicate P and a theorem:
then you can introduce a function symbol F of domain type T and codomain type U that satisfies:
This is useful, for example, in the context of proving metalogic
al theorems (such as Gö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, 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 statement, 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:
(Of course, this is the same proposition that had to be proved 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 a special kind of predicate, specifically one that satisfies the proposition above.
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?
To get an equivalent formulation of the schema, first replace anything of the form F(X) with a new variable Y.
Then universally quantify over each Y immediately after the corresponding X is introduced (that is, after X is quantified over, or at the beginning of the statement if X is free), and guard the quantification with P(X,Y).
Finally, make the entire statement a material consequence of the uniqueness condition for a functional predicate above.
Let us take as an example the axiom schema of replacement
in Zermelo-Fraenkel set theory.
(This example uses mathematical symbols.)
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. 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.
Formal logic
Classical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
and related branches of mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, 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 other meanings as well.
In a model, a function symbol will be modelled by a function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
.
Specifically, the symbol F in a formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
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
0 (number)
0 is both a numberand the numerical digit used to represent that number in numerals.It fulfills a central role in mathematics as the additive identity of the integers, real numbers, and many other algebraic structures. As a digit, 0 is used as a placeholder in place value systems...
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
which is simply a function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
with domain [T] and codomain [U].
It is a requirement of a consistent model that [F(X)] = [F(Y)] whenever [X] = [Y].
Introducing new function symbols
In a treatment of predicate logic that allows one to introduce new predicate symbols, one will also want to be able to introduce new function symbols.Introducing new function symbols from old function symbols is easy; given function symbols F and G, there is a new function symbol F o G, the composition of F and G, satisfying (F o G)(X) = F(G(X)), for all X.
Of course, the right side of this equation doesn't make sense in typed logic unless the domain type of F matches the codomain type of G, so this is required for the composition to be defined.
One also gets certain function symbols automatically.
In untyped logic, there is an identity predicate id that satisfies id(X) = X for all X.
In typed logic, given any type T, there is an identity predicate idT with domain and codomain type T; it satisfies idT(X) = X for all X of type T.
Similarly, if T is a subtype
Subtype
In programming language theory, subtyping or subtype polymorphism is a form of type polymorphism in which a subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program constructs, typically subroutines or functions, written to operate on...
of U, then there is an inclusion predicate of domain type T and codomain type U 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 appropriate theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
.
(If you're working in a formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
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 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.
Note that P will itself be a relational predicate involving both X and Y.
So if there is such a predicate P and a theorem:
- For all X of type T, for some unique Y of type U, P(X,Y),
then you can introduce a function symbol F of domain type T and codomain type U that satisfies:
- For all X of type T, for all Y of type U, P(X,Y) if and only ifIf and only ifIn logic and related fields such as mathematics and philosophy, if and only if is a biconditional logical connective between statements....
Y = F(X).
Doing without functional predicates
Many treatments of predicate logic don't allow functional predicates, only relational predicates.This is useful, for example, in the context of proving metalogic
Metalogic
Metalogic is the study of the metatheory of logic. While logic is the study of the manner in which logical systems can be used to decide the correctness of arguments, metalogic studies the properties of the logical systems themselves...
al theorems (such as Gö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, if F has domain type T and codomain
Codomain
In mathematics, the codomain or target set of a function is the set into which all of the output of the function is constrained to fall. It is the set in the notation...
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 statement, 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:
- For all X of type T, for some unique Y of type U, P(X,Y).
(Of course, this is the same proposition that had to be proved 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 a special kind of predicate, specifically one that satisfies the proposition above.
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?
To get an equivalent formulation of the schema, first replace anything of the form F(X) with a new variable Y.
Then universally quantify over each Y immediately after the corresponding X is introduced (that is, after X is quantified over, or at the beginning of the statement if X is free), and guard the quantification with P(X,Y).
Finally, make the entire statement a material consequence of the uniqueness condition for a functional predicate above.
Let us take as an example the axiom schema of replacement
Axiom schema of replacement
In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory that asserts that the image of any set under any definable mapping is also a set...
in Zermelo-Fraenkel set theory.
(This example uses mathematical symbols.)
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. 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.