Literal (mathematical logic)

Template:Short description In mathematical logic, a literal is an atomic formula (also known as an atom or prime formula) or its negation.Template:RefnTemplate:Refn 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:Template:Refn

• A positive literal is just an atom (e.g., $x$).
• A negative literal is the negation of an atom (e.g., $\mathrm{\neg }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 $\mathrm{\neg }\mathrm{\neg }x\equiv x$) the complementary literal or complement of a literal $l$ can be defined as the literal corresponding to the negation of $l$.Template:Refn We can write $\overline{l}$ to denote the complementary literal of $l$. More precisely, if $l\equiv x$ then $\overline{l}$ is $\mathrm{\neg }x$ and if $l\equiv \mathrm{\neg }x$ then $\overline{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 $\overline{A}BC$ contains three literals and the expression $\overline{A}C+\overline{B}\overline{C}$ contains four literals. However, the expression $\overline{A}C+\overline{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.Template:Sfn

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,\dots ,t_n)$ with the terms recursively defined starting from constant symbols, variable symbols, and function symbols. For example, $\mathrm{\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.

References

• Template:Cite book

• Template:Cite book

• Template:Cite book

• Template:Cite book