First order logic - why do we need function symbols?

Using function symbols in first order logic forces us to define "terms" inductively, which makes many proofs longer and much more tedious. Of course, function symbols simplify matters when trying to use first order logic to describe things, but on the surface it seems to me they could be replaced completely by relations: Instead of $f$ use a relation $R_f$ such that instead of writing $\varphi(f(x))$ write ($\forall x\exists! y(R(x,y))\wedge R(x,y)\wedge\varphi(y)$. Now use $f(x)$ as a shorthand notation, so you can use it in "real life" but avoid it in proofs.

I guess I'm missing some deep neccecity here, but what?

(The same goes for constant symbols, but they don't really complicate things as function symbols do).

• You can most likely replace functions and constants with predicates, but first order logic is full of notational redundancies that make life easier, such as having both $\exists$ and $\forall$, as well as both $\wedge$ and $\vee$, $\to$, etc. – Elchanan Solomon Mar 29 '12 at 7:45
• That only amplifies the point. Usually in the formal definition of FOL most of these symbols are ommited and used only for notational convenience, and the proofs only deal with the minimal set of symbols required. This is not the case for function symbols. – Gadi A Mar 29 '12 at 7:50
• I think you might get into some syntactic trouble if you don't use terms, i.e. omitting functions really changes the feel of first order logic. – Elchanan Solomon Mar 29 '12 at 7:52
• Isaac, this is my guess as well, but I'd love to see a concrete example. – Gadi A Mar 29 '12 at 7:52
• Fair enough. I suppose a good example would be that your definition of "quantifier free" would be ridiculously convoluted, and quantifier elimination is really important in model theory and first order logic. – Elchanan Solomon Mar 29 '12 at 7:55

You can always take a first-order theory with constants and function symbols and replace it with a theory using only relation symbols. This is at the expense of complicating the theory, since if, for example, $R$ is the relational symbol representing the binary functional symbol $f$, we need an axiom of the form $$( \forall x ) ( \forall y ) ( \exists z ) ( \forall u ) ( R(x,y,u) \leftrightarrow u = z ).$$ But since $R$ and $f$ are definable from one another, there would be a natural translation of theorems of one theory into the other.
Another expense is the statement of certain theorems of model theory. For example, a theory $T$ is said to admit elimination of quantifiers if for every formula $\phi (x_1 , \ldots x_n )$ there is a quantifier-free formula $\psi (x_1 , \ldots x_n )$ such that $$T \vdash (\forall x_1 ) \cdots ( \forall x_n ) ( \phi \leftrightarrow \psi ).$$ The basic example of a theory admitting elimination of quantifiers is the theory of real closed fields. Note that if the underlying language has no constant symbols, then there are no quantifier-free sentences, and therefore no theory without constant symbols can admit elimination of quantifiers. One would have to alter the definition so as to only concern those formulas $\phi$ with at least one free variable. One can show that this would be faithful, but it is also a somewhat less natural definition.
• This is a deficiency in the underlying propositional logic, not a reason to use constants. If your propositional logic is set up correctly, you have perfectly good quantifier-free sentences $\top$ and $\bot$ and you don't need to use silly hacks like $c=c$ and $\neg(c=c)$. – Chris Eagle Mar 29 '12 at 9:38