In mathematical logic, an atomic formula or its negation

In mathematical logic, a **literal** is an atomic formula (also known as an atom or prime formula) or its negation.^{[1]}^{[2]} The definition mostly appears in proof theory (of classical logic), e.g. in conjunctive normal form and the method of resolution.

Literals can be divided into two types:^{[2]}

- A
**positive literal** is just an atom (e.g., $x$).
- A
**negative literal** is the negation of an atom (e.g., $\lnot x$).

The **polarity** of a literal is positive or negative depending on whether it is a positive or negative literal.

In logics with double negation elimination (where $\lnot \lnot x\equiv x$) the **complementary literal** or **complement** of a literal $l$ can be defined as the literal corresponding to the negation of $l$.^{[3]} We can write ${\bar {l))$ to denote the complementary literal of $l$. More precisely, if $l\equiv x$ then ${\bar {l))$ is $\lnot x$ and if $l\equiv \lnot x$ then ${\bar {l))$ is $x$. Double negation elimination occurs in classical logics but not in intuitionistic logic.

In the context of a formula in the conjunctive normal form, a literal is **pure** if the literal's complement does not appear in the formula.

In Boolean functions, each separate occurrence of a variable, either in inverse or uncomplemented form, is a literal. For example, if $A$, $B$ and $C$ are variables then the expression ${\bar {A))BC$ contains three literals and the expression ${\bar {A))C+{\bar {B)){\bar {C))$ contains four literals. However, the expression ${\bar {A))C+{\bar {B))C$ would also be said to contain four literals, because although two of the literals are identical ($C$ appears twice) these qualify as two separate occurrences.^{[4]}

##
Examples

In propositional calculus a literal is simply a propositional variable or its negation.

In predicate calculus a literal is an atomic formula or its negation, where an atomic formula is a predicate symbol applied to some terms, $P(t_{1},\ldots ,t_{n})$ with the terms recursively defined starting from constant symbols, variable symbols, and function symbols. For example, $\neg Q(f(g(x),y,2),x)$ is a negative literal with the constant symbol 2, the variable symbols *x*, *y*, the function symbols *f*, *g*, and the predicate symbol *Q*.