Thanks again for pointing out ambiguities and lacks of clarity in the lecture material!

In the lab course today, we were discussing

**atoms** vs.

**atomic formulas** in FOL.

Usually, atoms and atomic formulas are used equivalently in FOL to denote formulas that contain no logical connectives and quantifiers, or equivalently, formulas that do not contain any strict subformulas. Atoms (atomic formulas) are the simplest well-formed formulas in FOL.

For example, consider the following (composite) formula:

∀x. P (x) ∧ ∃y. Q (y, f (x)) ∨ ∃z. R (z)

where x,y,z denote variables, f denotes a function symbol, and P, Q, R denote predicates.

The atoms (atomic formulas) contained in this formula are:

In the lecture slides, we only gave a brief summary for the definition of FOL based on examples. For an extensive definition of FOL, please refer to [1].

Thus, whenever we are talking about atoms, as e.g. when we were talking about rules, we refer to atomic formulas.

Then there was the question, **whether a function like e.g. mother(x) is an atom/atomic formula**?

The definition of an **FOL formula** says:

- If P is a predicate symbol of arity k, and if t
_{1},...,t_{k}, are terms, then P(t_{1},...,t_{k}) is a formula.
- (
**Negation**) For all formulas F, also ¬F is a formula
- (
**Binary** Connectives) For all Formulas F,G, also F∧G,F∨G,F→ G,F↔G are formulas
- (
**Quantifiers**) If x is a variable and F is a formula, then also ∀x.F and ∃x.F are formulas

A function alone is only considered a **term**, following the definition of an **FOL term**:

- all variables are terms
- If f is a function symbol of arity k, and if t
_{1},...,t_{k}, are terms, then f(t_{1},...,t_{k}) is also a term.

For a distinction, you may keep in mind that terms do not compute a truth value, a formula does.

**References:**
[1] Uwe Schöning: Logik für Informatiker. Spektrum Akademischer Verlag, 2000

or in english:

[2] Uwe Schöning: Logic for computer scientists, Birkhäuser, 2008, also

online available