リテラル（数学的論理）

数理論理学において、リテラルは原子式（アトム式または素数式とも呼ばれる）またはその否定である。^{[1] [2]}その定義は主に証明論（古典論理）に現れ、例えば連言正規形や解析法に現れる。

リテラルは2つのタイプに分けられます: ^[2]

• 肯定リテラルは単なるアトムです (例: )。${\displaystyle x}$
• 否定リテラルはアトムの否定です (例: )。${\displaystyle \lnotx}$

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

二重否定除去を伴う論理（ただし）では、補リテラルまたはリテラルの補リテラルは、 の否定に対応するリテラルとして定義できます。^[3]の補リテラルを表すために と書くことができます。より正確には、の場合、 であり、の場合、 です。二重否定除去は古典論理では発生しますが、直観主義論理では発生しません。 ${\displaystyle \lnot \lnot x\equiv x}$${\displaystyle l}$${\displaystyle l}$${\displaystyle {\bar {l}}}$${\displaystyle l}$${\displaystyle l\equiv x}$${\displaystyle {\bar {l}}}$${\displaystyle \lnotx}$${\displaystyle l\equiv \lnot x}$${\displaystyle {\bar {l}}}$${\displaystyle x}$

連言標準形の式のコンテキストでは、リテラルの補数が式に現れない場合、 リテラルは純粋です。

ブール関数では、逆数形式または非補数形式の変数の各出現はリテラルです。たとえば、、およびが変数である場合、式には3つのリテラルが含まれ、式には4つのリテラルが含まれます。ただし、リテラルのうち2つは同一（ 2回出現）ですが、これらは2つの別個の出現として適格であるため、式には4つのリテラルが含まれているとも言えます。^[4]${\displaystyle A}$${\displaystyle B}$${\displaystyle C}$${\displaystyle {\bar {A}}BC}$${\displaystyle {\bar {A}}C+{\bar {B}}{\bar {C}}}$${\displaystyle {\bar {A}}C+{\bar {B}}C}$${\displaystyle C}$

命題計算では、リテラルは単に命題変数またはその否定です。

述語計算では、リテラルは原子式またはその否定であり、原子式はいくつかの項に適用される述語記号であり、項は定数記号、変数記号、関数記号から始まって再帰的に定義されます。たとえば、は定数記号 2、変数記号x、y、関数記号f、g、および述語記号Qを持つ否定リテラルです。 ${\displaystyle P(t_{1},\ldots,t_{n})}$${\displaystyle \neg Q(f(g(x),y,2),x)}$

• Ben-Ari, Mordechai (2001).コンピュータサイエンスのための数学的論理(第 2 版). Springer. ISBN 1-85233-319-7。

• Buss, Samuel R. (1998)。「証明理論入門」(PDF)。Buss , Samuel R. (編)。証明理論ハンドブック。アムステルダム: Elsevier。pp. 1–78。ISBN 0-444-89840-9。

• Godse, Atul P.; Godse, Deepali A. (2008)。デジタル論理回路。技術出版物。ISBN 9788184314250。

• ラウテンバーグ、ヴォルフガング(2010)。『数学論理の簡潔な入門』。Universitext (第 3 版)。Springer。doi : 10.1007 / 978-1-4419-1221-3。ISBN 978-1-4419-1220-6。