## You are here

Homeatomic formula

## Primary tabs

# atomic formula

Let $\Sigma$ be a signature and $T(\Sigma)$ the set of terms over $\Sigma$. The set $S$ of symbols for $T(\Sigma)$ is the disjoint union of $\Sigma$ and $V$, a countably infinite set whose elements are called *variables*. Now, adjoin $S$ the set $\{=,(,)\}$, assumed to be disjoint from $S$. An *atomic formula* $\varphi$ over $\Sigma$ is any one of the following:

1. either $(t_{1}=t_{2})$, where $t_{1}$ and $t_{2}$ are terms in $T(\Sigma)$,

2. or $(R(t_{1},...,t_{n}))$, where $R\in\Sigma$ is an $n$-ary relation symbol, and $t_{i}\in T(\Sigma)$.

Remarks.

1. Using atomic formulas, one can inductively build formulas using the logical connectives $\vee$, $\neg$, $\exists$, etc… In this sense, atomic formulas are formulas that can not be broken down into simpler formulas; they are the building blocks of formulas.

2. A

*literal*is a formula that is either atomic or of the form $\neg\varphi$ where $\varphi$ is atomic. If a literal is atomic, it is called a*positive literal*. Otherwise, it is a*negative literal*.3. A finite disjunction of literals is called a

*clause*. In other words, a clause is a formula of the form $\varphi_{1}\vee\varphi_{2}\vee\cdots\vee\varphi_{n}$, where each $\varphi_{i}$ is a literal.4. A

*qunatifier-free formula*is a formula that does not contain the symbols $\exists$ or $\forall$.5. If we identify a formula $\varphi$ with its double negation $\neg(\neg\varphi)$, then it can be shown that any quantifier-free formula can be identified with a formula that is in conjunctive normal form, that is, a finite conjunction of clauses. For a proof, see this link

## Mathematics Subject Classification

03C99*no label found*03B10

*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections