Editing Functional predicate (section)

==Doing without functional predicates==
Many treatments of predicate logic don't allow functional predicates, only relational [[predicate (logic)|predicate]]s.
This is useful, for example, in the context of proving [[metalogic]]al theorems (such as [[Gödel's incompleteness theorem]]s), 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:
: [[For all]] ''X'' of type '''T''', for some [[unique (mathematics)|unique]] ''Y'' of type '''U''', ''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 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 (logic)|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 conditional|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:
:<math>\forall A, \exists B, \forall C, C \in A \rightarrow F(C)\in B.</math> 
First, we must replace ''F''(''C'') with some other variable ''D'': 
:<math>\forall A, \exists B, \forall C, C \in A\rightarrow D \in B.</math> 
Of course, this statement isn't correct; ''D'' must be quantified over just after ''C'': 
:<math>\forall A, \exists B, \forall C, \forall D, C \in A \rightarrow D\in B.</math> 
We still must introduce ''P'' to guard this quantification: 
:<math>\forall A, \exists B, \forall C, \forall D, P(C,D) \rightarrow (C \in A \rightarrow D \in B).</math> 
This is almost correct, but it applies to too many predicates; what we actually want is: 
:<math>(\forall X, \exists ! Y, P(X,Y))\rightarrow (\forall A, \exists B, \forall C, \forall D, P(C,D)\rightarrow (C \in A \rightarrow D \in B)).</math> 
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.