地上表現

Term that does not contain any variables

数理論理学において、形式体系の基底項とは、変数を含まない項のことである。同様に、基底式とは、変数を含まない式のことである。

定数記号およびとの同一性を持つ一階述語論理において、文は基礎式である。基礎式とは、基礎項または基礎式である。 ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle Q(a)\lor P(b)}$

例

数値 0 と 1 を表す定数シンボルと、後続関数を表す単項関数シンボル、および加算を表す二項関数シンボルを含むシグネチャ上の次の一階述語論理式を考えます。 ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle s}$ ${\displaystyle +}$

• ${\displaystyle s(0),s(s(0)),s(s(s(0))),\ldots }$基底用語です。
• ${\displaystyle 0+1,\;0+1+1,\ldots }$基底用語です。
• ${\displaystyle 0+s(0),\;s(0)+s(0),\;s(0)+s(s(0))+0}$基底用語です。
• ${\displaystyle x+s(1)}$およびは項ですが、基底項ではありません。 ${\displaystyle s(x)}$
• ${\displaystyle s(0)=1}$およびは、基本式です。 ${\displaystyle 0+0=0}$

正式な定義

以下は一階言語の正式な定義である。定数記号の集合、関数演算子の集合、述語記号の集合を持つ一階言語が与えられているとする。 ${\displaystyle C}$ ${\displaystyle F}$ ${\displaystyle P}$

グラウンド用語

あ基底項は変数を含まない項です。基底項は論理再帰（式再帰）によって定義できます。

1. の要素は基底項です。 ${\displaystyle C}$
2. が- 項関数の記号であり、が基底項である場合、は基底項です。 ${\displaystyle f\in F}$ ${\displaystyle n}$ ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ ${\displaystyle f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$
3. すべての基底項は、上記の 2 つの規則を有限に適用することで与えることができます (他の基底項はありません。特に、述語は基底項になることはできません)。

大まかに言えば、エルブラン宇宙はすべての基底項の集合です。

基底原子

あ根拠述語、基底原子または基底リテラルは、そのすべての引数項が基底項である原子式

が- 項述語記号でが基底項である場合、 は基底述語または基底アトムです。 ${\displaystyle p\in P}$ ${\displaystyle n}$ ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ ${\displaystyle p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$

大まかに言えば、エルブラン基底はすべての基底原子の集合であり、^[1]エルブラン解釈は基底内の各基底原子に真理値を割り当てます。

グラウンドフォーミュラ

あ粉砕式または基礎節は変数のない式です。

基底式は、次のように構文再帰によって定義できます。

1. 基底原子は基底式です。
2. および が基底式である場合、、、および は基底式です。 ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle \lnot \varphi }$ ${\displaystyle \varphi \lor \psi }$ ${\displaystyle \varphi \land \psi }$

基底式は、閉じた式の一種です。

参照

• オープン式 – 少なくとも1つの自由変数を含む式
• 文（数理論理学）  – 数理論理学において、自由変数を含まない整形式の式

注記

1. Alex Sakharov. 「Ground Atom」. MathWorld . 2025年5月4日閲覧。

参考文献

• Dalal, M. (2000). 「論理ベースのコンピュータプログラミングパラダイム」 Rosen, KH; Michaels, JG (編).離散数学と組合せ数学ハンドブック. p. 68.
• ファーン、アラン（2010年1月8日）「講義ノート｜一階述語論理：構文と意味論」（PDF）
• ホッジス、ウィルフリッド（1997年）『短縮モデル理論』ケンブリッジ大学出版局、ISBN 978-0-521-58713-6。

Retrieved from "https://en.wikipedia.org/w/index.php?title=Ground_expression&oldid=1289689386"