述語論理

Last-modified: Sat, 29 Apr 2017 10:13:24 JST (2551d)
Top > 述語論理
第2章 自然数の定式化へ戻る。

公理的集合論は述語論理という分野と切り離せない関係にあるので、まずは述語論理の概要について説明します。述語論理を詳述するにはそれなりのページ数が必要で、かつ極めて抽象的になってしまうため、ここではごく一部を雑に概説するに留めます。詳細については、例えばエルフ数学をご覧下さい。

述語論理というのは、数学で採用される基本的な論理の1つです。述語論理には最も基本的な1階述語論理と、その他の2階述語論理を始めとする高階述語論理というものがありますが、Encyclopedia of \( P \)-adic Numbersでは1階述語論理のみを扱いますので、それを単に述語論理と呼ぶことにします。

一言に述語論理と言っても色々な枠組みがありまして、例えばこの第2章で説明していく「公理的集合論」は1つの述語論理の枠組みですし、他にも「ペアノ算術」や「実数論」といった述語論理の枠組みがあります。そういった述語論理の数々の枠組みに共通することは、「論理式」または「命題」と呼ばれる、特別な文章を考えることです。

実は数学にも文法の概念があり、論理式という概念は述語論理の文法を用いて厳密に定義することが出来ます。具体的には、「形式言語」という概念を用いて、どのような文字列を論理式として許容するか定義します。その詳細は

を参照して下さい。ここでは形式言語については触れず、大雑把に述語論理の文法を説明していきます。

ちなみに公理的集合論にも色々な体系がありまして、通常の数学で最も多く使われる「ZFC公理系」の他にも、「NBG公理系」というものがあります。ZFC公理系もかなり汎用性が高いのですが、ZFC公理系を記述する形式言語では「集合」という概念しか扱えず、「圏」という重要な概念を記述するには表現力がやや不満なものとなります。対してNBG公理系を記述する形式言語では集合より汎用性の高い概念である「クラス」を扱うことが出来るので、圏の記述に十分な表現力を持ちます。そこでEncyclopedia of \( P \)-adic NumbersではNBG公理系と同様な形式言語を用いて表現力を補いつつも、NBG公理系そのものに踏み入ることはせずZFC公理系の理論を少しだけクラスに拡張して用いていくことにします((クラスを用いる公理的集合論はしばしば1階述語論理より広い2階述語論理を用いることがありますが、



論理式の構文

まず英語等の言語で現れる構文の典型例として、「主語 述語 目的語」の形で書かれる「SVO」構文がありました。述語には動詞に類するものが入りますし、主語と目的語には名詞に類するものが入ります。述語論理でも同様に、述語と名詞に類するものを考えて文法を定義します。

数学の述語には、等号\( = \)や不等号\( \neq \)\( \leq \)\( \geq \)\( < \)\( > \)等があります。これらは述語論理の文法において述語として扱われます。

数学の名詞には、「数」や「ベクトル」や「集合」や「関数」が挙げられます。述語論理ではこういった名詞的な概念をまとめて、項(term)と呼びます*1。また、一言に「数」と言っても、特定の1つの数を表す\( 0{} \)\( 1 \)や円周率\( \pi \)や自然対数の底\( e \)のような「定数」と、特定の数を表さず色々な数を代入できる「変数」の2種類があります。同様に、特定の1つの項を表すものを定項(constant term)、特定の項を表さず色々な項を代入できるものを変項(variable term)と呼びます。この他、いくつかの項を組み合わせて新たな項を作る関数記号(function symbol)というものがありますが、後で述べるように公理的集合論では関数記号が現れないので、詳細の説明は避けます。

述語論理のどの枠組みを考えるかによって、項の呼び方が変わります。例えばペアノ算術においては「自然数」という呼び方をすることがありますし、実数論においては「実数」と呼ぶことがあります。そしてZFC公理系に基づく公理的集合論においては項のことを集合(set)と呼びますし、NBG公理系に基づく公理的集合論においては項のことをクラス(class)と呼びます。これらはあくまで単なる呼び方であり、自然数を定義する前に項を自然数と呼ぶことは循環論法でも何でもありません。

例えば「自然数」や「関数」は集合の典型例として公理的集合論の中でも定式化されますし、「自然数の集まり」や「関数の集まり」や「数列」や「図形」も集合になります。この意味の自然数は定義を持つ用語ですので、ペアノ算術の項の呼び名である自然数とは似て非なるものです。しかしながら、集合としての自然数にもペアノ算術の理論が適用可能であることが示せるため、一度定義してしまえば、それらをあまり区別せず呼ぶことが慣例です。

また述語論理のどの枠組みを考えるかによって、形式言語に許容される項や述語の種類に制限が掛かります。例えばペアノ算術においては、変項以外に\( 0{} \)という定項を用いますし、関数記号としては主に、自然数\( n \)の次の自然数を表す\( S(n) \)、自然数\( n \)\( m \)の和を表す\( +(n,m) \)、自然数\( n \)\( m \)の積を表す\( \times(n,m) \)の3つが用いられます。実は\( + \)\( \times \)の2つは\( S \)を用いる「再帰」という方法によって後で定義し直すことが可能なので、\( + \)\( \times \)を関数記号として採用する必要はありません。同様に\( 1 \)という項を用いることがありますが、これは\( S(0) \)のこととして後で定義し直すことが可能なので、最初から形式言語の段階で与えて定項は\( 0{} \)のみで十分となります((もちろん

形式言語における定項というのはただの定数概念を表す記号というよりは、定数を表す記号として最初から与えておく必要性の高い概念だと思った方が分かりやすいかもしれません。例えば\( 0{} \)は「ペアノの公理」というペアノ算術の骨格の記述に必要であるため、定項として記号を与えておく必要があります。別の定項等を用いて後で定義し直せるものは、最初から定項として記号を用意しておく必要がないのです。そうでないと、\( 0{} \)\( 1 \)\( 2 \)\( 2 \times 2 \)\( (1 + 2) \times 2 + (2 + 1 + 2) \times (1 + 2 + 1) \)も定数なので個別に記号が必要、となってしまいますが、公理系を記述するために必要のない記号を形式言語の段階で指定しておくのは少し冗長であると言えましょう*2。ちなみに最初から形式言語の中に与えていない記号を後から定義して導入することの正当化については、

を参照して下さい。

それを踏まえまして、実は公理的集合論の項には変項しかありません。定項も関数記号も最初から記号を用意する必要ないので用いないのです。「空集合」という概念を知っている人は「\( \emptyset \)という定項が必要じゃないか」と思うかもしれませんが、空集合は\( \in \)や他の\( \forall \)等の記号を用いて後で定義し直せるので、最初から記号として\( \emptyset \)を用意しておく必要はないのです。また公理的集合論の中でもペアノ算術を適用可能な自然数概念を定式化して扱うと書きましたが、ペアノ算術の関数記号の代わりになるものが公理的集合論の中では「写像」という集合を用いて具体的に構成されるため、関数記号を最初から用意する必要はありません。

述語に関しては、ペアノ算術や実数論では\( = \)\( < \)\( > \)\( \leq \)\( \geq \)を用いることが一般的ですが、その中でも\( = \)さえ述語として許容しておけば、残りの述語は\( = \)と他の\( \exists \)等の記号を組み合わせて等価なものに翻訳し直して定義できますので、述語として採用する必要がありません。同様に、公理的集合論においては\( = \)\( \in \)という述語が主に用いられますが、Encyclopedia of \( P \)-adic Numbersでは集合間の等式を文字としてのメタな等式と区別する*3ために、\( \in \)のみを用いることにします。もちろん等号や不等号もあった方が便利なので、それらは全てこの\( \in \)を用いて翻訳し直して定義を与えます。

述語論理においては、文*4として「項 述語 項」という構文のみを許容することにします。このような文や、矛盾を表す記号\( \perp \)原子式(atomic formula)*5と呼びます。例えば公理的集合論においては項がクラスであり、述語は\( \in \)に他ならないので、クラス\( A \)とクラス\( x \)を用いて表される文\( x \in A \)は原子式となります。それに対して\( Ax \in \)\( x \in \in A \)のような文字列は許容される構文を持たないので、原子式ではありません。

さて、複数の原子式を組み合わせて新しい文を作りましょう。ただし単純に原子式を並べるだけではなく、やはり述語論理の文法に沿った組み合わせ方のみを許容します。具体的には、論理演算子(logical operator)と呼ばれる4つの記号\( \wedge \)\( \vee \)\( \neg \)\( \to \)と、量化子(quantifier)と呼ばれる2つの記号\( \forall \)\( \exists \)と、補助的なカッコ記号\( ( \)\( ) \)を使って以下の規則で表される有限の長さの文のみを論理式(logical formula)と呼び、許容します。

(1) 原子式
(2) (論理式) \( \wedge \) (論理式)
(3) (論理式) \( \vee \) (論理式)
(4) \( \neg \)(論理式)
(5) (論理式) \( \to \) (論理式)
(6) \( \forall x \)(論理式)
(7) \( \exists x \)(論理式)

ただし(6)と(7)における\( x \)は変項です。典型的には\( \forall x \)\( \exists x \)に続く論理式に\( x \)が現れますが、必ずしも\( x \)が現れなくても良いです。論理式の定義に論理式が入っていますが、これは循環論法ではなく再帰的*6な定義であるだけです。文の長さを有限に限っているので、与えられた文字列が論理式であるかか否かを計算機で判定することができます。

例えば公理的集合論において、2つのクラス\( A \)\( B \)を用いて表される文\( (A \in B) \wedge ( (B \in A) \to (A \in B) ) \)は論理式です。実際、(1)から\( A \in B \)\( B \in A \)は論理式であり、(5)から\( (B \in A) \to (A \in B) \)は論理式であり、(2)から\( (A \in B) \wedge ( (B \in A) \to (A \in B) ) \)は論理式であることが分かります。それに対して、文字列\( \vee (A \in B) \)\( (A \in B) \to \)\( (A \in B) \neg (B \in A) \)は(1)~(7)の構成を繰り返しても得られないため、論理式ではないことが分かります。

ここで、2つの論理式\( \Phi \)\( \Psi \)に対し、\( \Phi \wedge \Psi \)を「\( \Phi \)かつ\( \Psi \)\( \Phi \)and \( \Psi \))」、\( \vee \)を「\( \Phi \)または\( \Psi \)\( \Phi \)or \( \Psi \))」、\( \neg(\Phi) \)を「\( \Phi \)でない(not \( \Phi \))」、\( \Phi \to \Psi \)を「\( \Phi \)ならば\( \Psi \)(if \( \Phi \), then \( \Psi \))」等のように読んだり書いたりすることにします。また、「等のように読んだり書いたりする」という言い回しが長いので、今後はそれを単に「と読む」と表記します。この流儀において、\( (\Phi \to \Psi) \wedge (\Psi \to \Phi) \)という論理式は「\( \Phi \)ならば\( \Psi \)、かつ\( \Psi \)ならば\( \Phi \)」と読むことになりますが、これは長いので単に「\( \Phi \)\( \Psi \)は同値である」と読むことにします。

また、変項\( x \)と論理式\( \Phi \)に対し、\( \forall x(\Phi) \)を「任意の\( x \)に対し、\( \Phi \)である」と、\( \exists x(\Phi) \)を「\( \Phi \)を満たすような\( x \)が存在する」や「ある\( x \)が存在して\( \Phi \)を満たす」と読むことにします。更に、「任意の\( x \)に対し、任意の\( X \)に対し」のように同じ量化子が並ぶ場合は、「任意の\( x \)\( X \)に対し」のように略記することにします。

与えられたクラス\( A \)に対して、\( \forall x( (x \in A) \to (\Phi) ) \)\( \forall x \in A, \Phi \)と略記し、「任意の\( x \in A \)に対し、\( \Phi \)である」と読むことにします。論理式の略記の正確な意味については、次を参照して下さい。

同様に、\( \exists x( (x \in A) \wedge (\Phi) ) \)\( \exists x \in A, \Phi \)と略記し、「\( \Phi \)を満たすような\( x \in A \)が存在する」や「ある\( x \in A \)が存在して\( \Phi \)を満たす」と読むことにします。\( \forall x \in A \)\( \exists x \in A \)の形の文字列を、有界な量化と呼びます。

また論理式の再帰的定義のうち、(6)と(7)を

(6)' \( \forall x \in A, \)論理式
(7)' \( \exists x \in A, \)論理式

に変えて得られる概念のことを量化の有界な論理式と呼びます。ただし、(6)'と(7)'における\( x \)は変項です。(6)'と(7)'は(6)と(7)の特別な場合なので、量化の有界な論理式は論理式の特別なものとなります。例えば\( \forall x \in X, y \in x \)は量化の有界な論理式ですが、\( \exists X (\forall x \in X, y \in x) \)\( \exists X \)部分が有界な量化で表記できないため量化の有界な論理式ではない論理式となります。



変項への代入

2つの論理式\( \Phi \)\( \Psi \)に対し、\( \Psi \)\( \Phi \)の部分式(subformula)であるとは、連続した文字列として\( \Phi \)\( \Psi \)を含んでいるということとして定義します。変項\( x \)に対し、ここだけの用語として、\( \Phi \)\( x \)に関する量化式であるとは、\( \Phi \)\( \forall x(\Psi) \)\( \exists x(\Psi) \)のいずれかの論理式と文字列として一致するような部分式\( \Psi \)を持つということとして定義します。\( \Psi \)\( \Phi \)\( x \)に関する量化部分式であるとは、\( \Psi \)\( \Phi \)の部分式でありかつ\( x \)に関する量化式であることとして定義します。例えば\( \forall x(x \in X) \)\( (\forall x(x \in X) ) \wedge (x \in Y) \)\( x \)に関する量化部分式ですが、\( \forall x( (x \in X) \wedge (x \in Y) ) \)\( x \)に関する量化部分式ではありません。

変項\( x \)に対して、与えられた論理式\( \Phi \)から\( x \)に関する量化式\( \forall x(\Phi) \)\( \exists x(\Phi) \)を作る行為を「\( x \)について\( \Phi \)を閉じる」等のように表したりします。それを踏まえて論理式\( \Phi \)閉論理式であるとは、いかなる変項\( x \)も、\( \Phi \)の中に\( x \)が現れるのは\( \Phi \)\( x \)に関する量化部分式の中に現れる時に限る*7ということとして定義します。漠然とした意味としては、閉論理式は自由に項を代入できるような変項を持たない論理式ということです。例えば変項\( x \)\( X \)を含む論理式\( \forall x(\forall X (x \in X) ) \)や変項\( x \)を含む論理式\( \forall x( (x \in x) \vee (\neg(\exists x(x \in x) ) ) ) \)は閉論理式ですが、変項\( x \)\( X \)を含む論理式\( \forall x(x \in X) \)\( X \)に自由に項を代入できる)や変項\( x \)を含む論理式\( (x \in x) \vee (\neg(\exists x(x \in x) ) ) \)\( \vee \)の左側の\( x \)には自由に項を代入できる)は閉論理式ではありません。閉論理式には自由に項を代入できる変項がないため、「意味」の確定した文になります。

また、「論理式\( \Phi(x) \)に対し」と書くことがあります。これは直前の文脈で既に\( x \)という変項が使われている時は「論理式\( \Phi \)に対し」という意味ですし、そうでない時は「変項\( x \)と論理式\( \Phi \)に対し」という意味です。何故このような記法を用意するかと言うと、\( \Phi \)の中の自由変項\( x \)に項\( t \)を代入して得られる論理式を\( \Phi(t) \)と書くためです。つまり「論理式\( \Phi(x) \)に対し」と書く時は「今後\( \Phi \)の中の自由変項\( x \)に別の項を代入することがある」ということを表すことがあるということです。もちろん、単に「\( \Phi \)の中に自由変項\( x \)があるかもしれない」ということを表していたりすることもあります。

変項に項を代入する操作の定義については以下を参照して下さい。

論理式という概念が原子式から再帰的に定義されていたことと同様に、変項への項の代入という概念も原子式から再帰的に定義されます。このことから、代入操作は計算機にアルゴリズムとして実装することが出来ます。



論理式の証明可能性

さて、論理式には「証明可能」であるという概念があります。証明可能性を説明するには演繹規則という概念について述べなくてはならず、その詳細にはまたそれなりのページ数が必要になってしまいます。ここでは漠然と「論理式\( \Phi \)を仮定すれば論理式\( \Psi \)を帰結できる」ということを「\( \Phi \)の下で\( \Psi \)が証明可能である」と表し*8、「論理式\( \Phi \)を仮定すれば論理式\( \neg(\Psi) \)を帰結できる」ということを「\( \Phi \)の下で\( \Psi \)が反証可能である」と表します*9

それでは仮定から帰結できる論理式の簡単な例を挙げておきます。

例1(演繹規則の例)
(1) \( \Phi \)\( \Psi \)の両方を仮定すれば\( (\Phi) \wedge (\Psi) \)を帰結できる(("この規則を
(2) \( (\Phi) \wedge (\Psi) \)を仮定すれば\( \Phi \)\( \Psi \)の両方を帰結できる(("この規則を
(3) \( \Phi \)\( \Psi \)の少なくとも一方を仮定すれば\( (\Phi) \vee (\Psi) \)を帰結できる(("この規則を
(4) 「\( \Phi_1 \)を仮定すれば\( \Psi \)を帰結できる」ということと「\( \Phi_2 \)を仮定すれば\( \Psi \)を帰結できる」ということの両方を仮定すれば「\( (\Phi_1) \vee (\Phi_2) \)を仮定すれば\( \Psi \)を帰結できる」ということを帰結できる(("この規則を
(5) \( (\Phi) \wedge (\neg(\Phi) ) \)を仮定すれば\( \perp \)を帰結できる(("この規則を
(6) \( \perp \)を仮定すれば\( \Phi \)を帰結できる(("この規則を
(7) 「\( \Phi \)を仮定すれば\( \perp \)を帰結できる(つまり矛盾する)」ということを仮定すれば\( \neg(\Phi) \)を帰結できる(("この規則を

論理式\( \neg(\Phi) \)のように極端に単純な例を除くと、論理式の多くは何かを仮定しないと帰結することが出来ません。そこで、他の仮定なく帰結しても良いものを予め決めておき、それらを公理と呼びます。述語論理全般における公理にも色々なものがありますが、それらを1つずつ解説するにはやはりそれなりのページ数が必要となるので、ここでは公理的集合論において\( \in \)に課される重要な公理を紹介します。

公理2(排中律)
任意の\( x \)\( X \)に対し、\( x \in X \)であるまたは\( x \in X \)でない((論理式で書くと、

論理式の定義と演繹規則の例(7)から、この公理の下ではいかなる論理式\( \Phi \)に対しても仮定なしで\( \Phi \vee (\neg(\Phi)) \)が証明可能になります*10。排中律は「ある意味で」背理法と等価であり、とても強力な公理です。詳しくは以下をご覧下さい。

論理式\( \Phi \)が証明可能である時、単に「\( \Phi \)が成り立つ」と言うことにします。また論理式\( \Phi(X) \)とクラス\( A \)に対し、\( \Phi(A) \)が成り立つ時、単に「\( A \)\( \Phi \)を満たす」と言うことにします。「成り立つ」や「満たす」は文脈によって様々な流儀がありますので、他の文献を読む時の流儀の違いには注意しましょう。

さて、述語論理についての概要はこのくらいにして、公理的集合論に移ろうと思います。まずは公理的集合論で扱うクラスの中で、特に主役として活躍する「集合」という概念を定義していきます。




*1 通常は各種アルファベット(&mathjax{0, 1, 2, 3, 4, 5, 6, 7, 8, 9};)やそれらを組み合わせたり少しいじったりして作られているような見た目の記号(&mathjax{10, 2^3, 2x, -a, c_0, f(x), \beta_{\gamma}, \sin, \cos, \exp};)等が用いられます。人によっては漢字やひらがなを使うこともあります。
*2 もちろん全ての定数に対して最初から記号を与えておいても問題はありません。
*3 例えば&mathjax{A};という文字と&mathjax{B};という文字は異なる記号であるので、記号そのものとしては&mathjax{A};と&mathjax{B};が等号で結ばれません。
*4 後に述べる「閉論理式」の意味で「文」という用語を使うこともありますが、ここでは広く文字列の意味として下さい。
*5 化学とは関係がありません。
*6 再帰的(recursive)であるということ。
*7 &mathjax{x_0};等の見た目が似通った別の文字が現れることは&mathjax{x};が現れることと関係がありません。
*8 何も仮定する必要がない場合や、仮定が前提として紛れるおそれがない場合は、単に「&mathjax{\neg(\Psi)};を帰結できる」と言います。
*9 何も仮定する必要がない場合や、仮定が前提として紛れるおそれがない場合は、単に「&mathjax{\neg(\Psi)};を帰結させる行為を「反証する」と言います。
*10 「&mathjax{\neg(\Phi)};のいずれか一方が証明可能である」ということは明確に異なります。[[演繹規則の例(3)>#true]]により後者から前者は従いますが、前者から後者は従いません。