論理式

論理体系の文法に従って組み立てられた式。 well-formed formula、wff。

再帰的に定義する#

1. 原子命題は論理式
2. $A$ が論理式なら $\neg A$ も論理式
3. $A,B$ が論理式なら $A\wedge B$、$A\vee B$、$A\to B$ も論理式
4. 以上で作られるものだけが論理式

構成の仕方そのものが定義になっている。 この形の定義に対しては構造帰納法で 性質を証明できる。

プログラミング言語の構文も まったく同じ形で定義される（BNF）。

自由変数と束縛変数#

$$\forall xP(x,y)$$

$x$ は $\forall$ に束縛され、$y$ は自由。 自由変数を持つ式は、値が決まらないと真偽が定まらないので命題ではない。

束縛変数の名前は変えてよい（$\alpha$ 変換）。 これはラムダ計算でも同じ規則で、 論理式と関数の構文が同じ構造を持つことの一例。

標準形#

任意の論理式は同値な標準形に変換できる。

• 選言標準形 (DNF) — 論理積の論理和
• 連言標準形 (CNF) — 論理和の論理積

SAT ソルバは CNF を入力に取る。 任意の式は Tseitin 変換で、 サイズを線形に保ったまま CNF に直せる。

参考文献#

• Herbert B. Enderton. A Mathematical Introduction to Logic, 2nd ed. Academic Press, 2001. https://doi.org/10.1016/b978-0-08-049646-7.50005-9
• Kenneth H. Rosen. Discrete Mathematics and Its Applications, 8th ed. McGraw-Hill, 2019. https://www.mheducation.com/highered/product/discrete-mathematics-applications-rosen/M9781259676512.html