Polarity (mathematical Logic)

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:
* A positive literal is just an atom (e.g., $x$).
* A negative literal is the negation of an atom (e.g., $\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 $\lnot \lnot x \equiv x$) the complementary literal or complement of a literal $l$ can be defined as the literal corresponding to the negation of $l$. We can write $\bar$ to denote the complementary literal of $l$. More precisely, if $l\equiv x$ then $\bar$ is $\lnot x$ and if $l\equiv \lnot x$ then $\bar$ is $x$. Double negation elimination occurs in classical logics but not in