原子式

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

原子式の正確な形式は、検討対象の論理によって異なります。たとえば、命題論理では、命題変数はしばしば「原子式」と簡潔に呼ばれますが、より正確には、命題変数は原子式ではなく、原子式を表す形式表現です。述語論理では、原子は述語記号とその引数であり、各引数は項です。モデル理論では、原子式は単に与えられたシグネチャを持つ記号の列であり、与えられたモデルに関して充足可能である場合もそうでない場合もあります。 ^{[ 1 ]}

通常の1階述語論理の整形式項と命題は、以下の構文を持つ。

条項：

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

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

命題：

• ${\displaystyle 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 _nに対して、 P ( t ₁ ,…, t _n )の形式の式です。

その他の整形式論理式はすべて、原子を論理結合子と量化子で構成することによって得られる。

例えば、式 ∀ x. P ( x ) ∧ ∃ y. Q ( y , f ( x )) ∨ ∃ z. R ( z ) には原子が含まれています。

• ${\displaystyle P(x)}$
• ${\displaystyle Q(y,f(x))}$
• ${\displaystyle R(z)}$。

原子式には量化子がないため、原子式中の変数記号の出現はすべて自由である。^{[ 2 ]}

• モデル理論では、構造によって原子式に解釈が与えられる。
• 証明論では、原子式の極性割り当ては焦点化の重要な構成要素です。
• 原子文

• ヒンマン、P. (2005).数理論理学の基礎. AK Peters. ISBN 1-56881-262-0。