1

$F$ is a function symbol with arity $2$. Is $F(x,y)=x$ an atomic formula?

My teachers solutions say it is but I thought that atomic formula had to be a predicate name followed by a variable and if a $F$ is a function variable than it is not an atomic formula.

Is it an atomic formula or not? Thanks

M47145
  • 4,106

2 Answers2

4

It is an atomic formula. The atomic formulas include all formulas of the shape $s=t$ where $s$ and $t$ are terms. The terms $s$ and $t$ can be quite complicated. For instance $G(F(x,y))$ is a term, where $x$ and $y$ are variable symbols, $F$ is a binary function symbol, and $G$ is a unary function symbol.

André Nicolas
  • 507,029
  • Thanks for your reply. So just to clarify, all formulas of the shape s=t where s and t are terms, it doesn't matter if there is a function symbol or predicate symbol in front? on a side note, for a term, can you only have a function symbol in front i,e if you have a predicate symbol in front of a term is that not a term? –  Dec 28 '14 at 22:24
  • Predicate symbols with the appropriate terms form formulae, not terms. So if $P$ is a binary predicate symbol, $P(x,y)=z$ or $P(x=y,z)$ are gibberish. Identities between terms and predicates on terms are all the atomic formulae there are. – Malice Vidrine Dec 28 '14 at 22:38
  • So bare with me please ( I really struggle with this). Only function symbols with terms can form terms. And either function symbols or predicate symbols can be applied to terms to form atomic formulae? –  Dec 28 '14 at 22:46
  • reading up on wiki and other sites they all say that an atomic formula or atom is simply a predicate applied to a tuple of terms; that is, an atomic formula is a formula of the form P (t1, …, tn) for P a predicate, and the tk terms. Nothing about function symbols though. –  Dec 28 '14 at 22:56
  • Equality is special in standard first-order logic. But if you want you can think of it as a binary predicate symbol $E$. Then $E(s,t)$ is an atomic formula whenever $s$ and $t$ are terms. Predicate symbols or equality can be used with terms to make an atomic formula. – André Nicolas Dec 28 '14 at 23:16
  • You say that there is nothing about function symbols in the definition of atomic formula. True, but the definition of atomic formula uses the term "term" and certainly function symbols come up in the definition of term. – André Nicolas Dec 28 '14 at 23:20
2

The source of the confusion might be the difference between infix and prefix notation. In some formulations of first-order logic, the official definition of "atomic formula" presupposes prefix notation, where the predicate symbol comes first, followed by its argument(s). In that notation, the formula you asked about would be $=(F(x,y),x)$ or, depending on how eager the author is to avoid parentheses, $=F(x,y)x$ or even $=Fxyx$ (which is unambiguous as long as you know that $=$ and $F$ are binary symbols). For the sake of human readers, people usually adopt some notational conventions, including ones that say you can write binary predicate symbols between their arguments; the resulting expression is regarded as an "abbreviation" of the official formula or an alternative way of writing it. So $F(x,y)=x$ would be an alternative way of writing something like $=Fxyx$ and would therefore count as a formula.

By the way, there is a similar convention for certain function symbols, like $+$, that are usually written between their arguments rather than in front. So if the function symbol $F$ in your example were $+$, you could write $x+y=x$ rather than $+(x,y)=x$.

The reason for such conventions is that prefix notation is more systematic and easier to analyze but people have difficulty reading things like $=+xyx$ and are much happier with $x+y=x$.

Andreas Blass
  • 71,833