Literal (mathematical logic)

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]