地上表現

数理論理学では、形式体系の基底項は変数を含まない項です。同様に、基底式は変数を含まない 式です。

定数記号 および との同一性を持つ一階述語論理では、文は基礎式です。基礎式は基礎項または基礎式です。 ${\displaystyle a}$${\displaystyle b}$ ${\displaystyle Q(a)\or 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 つの規則を有限に適用することで作成できます (他の基底項はありません。特に、述語は基底項になることはできません)。

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

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

が-ary 述語記号で、が基底項である場合、 は基底述語または基底アトムです。 ${\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つの自由変数を含む式フォールバックとしてウィキデータの説明を表示するページ
• 文（数学的論理）  – 数学的論理において、自由変数のない整形式の式

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