In mathematical logic, a literal is an atomic formula (also known as an atom or prime formula) or its negation. 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:
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 ) the complementary literal or complement of a literal can be defined as the literal corresponding to the negation of . We can write to denote the complementary literal of . More precisely, if then is and if then is . 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 , and are variables then the expression contains three literals and the expression contains four literals. However, the expression would also be said to contain four literals, because although two of the literals are identical ( appears twice) these qualify as two separate occurrences.
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, with the terms recursively defined starting from constant symbols, variable symbols, and function symbols. For example, is a negative literal with the constant symbol 2, the variable symbols x, y, the function symbols f, g, and the predicate symbol Q.
The formulas procured by (F1) and (F2) are said to be prime or atomic formulas, or simply called prime. As in propositional logic, prime formulas and their negations are called literals.
A literal is an atom or a negation of an atom. An atom is a positive literal and the negation of an atom is a negative literal.
If is a literal, is its complement. This means that if , then, and if then .