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., ${\displaystyle x}$).
• A negative literal is the negation of an atom (e.g., ${\displaystyle \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 ${\displaystyle \lnot \lnot x\equiv x}$) the complementary literal or complement of a literal ${\displaystyle l}$ can be defined as the literal corresponding to the negation of ${\displaystyle l}$.^[3] We can write ${\displaystyle {\bar {l))}$ to denote the complementary literal of ${\displaystyle l}$. More precisely, if ${\displaystyle l\equiv x}$ then ${\displaystyle {\bar {l))}$ is ${\displaystyle \lnot x}$ and if ${\displaystyle l\equiv \lnot x}$ then ${\displaystyle {\bar {l))}$ is ${\displaystyle 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 ${\displaystyle A}$, ${\displaystyle B}$ and ${\displaystyle C}$ are variables then the expression ${\displaystyle {\bar {A))BC}$ contains three literals and the expression ${\displaystyle {\bar {A))C+{\bar {B)){\bar {C))}$ contains four literals. However, the expression ${\displaystyle {\bar {A))C+{\bar {B))C}$ would also be said to contain four literals, because although two of the literals are identical (${\displaystyle 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, ${\displaystyle P(t_{1},\ldots ,t_{n})}$ with the terms recursively defined starting from constant symbols, variable symbols, and function symbols. For example, ${\displaystyle \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.