Wednesday, December 16, 2015

Atoms, Atomic Formulas, and Functions

 © 2015 by Sidney Harris
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:
  • P (x) 
  • Q (y, f (x))
  • R (z)
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:
  1. If P is a predicate symbol of arity k, and if t1,...,tk, are terms, then P(t1,...,tk) is a formula.
  2. (Negation) For all formulas F, also ¬F is a formula
  3. (Binary Connectives) For all Formulas F,G, also F∧G,F∨G,F→ G,F↔G are formulas 
  4. (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:
  1. all variables are terms
  2. If f is a function symbol of arity k, and if t1,...,tk, are terms, then f(t1,...,tk) 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 availabl

No comments:

Post a Comment