Some FOL systems are equipped with function symbols, while some are not. Since function symbols apply to terms without restriction, terms like "father(Adam)" are well accepted, where Adam is the first man in the world. This causes a problem: objects to terms do not always exist. Then my guess is that, in FOL systems with function symbols, we better prove something like $\exists x, x = f(s_0)$, or even $\exists!x, x = f\left(s_{0}\right)$, or at least, we have to specify a range where function terms exist, e.g., we need such formulae: $\forall x \in \mathcal{S}, \exists!t, t = f(x)$ to be clear. Otherwise, we can't tell if a function term exists or not, although we can talk about it.
My concern is, maybe, a system without function terms is more concise, as compared to a system with function symbols. For instance, we can introduce a predicate "Father", such that $Father(x,y)$ asserts that "x is the father of y". Then as we talk about "Something happens to Father of a" in the form of $Something(Father(a))$, we can happily replace it by $\forall x, Father(x,a) \rightarrow Something(x)$. In my understanding, we can replace every function symbol with a predicate symbol, so that the logical system is of only constants as terms. This will lead to a system where each object is represented by a single constant symbol (exists or not), which in my feel, clean and precise.
These are only my feels as an amateur as I think about logic and math. Let me know if this thinking makes sense.
I just thought about the difference between having functions or not. It seems to me that the introduction of functions and terms into FOL reflects a trade-off between elegance and convenience. Indeed, a system with only predicates and constant symbols is cleaner and reflects perfectly the concept of objects in a logical system. Nevertheless, the problem is that the system is going to verbose, as compared to a system which allows function symbols. Using the case above, it is obvious that $\textrm{Something}\left(\textrm{Father}\left(a\right)\right)$ is shorter than $\forall x, Father(x,a) \rightarrow Something(x)$. In fact, as we introduce the function $f$ into the axioms of an FOL system, we have implicitly introduced a predicate $F$ that defines $f$: \begin{equation} \forall x \in \mathcal{S}, F\left(x,f\left(x\right)\right). \end{equation} That is to say, functions and predicates always come in pairs. Actually, we can always introduce constant symbols in reasoning from function terms. For instance, the formula \begin{equation} \forall x \in \mathcal{S}, P\left(f\left(x\right)\right) \end{equation} is equivalent to \begin{equation} \forall x \in \mathcal{S}, \forall y, y = f\left(x\right) \rightarrow P\left(y\right). \end{equation} Suppose we are looking at an object $x_{0} \in \mathcal{S}$ in a subproof. Then naturally, we have \begin{equation} \forall y, y = f\left(x_{0}\right) \rightarrow P\left(y\right). \end{equation} Suppose that $y_{0} = f\left(x_{0}\right)$ in a subproof (i.e., from existential introduction). Then we have $P\left(y_{0}\right)$, and the following reasoning may proceed with the object $y_{0}$.
To conclude, functions can be seen as an intermediate product that connects objects (constant symbols) and formulae, and the purpose of having them is to make formulae shorter in an FOL system. In fact, predicates are also introduced for such a purpose, i.e., the introduction of "=" in mathematical FOL. In set theory, equality of two sets, the symbol "=", is defined by the following formula:
\begin{equation} \forall x, \forall y, x = y \leftrightarrow \forall z, z \in x \leftrightarrow z \in y. \end{equation}
We can see that without the definition of $=$, mathematical reasoning will be very long and tedious. Again, the closer the bottom level of system is approached, the more verbose the language is. So, is math equipped with the beauty of brevity? The answer depends on at which level you are thinking about math.
In fact, the above thinking does not only apply to logic and math. Think about the relation between high-level programming language, i.e., C++ and Java, and the assembly language, or even machine language. High-level languages abstract formidably long description, at the cost of precision (This is indeed the case, as how an operation is conducted using adders, multipliers and registers is sealed in a black box), but with the benefit of brevity.
