一階述語論理
c {\displaystyle c} が定数記号ならば、 F ( c ) ∈ D {\displaystyle F(c)\in D} 、すなわち F ( c ) {\displaystyle F(c)} は D {\displaystyle D} のある要素である。
集合 D {\displaystyle D} を M {\displaystyle M} の領域 (universe, domain) と呼び、通常 | M | {\displaystyle |M|} で表す。また、 F ( P ) {\displaystyle F(P)} , F ( f ) {\displaystyle F(f)} , F ( c ) {\displaystyle F(c)} などは通常 P M {\displaystyle P^{M}} , f M {\displaystyle f^{M}} , c M {\displaystyle c^{M}} と表される。
M {\displaystyle M} が一階の言語に対する構造であるとき、 M {\displaystyle M} の領域 | M | {\displaystyle |M|} の要素を M の個体 (individual) と呼ぶ。
全称化規則とは、x が変数のとき、φ から ∀x φ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる:
GEN = { (φ, ∀x φ) | φ は論理式かつ x は変数 } 。
(φ1, φ2) ∈ GEN であるとき、φ2 は φ1 からの全称化による導出であるという。
論理式 φ が論理式の集合 Σ から証明可能であるとは、Σ に属する論理式と論理公理から推論規則の有限回の適用によって φ が得られることを意味する。そして、Σ に属する論理式と論理公理から φ を導出する仮定を示した論理式の有限列を、Σ からの φ の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。
φ を論理式、Σ を論理式の集合とする。Σ からの φ の形式的証明 (formal proof) あるいは証明 (proof) とは、論理式の有限列 (φ0, ..., φn) で次をみたすものをいう: φn = φ 。 n 以下の任意の自然数 k に対して、次のいずれかが成り立つ: (a) φk ∈ Σ 。 (b) φk は論理公理である。 (c) ある i, j < k が存在して、φk は φi , φj からのモーダス・ポーネンスによる導出である。 (d) ある i < k が存在して、φk は φi からの全称化による導出である。
Σ からの φ の証明が存在するとき、φ は Σ から証明可能 (provable) である、あるいは φ は Σ の定理 (theorem) であるといい、 Σ ⊢ φ {\displaystyle \Sigma \vdash \varphi } と書く。