原子式

数理論理学において、原子式（アトム式、プライム式とも呼ばれる）とは、より深い命題構造を持たない式、すなわち論理接続詞を含まない式、あるいは厳密な部分式を持たない式である。したがって、アトムは論理における最も単純な整形式式である。複合式は、原子式を論理接続詞を用いて組み合わせることによって形成される。

原子式（atomic formula）の正確な形式は、対象となる論理に依存する。例えば、命題論理においては、命題変数はしばしば「原子式」と略されるが、より正確には、命題変数は原子式ではなく、原子式を表す形式表現である。述語論理においては、原子は述語記号とその引数（各引数は項）の組み合わせである。モデル理論においては、原子式は与えられたシグネチャを持つ単なる記号列であり、与えられたモデルに関して満足可能である場合もそうでない場合もある。 ^[1]

一階述語論理における原子式

通常の第一階論理の整形式の項と命題は次のような構文を持ちます。

条項：

$t\equiv c\mid x\mid f(t_{1},\dotsc ,t_{n})$ 、

つまり、項は再帰的に定数c （談話領域の名前付きオブジェクト）、変数x（談話領域内のオブジェクトを範囲とする）、または項t _kを引数とするn項関数fとして定義されます。関数はオブジェクトのタプルをオブジェクトにマッピングします。

提案:

$A,B,...\equiv P(t_{1},\dotsc ,t_{n})\mid A\wedge B\mid \top \mid A\vee B\mid \bot \mid A\supset B\mid \forall x.\ A\mid \exists x.\ A$ 、

つまり、命題は、項t _kを引数とするn項述語 P、または他の命題で使用される論理接続詞(and、or) と量指定子(for-all、there-exists) で構成される式として再帰的に定義されます。

原子式またはアトムは、単に項の組に適用される述語です。つまり、原子式は、P ( t ₁ ,…, t _n ) という形式の式です ( Pは述語、t_は項です)。

その他の適切な式はすべて、論理接続詞と量指定子を使用してアトムを構成することによって得られます。

例えば、式 ∀ x. P ( x ) ∧ ∃ y. Q ( y , f ( x )) ∨ ∃ z. R ( z ) には、原子

$P(x)$
$Q(y,f(x))$
$R(z)$ 。

原子式には量指定子は現れないので、原子式中の変数記号の出現はすべて自由である。^[2]

参照

モデル理論では、構造によって原子式に解釈が割り当てられます。
証明理論では、原子式の極性割り当ては焦点を当てる上で重要な要素です。
原子刑

参考文献

^ ホッジス、ウィルフリッド (1997). 『短縮モデル理論』ケンブリッジ大学出版局. pp. 11– 14. ISBN 0-521-58713-1。
^ WVOクワイン『数理論理学』（1981年）、p.161。ハーバード大学出版局、0-674-55451-5

さらに読む

ヒンマン、P. (2005). 『数理論理学の基礎』 AKピーターズ. ISBN 1-56881-262-0。

[1] ホッジス、ウィルフリッド (1997). 『短縮モデル理論』ケンブリッジ大学出版局. pp. 11– 14. ISBN 0-521-58713-1。

[2] WVOクワイン『数理論理学』（1981年）、p.161。ハーバード大学出版局、0-674-55451-5