一階述語論理

一階述語論理（いっかいじゅつごろんり、英: first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（英: second-order predicate logic）と呼び、さらなる一般化を加えた述語論理を高階述語論理（英: higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細はそれぞれの記事を参照。

命題論理では文を構成する最も基本的な命題（原子命題）は命題記号と呼ぶ一つの記号によって表していた。それに対し、一階述語論理においては、最も基本的な命題は原子論理式と呼ぶ記号列によって表す。原子論理式とは述語記号( ${\displaystyle P}$ )と呼ぶ記号と、項( ${\displaystyle t_{1},\,\cdots ,\,t_{n}}$ ) と呼ぶものの列、からなる ${\displaystyle P(t_{1},\,\cdots ,\,t_{n})}$ という形の記号列であり、これは個体の間の関係を表すものである。

命題論理にない一階述語論理のもう一つの特徴は量化 (quantification) である。例えば、定言的命題論理の範囲において、次のような推論の妥当性を扱うことはできない：

すべての人間は死ぬ。

ソクラテスは人間である。

したがってソクラテスは死ぬ。

一階述語論理では、このような「すべての…について」という表現や、また「ある…について」といった表現を扱えるように、全称量化記号 (universal quantifier) と呼ぶ記号 ${\displaystyle \forall }$; と存在量化記号 (existential quantifier) と呼ぶ記号 ${\displaystyle \exists }$; を新たに導入する。これらを用いると「すべての ${\displaystyle x}$ について ${\displaystyle \phi }$; である」という命題は ${\displaystyle \forall x\phi }$; 、「ある ${\displaystyle x}$ に対して ${\displaystyle \phi }$; である」は ${\displaystyle \exists x\phi }$; と表される。これらの記号を用いると上の三つの文はそれぞれ、例えば、

${\displaystyle \forall x[P(x)\Rightarrow Q(x)]}$

${\displaystyle P(a)}$

${\displaystyle Q(a)}$

のように記号化することができる。ここで、${\displaystyle P(x)}$ と ${\displaystyle Q(x)}$ はそれぞれ「 ${\displaystyle x}$ は人間である」「${\displaystyle x}$ は死ぬ」を表し、${\displaystyle a}$ はソクラテスを表すことを意図している。上の日本語による定言命題推論の妥当性は不決定的だが、仮言命題推論化されるならば、一階述語論理において ${\displaystyle Q(a)}$ が

${\displaystyle \{\forall x[P(x)\Rightarrow Q(x)]\,,\,P(a)\}}$

の論理的帰結 (logical consequence) であるという事実に反映される。一般に、論理式 ${\displaystyle \phi }$; が論理式の可算集合 ${\displaystyle \Sigma }$; の論理的帰結であるとは、${\displaystyle \Sigma }$; の論理式のすべてをみたす解釈は必ず ${\displaystyle \phi }$; もみたすこととして定義され、これは、あるいくつかの前提からある結論が論理的に導かれるという概念の数学的な定式化である。

命題論理においては、論理式の解釈は各命題記号に対する真理値 0 , 1 の割り当てが与えられた。これに対して、一階述語論理の論理式の解釈は構造 (structure) と呼ばれ、これは領域 (universe, domain) と呼ぶ空でない集合と、それぞれの非論理記号（述語記号・関数記号・定数記号）の "意味" の割り当てからなる。領域とは「すべての ${\displaystyle x}$ について」といったときの ${\displaystyle x}$ が動きうる値の範囲である。一階述語論理の論理式は構造を一つ与えることによって真偽が決定される。

二階述語論理（およびそれ以上の高階述語論理）では、述語および関数に対する量化を導入する。

一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 ZFC は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの形式的証明 (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他にペアノ算術のように単独で形式化する理論もある。

一階述語論理の言語（一階の言語）は次のものからなる：

論理記号 (logical symbol)

1. 変数（あるいは個体変数）と呼ぶ記号の集合： ${\displaystyle V=\{x_{1},\,x_{2},\,\cdots \}}$
2. 結合記号： ${\displaystyle \lnot }$, ${\displaystyle \land }$ , ${\displaystyle \lor }$, ${\displaystyle \Rightarrow }$, ${\displaystyle \Leftrightarrow }$
3. 量化記号： ${\displaystyle \forall }$, ${\displaystyle \exists }$
4. 括弧： ${\displaystyle (}$ , ${\displaystyle )}$ , ${\displaystyle [}$ , ${\displaystyle ]}$ , ${\displaystyle \{}$ , ${\displaystyle \}}$
5. 等号： ${\displaystyle =}$ （含まなくてもよい。）

非論理記号 (nonlogical symbol)

1. 述語記号と呼ぶ記号の集合（有限集合でも無限集合でもよい）。各述語記号にはアリティ（arity）と呼ぶ引数の個数に相当する正の整数が一つ対応しているものとする^[1]。
2. 関数記号と呼ぶ記号の集合（有限集合でも無限集合でもよい）。各関数記号もアリティを持っているものとする。
3. 定数記号と呼ぶ記号の集合（有限集合でも無限集合でもよい）。

一階の言語は、それが等号を持つかどうか、非論理記号に何を持っているかを決めることによって定まる。例えば集合論においては、等号を持ち、非論理記号としてはアリティ ${\displaystyle 2}$ の述語記号 ${\displaystyle \in }$; だけをもつ一階の言語（集合論の言語）が使われる。以下に一階の言語について、いくつかの注意を述べる。

• 等号 ${\displaystyle =}$ はアリティ ${\displaystyle 2}$ の特別な述語記号として扱われる。どの一階の言語にも等号を含めて少なくとも一つは述語記号が含まれていなければならないものとする。
• アリティ ${\displaystyle n}$ の述語（関数）記号を、${\displaystyle n}$ 変数述語（関数）記号と呼ぶこともある。
• 記号は一つの用途のみに用いる。すなわち、一つの一階の言語において、ある記号が述語記号であると同時に定数記号でもあるということや、論理記号であると同時に関数記号でもあるというようなことがあってはならない。
• いくつかの結合記号や量化記号は言語にもともと含まれている記号ではなく、省略記法として定義によって導入される場合がある。例えば、${\displaystyle \Leftrightarrow }$; は言語に含まれず、 ${\displaystyle (\phi \Leftrightarrow \psi )}$ は ${\displaystyle [(\phi \Rightarrow \psi )\land (\psi \Rightarrow \phi )]}$ を表すものとして定義される場合もある。上の論理記号すべてを用いて表現される命題は、例えば ${\displaystyle \lnot }$、${\displaystyle \lor }$、${\displaystyle \exists }$ や ${\displaystyle \lnot }$、${\displaystyle \Rightarrow }$、${\displaystyle \forall }$ だけを用いても十分に表現できることが知られている。
• 文献によっては、${\displaystyle \Rightarrow }$ の代わりに ${\displaystyle \supset }$; を用い、${\displaystyle \forall }$ の代わりに ${\displaystyle \Pi }$; を用いている場合がある。
• 同一性関係を一階述語論理の一部とみなす場合もある。その場合、等号は必ず言語に含まれることになる。常に等号が含まれることを仮定した一階述語論理を等号付き一階述語論理と呼ぶ。
• 定数記号はアリティ 0 の関数記号と呼ぶこともある。
• 上の定義では述語は 1 以上のアリティを持つとされているが、アリティ 0 の述語も考えることができ、それらは「真」や「偽」を意味するものと考えることができる。しかし「真」は ${\displaystyle \forall x(x=x)}$ などと別の方法で表せるので、アリティ 0 の述語を導入することに大きな意味はない。
• 括弧の使い方の流儀は様々である。ある人は ${\displaystyle \forall x}$ を ${\displaystyle (\forall x)}$ と書く。括弧の代わりにコロンや終止符を使う場合もある。もちろんその場合には、言語にコロンや終止符を含めておく必要がある。括弧を全く使わない表記法にポーランド記法(Polish notation)と呼ぶものがある。これは、${\displaystyle \land }$; や ${\displaystyle \lor }$; を先頭に書いて ${\displaystyle (\phi \land \psi )}$ の代わりに ${\displaystyle \land \phi \psi }$ のように書く方法である。ポーランド記法はコンパクトで数学的に取り扱いやすいという利点があり、可読性が低いという欠点がある。

一階述語論理の項 (term) は次のように帰納的に定義される：

1. 変数と定数記号はすべて項である。
2. ${\displaystyle t_{1},\,\cdots ,\,t_{n}}$ が項で、${\displaystyle f}$ がアリティ n の関数記号ならば、${\displaystyle ft_{1},\,\cdots ,\,t_{n}}$ は項である^[2]。
3. 上記の 1. と 2. によって項とされるものだけが項である。

項というのは直観的には議論領域に属するある対象を表す"名前"の役割をもった記号列である。

例． 自然数論の言語は等号を持つ一階の言語で、非論理記号として 、${\displaystyle 1}$ 変数関数記号 ${\displaystyle S}$ 、${\displaystyle 2}$ 変数関数記号 ${\displaystyle +}$ , ${\displaystyle \cdot }$ と定数記号 ${\displaystyle 0}$ を持つ。定義より、

${\displaystyle x_{1}}$ , 　${\displaystyle x_{5}}$ , 　${\displaystyle 0}$ , 　${\displaystyle Sx_{1}}$ , 　${\displaystyle S0}$ , 　${\displaystyle SS0}$ , 　${\displaystyle +S0S0}$ , 　${\displaystyle +0x_{5}}$ , 　${\displaystyle \cdot Sx_{1}+0x_{5}}$

はすべて項である。 ${\displaystyle +S0S0}$ や ${\displaystyle +0x_{5}}$ といった前置記法は読みにくいため、これらの項を表すのに、通常使われている ${\displaystyle S(0)+S(0)}$ や ${\displaystyle 0+x_{5}}$ のような表現(中置記法)が用いられることもある。したがって ${\displaystyle \cdot Sx_{1}+0x_{5}}$ は中置記法では ${\displaystyle S(x_{1})\cdot (0+x_{5})}$ のように表される。

項が何らかの対象を表す記号列であったのに対して、論理式は何らかの命題を表すものである。論理式は原子論理式と呼ぶ最も基本的な論理式から結合記号と量化記号を繰り返し用いることによって形成される。まず、原子論理式は次のように定義される：

ある正の整数 ${\displaystyle n}$ に対するアリティ ${\displaystyle n}$ の述語記号 ${\displaystyle P}$ と ${\displaystyle n}$ 個の項 ${\displaystyle t_{1},\,\cdots ,\,t_{n}}$ を用いて ${\displaystyle P(t_{1},\,\cdots ,\,t_{n})}$ と表される記号列を原子論理式 (atomic formula) と呼ぶ。

原子論理式を用いて、論理式 (well-formed formula, wff) あるいは式 (formula) は次のように帰納的に定義される：

1. 原子論理式は論理式である。
2. ${\displaystyle \phi }$ と ${\displaystyle \psi }$ が論理式ならば、${\displaystyle (\lnot \phi )}$ , ${\displaystyle (\phi \land \psi )}$ , ${\displaystyle (\phi \lor \psi )}$ , ${\displaystyle (\phi \Rightarrow \psi )}$ , ${\displaystyle (\phi \Leftrightarrow \psi )}$ は論理式である。
3. ${\displaystyle \phi }$ が論理式で ${\displaystyle x}$ が変数ならば、${\displaystyle (\forall x\phi )}$ , ${\displaystyle (\exists x\phi )}$ は論理式である。
4. 上記の 1. と 2. と 3. によって論理式とされるものだけが論理式である。

例． 再び自然数論の言語を考える。定義から、

${\displaystyle [(S0+S0)=SS0]}$ ,　 ${\displaystyle [(0+x_{5})=S0]}$

はすべて原子論理式（したがって論理式）であり、

${\displaystyle \{\lnot [(S0+S0)=SS0]\}}$ , 　${\displaystyle \{[(0+x_{5})=S0]\land [(S0+S0)=SS0]\}}$ , 　${\displaystyle \{\forall x_{5}[(0+x_{5})=S0]\}}$, 　${\displaystyle \{\exists x_{2}[(0+x_{5})=S0]\}}$

自然数論の言語における論理式 ${\displaystyle (S0+S0)=SS0}$ の各記号を通常の意味で解釈すれば「${\displaystyle 1+1=2}$」となり、これは真である論理式である。${\displaystyle \lnot [(S0+S0)=SS0]}$ は「${\displaystyle 1+1\neq 2}$」となるので通常の解釈で偽なる論理式である。また、変数の動く範囲（議論領域）は自然数全体の集合だとすれば、論理式 ${\displaystyle [\forall x_{1}(0=Sx_{1})]}$ は「すべての自然数 ${\displaystyle n}$ について ${\displaystyle 0=n+1}$」という意味になり、これは偽である論理式であることが分かる。一方、論理式 ${\displaystyle (0+x_{5})=S0}$ の意味を考えてみると、「${\displaystyle 0+x_{5}=1}$」となるがこれは真であるか偽であるかを判断することができない。なぜなら、${\displaystyle x_{5}}$ という変数が何を表しているかが決まっていないからである。このようなとき、${\displaystyle x_{5}}$ は論理式 ${\displaystyle (0+x_{5})=S0}$ における自由変数 (free variable) であると言われる。正式には、各論理式 ${\displaystyle \phi }$ に対して、"${\displaystyle \phi }$ における自由変数全体の集合" ${\displaystyle fr(\phi )}$ を次のように再帰的に定義する：

1. ${\displaystyle \phi }$ が原子論理式ならば、${\displaystyle fr(\phi )}$ は記号列 φ に現れるすべての変数からなる集合である。
2. ${\displaystyle fr[(\lnot \phi )]=fr(\phi )}$ 。
3. ${\displaystyle fr[(\phi \land \psi )]=fr[(\phi \lor \psi )]=fr[(\phi \Rightarrow \psi )]=fr[(\phi \Leftrightarrow \psi )]=fr(\phi )\cup fr(\psi )}$ 。
4. ${\displaystyle fr(\forall x\phi )=fr(\exists x\phi )=fr(\phi )-\{x\}}$。

論理式 ${\displaystyle \phi }$ が自由変数を一切持たないとき、つまり ${\displaystyle fr(\phi )=\varnothing }$ のとき、${\displaystyle \phi }$ は閉論理式 (closed formula) あるいは文 (sentence) と呼ぶ。直観的には、文とは記号に解釈を与えて意味を考えたときに正しいか正しくないかが決まるような論理式である。${\displaystyle (S0+S0)=SS0}$ や ${\displaystyle \forall x_{1}0=Sx_{1}}$ は文であるが、${\displaystyle fr[(0+x_{5})=S0]=\{x_{5}\}}$ より ${\displaystyle (0+x_{5})=S0}$ は文でない。

はじめに述べたように、一階述語論理の論理式の解釈は構造と呼ぶものによって与えられる。構造は変数が動く領域とそれぞれの非論理記号に対する "意味" の割り当てからなる。正式には、構造は次のように定義される。

一階の言語に対する構造 (structure) とは、空でない集合 ${\displaystyle D}$ と、非論理記号全体の集合を定義域とする関数 ${\displaystyle F}$ の組 ${\displaystyle M=(D,\,F)}$ で次をみたすものをいう：

1. ${\displaystyle P}$ がアリティ ${\displaystyle n}$ の述語記号ならば、${\displaystyle F(P)\subseteq D^{n}}$ 、すなわち ${\displaystyle F(P)}$ は ${\displaystyle D}$ 上の ${\displaystyle n}$ 項関係である。
2. ${\displaystyle f}$ がアリティ ${\displaystyle n}$ の関数記号ならば、${\displaystyle F(f):D^{n}\to D}$ 、すなわち ${\displaystyle F(f)}$ は ${\displaystyle D}$ 上の ${\displaystyle n}$ 項演算である。
3. ${\displaystyle c}$ が定数記号ならば、${\displaystyle F(c)\in D}$ 、すなわち ${\displaystyle F(c)}$ は　${\displaystyle D}$ のある要素である。

集合 ${\displaystyle D}$ を ${\displaystyle M}$ の領域 (universe, domain) と呼び、通常 ${\displaystyle |M|}$ で表す。また、${\displaystyle F(P)}$ , ${\displaystyle F(f)}$ , ${\displaystyle F(c)}$ などは通常 ${\displaystyle P^{M}}$ , ${\displaystyle f^{M}}$ , ${\displaystyle c^{M}}$ と表される。

${\displaystyle M}$ が一階の言語に対する構造であるとき、${\displaystyle M}$ の領域 ${\displaystyle |M|}$ の要素を M の個体 (individual) と呼ぶ。

上で見たように、自由変数を持たない論理式（すなわち文）は解釈（構造）を一つ与えることで、正しいか正しくないかが定まる。構造 M を与えたとき、文 φ が正しい命題になっているならば、φ は解釈 M において真 (true) であるといい、正しくない命題である場合、φ は M において偽 (false) であるという。以下で、これらの真偽の概念をより正確に定義する。ただし、論理式の真偽の定義にはいくつかの異なる（同値な）方法があり、ここで述べる定義はその内の一つである。

M が一階の言語に対する構造であるとき、変数全体の集合 V から M の領域 |M| への関数を、変数に対する M の個体の割り当て関数と呼ぶ。変数に対する M の個体の割り当て関数 s を一つとったとき、それぞれの項 t に対して、t の値 (value) t ^M(s) が次のように再帰的に定義される：

1. 変数 x に対しては、x ^M(s) = s(x) 。
2. 定数記号 c に対しては、c ^M(s) = c ^M 。
3. t₁ , ..., t_n が項で、f がアリティ n の関数記号ならば、(f t₁ … t_n)^M(s) = f ^M (t₁^M(s), ..., t_n^M(s)) 。

直観的には、項 t の値 t ^M(s) とは、各変数 x が Mの個体 s(x) を表すとしたとき、t が表す M の個体のことである。

次に、「構造 M が個体の割り当て関数 s によって論理式 φ を充足する」と言うことを定義する。M が s によって φ を充足するとは、各変数 x は s(x) を表すとし、各非論理記号は M によって与えられた意味を表すとしたとき、φ が正しい命題になっているということである。

M が一階の言語に対する構造であるとき、各論理式 φ と M の個体の割り当て関数 s に対して、M(φ, s) ∈ { 0, 1 } を次のように再帰的に定義する：

1. M(t₁ = t₂ , s) = 1 　⇔　 t₁^M(s) = t₂^M(s) 。
2. P がアリティ n の非論理述語記号ならば、　M(P t₁ … t_n , s) = 1　 ⇔　 (t₁^M(s), ..., t_n^M(s)) ∈ P ^M 。
3. M((¬ φ), s) = 1 　⇔　 M(φ, s) = 0 。
4. M((φ ∧ ψ), s) = 1 　⇔　 M(φ, s) = 1 かつ M(ψ, s) = 1 。
5. M((φ ∨ ψ), s) = 1 　⇔　 M(φ, s) = 1 または M(ψ, s) = 1 。
6. M((φ → ψ), s) = 1 　⇔　 M(φ, s) = 0 または M(ψ, s) = 1 。
7. M((φ ↔ ψ), s) = 1 　⇔　 M(φ, s) = M(ψ, s) 。
8. M(∀x φ, s) = 1 　⇔　 すべての m ∈ |M| に対して M(φ, s[x|m]) = 1 。
9. M(∃x φ, s) = 1 　⇔　 ある m ∈ |M| に対して M(φ, s[x|m]) = 1 。

ただし、s[x|m] は変数 x には m を割り当て、x 以外の変数に対しては s と同じ個体を割り当てる関数を表す。

M(φ, s) = 1 であるとき M は s によって φ を充足するという。

特に φ が文である場合は、すべての個体の割り当て関数 s に対して M(φ, s) = 1 であるか、すべての個体の割り当て関数 s に対して M(φ, s) = 0 であるかのいずれかであることが示される。そこで、前者の場合に φ は M において真であるといい、後者の場合に φ は M において偽であるという。すなわち、構造 M と文 φ に対して、

φ は M において真 (true) 　⇔　 任意の M の個体の割り当て関数 s に対して、M(φ, s) = 1 。

φ は M において偽 (false) 　⇔　 任意の M の個体の割り当て関数 s に対して、M(φ, s) = 0 。

と定義する。φ が M において真であるとき、M は φ のモデル (model) であるともいう。また、M が文の集合 Σ のすべての要素のモデルであるとき、単に M は Σ のモデルであるという。

Σ を論理式の集合とし、φ を論理式とする。Σ に属するすべての論理式 ψ に対して M(ψ, s) = 1 であるような任意の構造 M と M の個体の割り当て関数 s が M(φ, s) = 1 をみたすとき、φ は Σ の論理的帰結 (logical consquence) であるといい、${\displaystyle \Sigma \vDash \varphi }$ と書く。論理式 φ と ψ が ${\displaystyle \{\varphi \}\vDash \psi }$ かつ ${\displaystyle \{\psi \}\vDash \varphi }$ をみたすとき、φ と ψ は論理的に同値 (logically equivalent) であるという。また、φ が ∅ の論理的帰結である場合、すなわち任意の構造 M と M の個体の割り当て関数 s に対して M(φ, s) = 1 であるとき、φ は恒真 (valid) であるという。φ と ψ が論理的に同値であることは、(φ ↔ ψ) が恒真であることと同値である。

命題論理においては、論理公理 (logical axiom) と呼ぶ論理式の集合と、ある論理式たちから新たな論理式を導出する規則（推論規則）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体とトートロジー全体が一致するようにすることができる（命題論理の健全性と完全性）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。

形式的証明の定義の仕方はひとつではなく、様々な異なる（等価な）方法がある。ここで述べる定義はヒルベルト流計算の典型例であり、これは異なる公理を多数用意して推論規則を少なくするスタイルをとっている。ゲンツェン流の形式的証明では逆に、公理を少なくして推論規則を多く用いている。ここで述べるものと異なる証明可能性の定義については「自然演繹」「シークエント計算」などを参照。

以下の形の論理式すべてを論理公理とする。ここで、x, y は変数、t, t₁ , ..., t_n は項、φ, ψ は論理式を表す：

• トートロジー（命題論理におけるトートロジーの命題記号を一階の論理式で置き換えて得られる論理式）
• 量化記号に関する公理

1. ∀x φ → φ_x [ t ] 　（ただし、φ において t が x に代入可能（後述）の場合に限る）
2. ∀x (φ → ψ) → (∀x φ → ∀x ψ)
3. ∀x (¬ φ) ↔ (¬ ∃x φ)

• 等号に関する公理（言語が等号を持つ場合に限る）

1. x = x
2. x = y → (P t₁ … t_n → P u₁ … u_n) 　（ただし、P は n 変数述語記号で、u_i は t_i における x のいくつかを y で置き換えて得られる項である）

量化記号に関する公理 1. における φ_x [ t ] とは、論理式 φ において "束縛されていない" 変数 x をすべて項 t で置き換えて得られる論理式を表す（正確な定義は後述）。

推論規則とは、あるいくつかの論理式から別の論理式を導出するための規則である。これは正確には、論理式全体の集合の上の関係として定義される。推論規則には様々なものが考えられるが、ここで用いる推論規則はモーダス・ポーネンス (modus ponens) と呼ぶ規則と全称化 (generalization) と呼ぶ規則の二つである。

モーダス・ポーネンスとは、φ と (φ → ψ) から ψ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：

MP = { (φ, (φ → ψ), ψ) | φ と ψ は論理式 } 。

(φ₁, φ₂, φ₃) ∈ MP であるとき、φ₃ は φ₁, φ₂ からのモーダス・ポーネンスによる導出であるという。

全称化規則とは、x が変数のとき、φ から ∀x φ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる：

GEN = { (φ, ∀x φ) | φ は論理式かつ x は変数 } 。

(φ₁, φ₂) ∈ GEN であるとき、φ₂ は φ₁ からの全称化による導出であるという。

論理式 φ が論理式の集合 Σ から証明可能であるとは、Σ に属する論理式と論理公理から推論規則の有限回の適用によって φ が得られることを意味する。そして、Σ に属する論理式と論理公理から φ を導出する仮定を示した論理式の有限列を、Σ からの φ の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。

φ を論理式、Σ を論理式の集合とする。Σ からの φ の形式的証明 (formal proof) あるいは証明 (proof) とは、論理式の有限列 (φ₀, ..., φ_n) で次をみたすものをいう：

1. φ_n = φ 。
2. n 以下の任意の自然数 k に対して、次のいずれかが成り立つ：

(a) φ_k ∈ Σ 。

(b) φ_k は論理公理である。

(c) ある i, j < k が存在して、φ_k は φ_i , φ_j からのモーダス・ポーネンスによる導出である。

(d) ある i < k が存在して、φ_k は φ_i からの全称化による導出である。

Σ からの φ の証明が存在するとき、φ は Σ から証明可能 (provable) である、あるいは φ は Σ の定理 (theorem) であるといい、${\displaystyle \Sigma \vdash \varphi }$ と書く。

φ_x [ t ] は、論理式 φ において "束縛されていない" 変数 x をすべて項 t で置き換えて得られる論理式を表すと述べた。正確には、φ_x [ t ] は再帰によって次に述べるような仕方で定義される。

まず、それぞれの項 u に対して u_x [ t ] を次のように再帰的に定義する：

1. x_x [ t ] = t 。
2. y が x と異なる変数ならば、y_x [ t ] = y 。
3. c 定数記号ならば、c_x [ t ] = c 。
4. t₁ , ..., t_n が項で、f がアリティ n の関数記号ならば、(f t₁ … t_n)_x [ t ] = f (t₁)_x [ t ] … (t_n)_x [ t ] 。

そして、φ_x [ t ] を次のように再帰的に定義する：

1. 原子論理式 P t₁ … t_n に対しては、(P t₁ … t_n)_x [ t ] = P (t₁)_x [ t ] … (t_n)_x [ t ] 。
2. (¬ φ)_x [ t ] = (¬ φ_x [ t ])
3. (φ ∧ ψ)_x [ t ] = (φ_x [ t ] ∧ ψ_x [ t ])
4. (φ ∨ ψ)_x [ t ] = (φ_x [ t ] ∨ ψ_x [ t ])
5. (φ → ψ)_x [ t ] = (φ_x [ t ] → ψ_x [ t ])
6. (φ ↔ ψ)_x [ t ] = (φ_x [ t ] ↔ ψ_x [ t ])
7. (∀x φ)_x [ t ] = ∀x φ 、(∃x φ)_x [ t ] = ∃x φ 。
8. y が x と異なる変数ならば、(∀y φ)_x [ t ] = ∀y φ_x [ t ] 、(∃y φ)_x [ t ] = ∃y φ_x [ t ] 。

次に、論理式 φ において項 t が変数 x に代入可能であるということを定義する。このことの直観的な意味は、φ が x について述べていることと同じことを φ_x [ t ] が t について述べているということである。代入可能性の正式な定義は次の通りである。

論理式 φ において項 t が変数 x に代入可能 (substitutable) であるということを次のように再帰的に定義する：

1. 原子論理式においては、常に t は x に代入可能である。
2. (¬ φ) において t が x に代入可能 　⇔　 φ において t が x に代入可能 。
3. (φ ∧ ψ) において t が x に代入可能 　⇔　 φ と ψ において t が x に代入可能 。
4. (φ ∨ ψ) において t が x に代入可能 　⇔　 φ と ψ において t が x に代入可能 。
5. (φ → ψ) において t が x に代入可能 　⇔　 φ と ψ において t が x に代入可能 。
6. (φ ↔ ψ) において t が x に代入可能 　⇔　 φ と ψ において t が x に代入可能 。
7. ∀y φ において t が x に代入可能 　⇔　 x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。
8. ∃y φ において t が x に代入可能 　⇔　 x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。

等号に関する公理の 2. は、

x = y → (P t₁ … t_n → P u₁ … u_n) 　（ただし、P は n 変数述語記号で、u_i は t_i における x のいくつかを y で置き換えて得られる項である）

となっている。ここで、項 u が項 t における x のいくつかを y で置き換えて得られる項であるということは正確には次のように定義される。

変数 x と y を固定し、項の間の関係 ≈ を次のように再帰的に定義する：

1. x ≈ u 　⇔　 u = x または u = y 。
2. z が x と異なる変数ならば、z ≈ u 　⇔　 u = z 。
3. c 定数記号ならば、c ≈ u 　⇔　 u = c 。
4. t₁ , ..., t_n が項で、f がアリティ n の関数記号ならば、f t₁ … t_n ≈ u 　⇔　 t₁ ≈ u₁ , ..., t_n ≈ u_n であるような u₁ , ..., u_n が存在して u = f u₁ … u_n 。

t ≈ u であるとき、u は t における x のいくつかを y で置き換えて得られる項であるという。

文 φ が文の集合 Σ の論理的帰結であること ( ${\displaystyle \Sigma \vDash \varphi }$ ) と、φ が Σ の定理であること ( ${\displaystyle \Sigma \vdash \varphi }$ ) は全く別の仕方で定義されている。

健全性とは、Σ の定理はすべて Σ の論理的帰結であることである。

${\displaystyle \Sigma \vdash \varphi \Longrightarrow \Sigma \vDash \varphi }$

完全性とは、Σ の論理的帰結はすべて Σ の定理であることである。

${\displaystyle \Sigma \vDash \varphi \Longrightarrow \Sigma \vdash \varphi }$

古典一階述語論理は健全かつ完全である。

以下、健全性定理と完全性定理以外の重要な定理を列挙する。

1. コンパクト性定理 ： 文の集合 Σ のすべての有限部分集合がモデルを持つならば、Σ 自身もモデルを持つ。
2. レーヴェンハイム・スコーレムの定理 ： κ を無限基数とする。論理式全体の集合の濃度が κ であるような一階の言語における文の集合がモデルを持つなら、それは濃度 κ 以下のモデルも持つ。
3. 恒真論理式全体の集合は（言語にアリティ 2 以上の述語が一つでも含まれていると）決定可能でない。つまり、任意に論理式が与えられたとき、それが恒真であるか否かを判定するアルゴリズムは存在しない（「チューリングマシンの停止問題」を参照）。この結果はアロンゾ・チャーチとアラン・チューリングがそれぞれ独立に導き出した。正確には、恒真論理式のゲーデル数全体の集合は帰納的でないということである。
4. それでも、与えられた論理式が恒真であるとき、かつそのときにのみ 1 (yes) を出力して停止するアルゴリズムは存在する。ただし、恒真でない論理式を入力した場合はこのアルゴリズムは停止しないかもしれない。これを、恒真論理式全体の集合は準決定可能であるという。これは正確に述べれば、恒真論理式のゲーデル数全体の集合が帰納的可算であるということである。
5. 1 変数述語記号だけを非論理記号に持つ言語の恒真論理式全体の集合は決定可能である。

• 型つき一階述語論理は変項や項に型または種を導入したものである。型の個数が有限個であれば普通の一階述語論理と大きな違いはなく、有限個の単項述語で型を記述し、いくつかの公理を追加すればよい。真理値として Ω という特殊な型を持つ場合があるが、その場合の論理式は Ω 型の項となる。
• 弱二階述語論理は有限個の部分集合の量化を許すものである。
• 単項二階述語論理は部分集合、すなわち単項述語の量化のみを許すものである。
• 二階述語論理は部分集合および関係、すなわち全ての述語の量化を許すものである。
• 高階述語論理は述語を引数とする述語など、さらに一般化したものの量化を許す。
• 直観主義的一階述語論理は古典命題計算ではなく直観主義を導入するものである。例えば、¬¬φ は必ずしも φ と等しいとは限らない。
• 様相論理は様相演算子を追加したものである。これは、直観的に説明すれば、「～は必然的である」および「～は可能である」を意味する演算子である。
• 無限論理は無限に長い文を許す。例えば無限個の論理式の連言や選言が許されたり、無限個の変項を量化できたりする。
• 新たな量化子を加えた一階述語論理は、例えば「……であるような多くの x が存在する」といった意味の新たな量化子 Qx, ..., を持つ。

こうした論理の多くは、一階述語論理の何らかの拡張と言える。これらは、一階述語論理の論理演算子と量化子を全て含んでいて、それらの意味も同じである。リンドストレムは、一階述語論理の拡張には、レーヴェンハイム・スコーレムの下降定理とコンパクト性定理の両方を満足するものが存在しないことを示した。この定理の内容を精確に述べるには、論理が満たしていなければならない条件を数ページにわたって列挙する必要がある。例えば、言語の記号を変更しても各文の真偽が基本的に変わらないようになっていなければならない。

一階述語論理のいくぶんエキゾチックな等価物には、次のものがある。順序対構成をもつ一階述語論理は、特別な関係として順序対の射影を持つ関係代数（これはタルスキと Givant によって構築された）と精確に等価である。

• D.ヒルベルト、W.アッケルマン 著、伊藤誠^{[要曖昧さ回避]}（訳） 編『記号論理学の基礎（第３版 ）』大阪教育図書社、1954年。 

表 話 編 歴 論理学
関連項目 学術的領域 議論学 価値論 批判的思考 再帰理論 形式意味論 論理史 非形式論理学 計算機科学における論理学（英語版） 数理論理学 数学 メタ論理学 メタ数学 モデル理論 哲学的論理学 哲学 論理学の哲学 数学の哲学 証明論 集合論 論理学の歴史 基本概念 アブダクション 分析的と総合的の区別（英語版） 二律背反 アプリオリ 演繹 定義(内包と外延) 記述 帰納 推論 論理的帰結 論理形式（英語版） 論理的含意（英語版） 論理的真理 名前 必要十分条件 意味 パラドックス 可能世界論 前提 確率 理性 推理 参考 意味論 命題 サブスティトゥーション（英語版） 統語論（英語版） 真理 真理値 妥当性 数学記号の表
哲学的論理学 批判的思考と非形式論理学 分析 曖昧 信念 信用性（英語版） 根拠 説明 説明力（英語版） 事実 誤謬 探究 意見 節約 根拠 プロパガンダ 思慮分別（英語版） 推理 関連 修辞学 厳格 漠然（英語版） 論理学の哲学 構成主義 真矛盾主義 虚構主義（英語版） 有限主義（英語版） 形式主義 直観主義 論理的原子論（英語版） 論理主義 唯名論 プラトニック実在論（英語版） プラグマティズム 実在論
メタ論理学と超数学 カントールの定理 決定問題 チャーチのテーゼ 無矛盾性 実効的方法（英語版） 数学基礎論 ゲーデルの完全性定理 ゲーデルの不完全性定理 健全性 完全性 決定可能性 解釈 レーヴェンハイム-スコーレムの定理 メタ定理（英語版） 充足可能性 独立性（英語版） 独立 タイプとトークンの区別 使用と言及の区別
数理論理学 基幹 形式言語 構成規則 形式体系 演繹システム（英語版） 形式的証明 形式意味論 論理式 集合 元 クラス 古典論理 公理 自然演繹 推論規則 有限関係（英語版） 定理 論理的帰結 公理系 型理論 記号 統語論（英語版） 理論（英語版） 名辞論理学（英語版） 命題 推論 論証 妥当性 三段論法 反対の正方形 ベン図 命題論理とブール論理 ブール関数 命題論理 論理演算 真理値表 原子論理式 リテラル 述語論理 量化 全称記号 存在記号 一階述語論理 二階述語論理 高階述語論理 単項述語計算（英語版） 標準形 連言標準形 選言標準形 否定標準形 冠頭標準形 スコーレム標準形 節標準形 集合論 集合 空集合 数え上げ 外延 有限集合 関数 部分集合 冪集合 可算集合 帰納的集合 定義域 値域 順序対 非可算集合 モデル理論 モデル（英語版） 解釈（英語版） 超準モデル 有限モデル理論 真理値 妥当性 証明論 形式的証明 演繹システム（英語版） 形式体系 定理 論理的帰結 推論規則 統語論（英語版） 再帰理論 再帰 帰納的集合 帰納的可算集合 決定問題 チャーチ＝チューリングのテーゼ 計算可能関数 原始再帰関数 表現 真理値表 クワイン・マクラスキー法 カルノー図 存在グラフ 概念地図 オイラー図 ベン図 スパイダー図 タブローの方法 Xバー理論 構文木 構文解析
非古典論理 様相論理学 真理様相（英語版） 価値様相（英語版） 義務論理 信念様相（英語版） 認識論理 時相論理 線形時相論理 直観主義 直観論理 構成的解析（英語版） ハイディング算術（英語版） 直観主義型理論 構成的集合論（英語版） ファジィ論理 真理の程度（英語版） ファジィルール（英語版） ファジィ集合 ファジィ有限要素（英語版） ファジィ集合演算（英語版） 部分構造論理 構造規則（英語版） 適切さの論理 線形論理 矛盾許容論理 真矛盾主義 様相記述論理（英語版） 存在論 オントロジー言語（英語版）
論理学者 アンダーソン アリストテレス イブン・ルシュド イブン・スィーナー ベイン（英語版） バーワイズ（英語版） ベルナイス ブール ブーロス（英語版） カントール カルナップ チャーチ クリュシッポス カリー ド・モルガン フレーゲ ギーチ ゲンツェン ゲーデル ヒルベルト クリーネ クリプキ ライプニッツ レーヴェンハイム（英語版） ペアノ パース パトナム クワイン ラッセル シュレーダー（英語版） スコトゥス スコーレム スマリヤン タルスキ チューリング ホワイトヘッド オッカムのウィリアム ウィトゲンシュタイン ツェルメロ
カテゴリ