What are not examples of Atomic Formulas?

306 Views Asked by At

I am having trouble understanding what exactly an atomic formula is and its relevance.

The definition I have is as follows: An Atomic Formula is an expression of the form $A(t_1, \dots, t_n)$ where $A$ is an n-ary predicate symbol and each $t_i$ is a term (i.e., variable or constant symbol).

I believe my confusion primarily lies in the fact that it seems to just be a predicate with values filled in rather than a "standard" formula (using $\neg, \lor, \land, \rightarrow, \leftarrow$). Moreover, I am having issue understanding when this would not be the case. I.e., what is an example of a non-atomic formula?

1

There are 1 best solutions below

7
On

Welcome to MSE!

Recall how formulas are (recursively) defined. let's work with the language of arithmetic for concreteness. So we have symbols $0,1,S,+,\times,<,=$ with their expected arities.

First we make the terms, which pick out elements of our structure. For instance

  • $0$
  • $S(0)$
  • $(1 + 1) + 1$
  • $1 \times y$
  • $y \times (y + 1)$
  • etc.

Next we define the atomic formulas. These are "atoms" in the sense that they "can't be broken down". These have truth values, but are the most basic questions we can ask. For us,

  • $0 = S(0)$
  • $(1 + 1) + 1 < 1 \times y$
  • etc.

Notice these all look like one of the relation symbols given in our language, with terms inside it. Notice, importantly, that these have nothing to do with the truth values of the formulas. It only has to do with whether it's a question we can ask. Of course, there's plenty of nonatomic formulas too:

  • $\big ( 0 = S(0) \big ) \land \big ( (1+1) + 1 < 1 \times y \big )$
  • $\lnot (0 = S(0))$
  • $\big ( (0 = x) \to (x \times y = 0) \big )$
  • etc.

Notice these are all formulas, which have truth values (at least once we instantiate the variables). They aren't "atomic" though, in the sense that they can be broken down into smaller parts.

If you like, formulas are trees, with leaves corresponding to atomic formulas and internal nodes corresponding to the connectives. See the example below

an example of the tree structure


I hope this helps ^_^