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]

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.

• Ben-Ari, Mordechai (2001). Mathematical Logic for Computer Science (2nd ed.). Springer. ISBN 1-85233-319-7.

• Buss, Samuel R. (1998). "An Introduction to Proof Theory" (PDF). In Buss, Samuel R. (ed.). Handbook of Proof Theory. Amsterdam: Elsevier. pp. 1–78. ISBN 0-444-89840-9.

• Godse, Atul P.; Godse, Deepali A. (2008). Digital Logic Circuits. Technical Publications. ISBN 9788184314250.

• Rautenberg, Wolfgang (2010). A Concise Introduction to Mathematical Logic. Universitext (3rd ed.). Springer. doi:10.1007/978-1-4419-1221-3. ISBN 978-1-4419-1220-6.