When dealing with functions outside of formal languages, the concept of 'function' and of 'binary relation' are such that the set of all functions is a subset of binary relations.

For example using infix notation we might specify the application of a function $¬$ on $x$ and $y$ as $x¬y$, however we might also treat $¬$ as a binary relation on $z$ and $w$, and have $z¬w$ as a sentence that asserts that $z$ and $w$ are related by the mapping $¬$.

It's slightly ambiguous, however context usually solves this problem.

In FOL we use notations like this to discuss mathematical concepts such as the formula $x+1=2$ where we have both a relation and a function taking two arguments.

In FOL we must know to interpret $x+1$ as a term and $x+1=2$ as a formula in order to make statements such as $P(x)=(x+1=2)$ is true for $x=1$. For example if we treat $x+1=2$ as a term then $=$ is an operator taking two arguments $(x+1)$ and $2$ and yielding another object as opposed to making a formula.

Is it that in FOL we make a clear distinction between a relation and a function (for example a function cannot be a relation) or that whether we treat a formula of the form $x¬y$ as a term or formula depends on the interpretation/model we are working in?

  • $\begingroup$ Not clear... $\neg$ is not a function nor a relation symbol in FOL. $x \neg y$ is not well-formed. $\endgroup$ Feb 25, 2023 at 0:16
  • $\begingroup$ Also note that an $n$-ary function is an $n+1$-ary relation. So if you have a binary function like $+$ the corresponding relation is ternary. $\endgroup$ Feb 25, 2023 at 0:18
  • $\begingroup$ $=$ is typically treated as a built-in (logical) symbol, though it can also be defined as a binary relation symbol. $\endgroup$ Feb 25, 2023 at 0:36
  • $\begingroup$ @lemontree the distinction between the arity is true, but equally you could be trying to apply a 1-ary function to an ordered pair, it does not help us intepret it any better except in a textbook where we know they wouldn't be doing anything blatantly wrong. $\endgroup$
    – Confused
    Feb 26, 2023 at 11:47
  • $\begingroup$ "you could be trying to apply a 1-ary function to an ordered pair" No, not in FOL. Function arguments are limited strictly to individuals of the domain. $\endgroup$ Feb 26, 2023 at 14:31

1 Answer 1


A signature for first order logic will normally both have function symbols and relation symbols. For example, the signature $\Sigma_{PA}$ for Peano comes with function symbols $0,S,+,\cdot$ and normally without relation symbols, while the signature $\Sigma_{ZFC}$ for formal material set theory comes with a single relation symbol $\in $ and no function symbols. Relations and functions symbols are at this level disctinct concepts, though once we add the logic to our language and once we start talking about semantic, there start to appear connections between $n$-airy function symbols and $n+1$-airy predicates $\phi(\underline x,y)$ which are functional. The relations appear both in syntax and semantic. I will write some down.

  • The classical model theory of first order logic usually takes place in the framework of ZFC. One chooses a carrier set $M$ for a model, and then functions and relations to model the symbols of the signature. The problem is that material set theory itself (informal and formal) has no primitive concept of what a function is. They got Occam's razored away and have been replaced by functional relations. You may find some justification for that step in the next bullet point about syntax. Hence, when we do model theory of first-order logic in the framework of a material set theory, then the semantic of a function symbol will always be a relation $\phi(\underline x,y)$ such that $\forall \underline x\,\exists !y\, \phi(\underline x,y)$ is true in the meta-theory. As I have said before, this is simply because in the meta-theory functions are a derived and not a primitive concept. I want to stress that in ordinary mathematics many people use function as a primitive concept (or more precisely: most mathematicians don't about such stuff), and there are foundations which take functions as the primitive concept, and containment (Lawvere's elementary theory of the category of sets comes to mind).

  • Functional relations and function symbols are also related in a purely syntactical way. There is a result that states that if you work within a theory $T$ with a signature $\Sigma$ and you have a predicate $\phi(\underline x,y)$ for which the theory $T$ shows that it is functional $$T\vdash \forall \underline x\, \exists ! y\, \phi(\underline x,y)$$ then you may add a new function symbol $f$ to your signature $\Sigma$ and a new axiom $$\forall \underline x\, \forall y\, (f(\underline x) = y \leftrightarrow \phi(\underline x,y))$$ to your theory to get a new theory $T'$ relative to the signature $\Sigma' = \Sigma \sqcup \{f\}$. Note that every statement in the language $L$ of $\Sigma$ is automatically a sentence in the richer language $L'$ of $\Sigma'$, and the theorem states that using the richer language is a conservative extension of the old one. In other words, if $\phi$ is a sentence in the old language and $T'\vdash \phi$, then already $T\vdash \phi$. Not more sentences of the old language become true. Additionally, there is a mechanical procedure the produce mentions of the new function symbol from sentences in $L'$ which is provability preserving and reflecting (you kind of mention this procedure in your second paragraph). There is a way to associate to each sentence $\psi$ in $L'$ a senctence $\overline \psi$ in the old language such that $T'\vdash \psi$ if and only if $T\vdash \overline \psi$. This is the sense in which new theory is not only a conservative extension of the old one (i.e. it does not say anything new about the stuff that $L$ can already speak about), it also does not add anything new about which $L$ can not speak. Btw, the categorical logicians way of expressing that $T$ and $T'$ are essentially the same theory is: the syntactic categories $\mathcal C_T$ and $\mathcal C_{T'}$ are equivalent.

The last syntactic fact explains why you can in principle work without function symbols. We could for example replace each function symbol in Peano Arithmetic by a (+1 ary) relation symbol, add to the axioms of PA that the relation symbols are functional, and formulate all the axioms in the new style, and we would get (up to a mechanical translation process) essentially the same theory.

Reference: Elliott Mendelson, Introduction to Mathematical Logic, chapter 2.9


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .