What is the difference between a function and a predicate in this specific case?

Question

∀ x,y. Foo(x) ⇒ (Bar(x,y) = Bar(x,x))

I can't quite understand if Foo is a function or a predicate, nor if Bar is a question or a predicate. Could you please help me out?

And in that case, what about?

∀ x,y. (Foo(x) = Foo(y)) ⇒(Bar(x,y) = Bar(x,x))

Answer 1

Whether someting is a function or a predicate symbol can be determined by how it combines with the rest of the formula.

In particular, what matters is the difference between terms and formulas.

Terms stand for objects (such as numbers), and either occur as arguments to functions and predicates or one side of an equality. $=$ only goes between terms, not formulas.

Formulas stand for propositions that can be either true or false and are composed of predicate symbols applied to arguments which are terms, and these formulas can in turn be combined with each other trough logical conenctives ($\neg, \land, \to$, etc.). Logical connectives can only occur between formulas, not terms.

Function symbols are symbols that take one or more terms (= symbols that stand for objects) and produce another term (= something that stands for an object). For example, $successsor$ could be a function symbol that takes a term $x$ and produces another term $successor(x)$ which stands for the number that is the successor of the object denoted by $x$. Or $sum$ could be a function symbol that takes two terms $x,y$ and produces another term $sum(x,y)$ which stands for the number that is the sum of $x$ and $y$. We can then express the identity of objects (e.g. numbers) with $=$ by saying things like $sum(0,1) = successor(0)$, where $successor(0)$ and $sum(0,1)$ both must be terms which are interpreted as objects, here the numbers $1$ and $1$, respecively.

Predicate symbols are symbols that take one or more terms and produce a formula (= something that can be true or false). For example, $even$ could be a predicate symbol that takes a term $x$ and produces a truth value depending on whether or not $x$ is an even number. Or $greaterthan$ could be a predicate symbol that takes two terms $x,y$ and produces a truth value depending on whether or not $x$ is greater than $y$. We can then combine these formulas to new formulas with a truth value and say things like $even(1) \land greaterthan(2,1)$, which is s false in this case.

---

In your first example:
Since $Foo(x)$ goes with a logical connective ($Foo(x) \to ...)$, $Foo(x)$ must be a formula (something that has a truth value) so $Foo$ must be a predicate symbol that takes a term and produces a formula.
$Bar(x,y)$ and $Bar(x,x)$ are compared with the equality sign ($Bar(x,y) = Bar(x,x)$) so they must be terms (= something that stands for an object), hence $Bar$ must be a function symbol that takes two terms and produces another term.

In your second example, $Foo(x)$ goes with an equality sign ($Foo(x) = Foo(y)$) so $Foo(x)$ and $Foo(y)$ must be terms so $Foo$ must be a function symbol like $Bar$.

Answer 2

There are certain rules that an expression in predicate logic has to follow in order to be well-formed. Amongst these are:

• Equality ($=$) only binds terms.

• Connectives ($\vee,\wedge,\neg,\implies,\iff$) only bind formulas.

As such, as soon as I see something like "$p=q$" I know that both $p$ and $q$ have to be terms (or the expression is ill-formed). So, for example, in the first example we know that:

• $Foo(x)$ has to be a formula.

• $Bar(x,y)$ and $Bar(x,x)$ have to be terms.

At this point we look at how terms and formulas are built up, and it's clear that (in this case) $Foo$ must be a unary predicate symbol and $Bar$ must be a binary function symbol.

(One useful thing to keep in mind is that we can't "go back" from formulas to terms: if $t$ is a term, no predicate/relation symbol can occur in $t$. Similarly, an atomic formula will always have the form "$R(t_1,...,t_n)$" for some relation symbol $R$ and some terms $t_1,...,t_n$ - or the form "$t_1=t_2$," if you want to treat $=$ separately.)

---

Of course, as often happens with these issues, this is a point we can avoid by being clearer. Most presentations of first-order logic use separate alphabets for function and relation symbols, so that there can be no possible confusion: in such a system there is no symbol that in one context can be a function symbol and in another can be a relation symbol. So while this is worth understanding, it's also not something you should ever actually run into.