I watched a series of lectures on the theory of computation, and noticed that in its definition of first-order logic, there was no mention of function symbols.
Are they optional?
I watched a series of lectures on the theory of computation, and noticed that in its definition of first-order logic, there was no mention of function symbols.
Are they optional?
Copyright © 2021 JogjaFile Inc.
You can certainly get away with only using relation symbols. This is because each function is "equivalent," in a precise sense (see below), to its graph $$Graph(f)=\{(a_1,...,a_n, b): f(a_1,..., a_n)=b\}.$$
That said, there are definitely situations where we actually are interested in functions in particular; we can always use the language of relations instead in these cases, but it becomes cumbersome. (And see below for a bit more on this.)
Here's the precise notion of "equivalence" mentioned above (for simplicity, in the case of a language consisting of a single function symbol $f$).
Fix a binary relation symbol $U$ (in general the graph of an $n$-ary function is an $(n+1)$-ary relation). There is now a natural map from $\{f\}$-structures to $\{U\}$-structures $$\mathcal{M}\mapsto\tilde{\mathcal{M}},$$ namely $\tilde{\mathcal{M}}$ has the same underlying set as $\mathcal{M}$ and $U^\tilde{\mathcal{M}}=\{(a,b): \mathcal{M}\models f(a)=b\}$.
This map is an injection. Moreover, there is a single sentence $\varphi$ such that for every $\{U\}$-structure $\mathcal{N}$ we have $\mathcal{N}\models\varphi$ iff $\mathcal{N}=\tilde{\mathcal{M}}$ for some $\{f\}$-structure $\mathcal{M}$. Finally, there is a natural "translation" map from $\{f\}$-formulas to $\{U\}$-formulas, $$\varphi\mapsto \tilde{\varphi},$$ such that $$\varphi^\mathcal{M}=\tilde{\varphi}^\tilde{\mathcal{M}}$$ for every $\{f\}$-structure $\mathcal{M}$. In particular, when $\varphi$ is a sentence we have $$\mathcal{M}\models\varphi\iff\tilde{\mathcal{M}}\models\tilde{\varphi}.$$
Essentially, we can convert from functions to relations in a fully-definable way without losing any information.
OK, now let me mention one somewhat-more-serious drawback with the translation above.
You'll note that I didn't actually define the map $\varphi\mapsto\tilde{\varphi}$. This is because there are a couple natural choices. Basically, sometimes we wind up having to increase the quantifier complexity of the formula in question, but only for stupid reasons; then we have a choice of whether to introduce a "$\forall$" or an "$\exists$."
The reason this happens is that we can compose function symbols. For example, consider the formula $$\varphi(x,y): \quad f(f(x))=y.$$ After relationalization, we need to introduce a new dummy variable to stand for the "intermediate" object $f(x)$. There are a couple choices for how to translate $\varphi$:
In my opinion, the most natural is $$\exists z(U(x,z)\wedge U(z,y)).$$
But we could also use $$\forall z(U(x,z)\rightarrow U(z,y)).$$
The freedom here comes from the fact that $z$ is really not doing anything, but there's no escaping the fact that we need some quantifier to bring it in. And this winds up increasing syntactic complexity, and so model-theoretic properties which are syntax-sensitive - like quantifier elimination - need not be preserved by relationalization.
But the general "modern" view is that these properties aren't really important in and of themselves, but rather by virtue of what other, syntax-independent properties they help us deduce. Since those properties are preserved under relationalization, we don't really lose anything important.