リテラル (数理論理学)

数理論理学において、リテラル（テンプレート:Lang-en-short）とは、原子論理式（アトムあるいは素論理式とも呼ばれる）あるいはその否定のことであるテンプレート:Refn テンプレート:Refn。この定義は主に（古典論理の）証明論において、例えば連言標準形や導出の方法において現れる。

リテラルは2つの種類に分けることができるテンプレート:Refn。

正リテラルとは、単にアトムのことである（例えば $x$ ）。
負リテラルとは、アトムの否定のことである（例えば $\neg x$ ）。

リテラルの「極性」は、それが正リテラルであるか負リテラルであるかに応じて正または負となる。

二重否定の除去（ $\neg \neg x \equiv x$ ）が成り立つ論理では、あるリテラル $l$ の「補リテラル」あるいは「補元」は、 $l$ の否定に対応するリテラルとして定義できるテンプレート:Refn。 $l$ の補リテラルを表すのに $\bar{l}$ と書くことができる。より正確には、 $l \equiv x$ ならば $\bar{l}$ は $\neg x$ であり、 $l \equiv \neg x$ ならば $\bar{l}$ は $x$ である。二重否定の除去は古典論理では成り立つが、直観主義論理では成り立たない。

連言標準形における論理式の文脈では、あるリテラルの補元がその論理式中に現れないとき、そのリテラルは「純粋」であるという。

ブール関数においては、逆形式であるか非補形式であるかにかかわらず、変数の個々の出現がそれぞれリテラルである。例えば、 $A$ 、 $B$ 、 $C$ が変数であるとき、式 $\bar{A} B C$ は3つのリテラルを含み、式 $\bar{A} C + \bar{B} \bar{C}$ は4つのリテラルを含む。しかし、式 $\bar{A} C + \bar{B} C$ も4つのリテラルを含むと言われる。なぜなら、2つのリテラルが同一である（ $C$ が2回現れる）としても、これらは2つの別個の出現として数えられるからであるテンプレート:Sfn。

例

命題計算においては、リテラルとは単に命題変数あるいはその否定のことである。

述語計算においては、リテラルとは原子論理式あるいはその否定のことであり、原子論理式とは、いくつかの項に適用された述語記号 $P (t_{1}, \dots, t_{n})$ のことである。ここで項は、定数記号、変数記号、関数記号から出発して再帰的に定義される。例えば、 $\neg Q (f (g (x), y, 2), x)$ は、定数記号 2、変数記号 x、y、関数記号 f、g、述語記号 Q からなる負リテラルである。