原子式

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

原子式の正確な形式は、検討中の論理によって異なります。たとえば、命題論理では、命題変数はしばしば「原子式」とより簡潔に呼ばれますが、より正確には、命題変数は原子式ではなく、原子式を表す形式表現です。述語論理では、原子は述語記号とその引数であり、各引数は項です。モデル理論では、原子式は、特定のシグネチャを持つ記号の文字列にすぎず、特定のモデルに関して満足できる場合とそうでない場合があります。 ^[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 ₁ ,…, t _n )という形式の式であり、 P は述語で、t_は項です。

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

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

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

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

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

• Hinman, P. (2005).数学論理学の基礎. AK Peters. ISBN 1-56881-262-0。