論理式内の名前の消去とイプシロン項

N君と話していて、「論理式のなかの名前は消そうと思えば消せるよ」と言ったのですが、名前とは何のことで、どうやって名前を消すかは言ってなかったので、ここに書いておきます。

内容：

モノイドの単位元

Aは集合で、m:A×A→A を写像とします。mはA上の二項演算ですね。このmは結合律を満たすとしましょう。登場する変数x, y, zなどは集合A上を走るとします。

• ∀x, y, z.(m(m(x, y), z) = m(x, m(y, z))) --- 結合律

結合律に加えて単位元が存在すれば、Aはモノイドになります。単位元を表す名前として最初からeとかを入れてもいいのですが、ここでは単位元を指す名前は用意しないとします。その代わり、単位元の存在は要請します。

• ∃y.∀x.(m(y, x) = x ∧ m(x, y) = x)

∀x.(m(y, x) = x ∧ m(x, y) = x) という論理式にUnitという名前を付けましょう。

• Unit(y) :≡ ∀x.(m(y, x) = x ∧ m(x, y) = x)

ここで、記号':≡'は、左辺の名前'Unit'を、右辺の論理式で定義するという意味です。Unitは、「単位元である」というコトに付けられた名前です。Unitを使うと、単位元の存在は、次のように簡略に書けます。

• ∃y.Unit(y)

Unitのような“コトの名前”は、構文上は述語記号になります。後から導入された述語記号は、その定義本体（':≡'の右辺）で置き換えれば消去できます。これは簡単ですね。

さて、∃y.Unit(y) から単位元の存在は保証されているので、それに名前を付けたい気分になります。単位元の名前は初めからは用意してなかったので、後から導入することになります。とりあえずはインフォーマルに：

• u := (Unit(y)であるようなy)

と書いておきましょう。名前'u'は、集合A内の特定の要素を名指す固有名詞です。つまり、モノの名前です。記号':='は、左辺の“モノの名前”を右辺の項（モノを表す表現）で定義することを示します。

モノの名前の導入と消去は、コトの名前（述語記号）より少し面倒です。準備としてイプシロン記号の話をしましょう（次節から）。

イプシロン記号

これからイプシロン記号について説明します。以下の過去記事でも説明していますので、興味があれば参照してみてください。

• イプシロン計算ってなんですかぁ？ こんなもんですよぉ
• ラムダ計算とイプシロン計算を使って線形代数の計算 -- 随伴の例

Pを変数xを含む論理式だとして、P(x)と書きましょう。εx.P(x)とは、

• 命題P(x)を満たすようなモノ

という意味です。イプシロン'ε'を前置させた式εx.P(x)は項（モノを表す表現）として使えるのでイプシロン項〈epsilon term〉と呼びます。変数xは他の変数に置き換えてもかまいません。つまり、xは束縛変数で、イプシロン記号は変数を束縛する作用を持ちます。論理の文脈でイプシロン記号といった場合は、イプシロン項を作る目的で使われる'ε'のことです。

イプシロン記号／イプシロン項は、ヒルベルト（David Hilbert）が最初に使ったらしいです。ヒルベルトのイプシロン項εx.P(x)では、P(x)に何の制限もなく勝手な論理式を許します。∃x.P(x)が偽であってもかまいません。最初に「Pは変数xを含む」と言いましたが、xを含まない場合さえも許します。

ヒルベルトのオリジナルでは、εx.P(x)のP(x)は何だっていいわけです。しかし、現実的にはP(x)に制限を加えて利用することが多いです。次の2つことを前提するのが普通でしょう。

1. 論理式Pのなかには実際に変数x（イプシロン記号の束縛変数となる変数）が出現する。
2. ∃x.P(x)は真である。

「真である」は、「証明されている」（構文論的な真）と解釈してもいいし、「実在と比較して確認済み」（意味論的な真）と解釈してもどっちでもいいです。

上記の前提のもとでは、εx.P(x)は、

• a x such that P(x)

と読めばいいでしょう。日本語なら

• P(x)であるようなxのなかのどれか

例えば、変数xが実数を表すとして、εx.(x² = 2) の意味は次のとおり。

• a x such that x² = 2
• x² = 2 であるようなxのなかのどれか

x² = 2 となるxは、√2と-√2の2つがあるので、イプシロン項の意味が一意に決まるわけではありません。

一意存在と一意イプシロン記号

イプシロン項εx.P(x)の使用条件をさらにきびしくして、次のようにしましょう。

• ∃!x.P(x)が真であるときに限り、εx.P(x)を使ってよい。

ここで出てきた∃!は、一意的な存在を意味します。つまり、

• P(x)であるようなxがただひとつだけ存在する

という条件が満たされるときに限りイプシロン項を使っていいことにします。この前提で使うイプシロン記号を特にε!と書くことにして、一意イプシロン記号と呼ぶことにします。ε!x.P(x)は一意イプシロン項です。

例えば、xは実数の変数だとして、∃!x.(x² = 2 ∧ x ≧ 0) は真なので、ε!x.(x² = 2 ∧ x ≧ 0) というイプシロン項は利用可能です。しかし、∃!x.(x² = 2) は真ではないので、ε!x.(x² = 2)という表現はイプシロン項として不適切で許されません。

我々がイプシロン項を使いたいときは、特定のモノに固有名詞を付けたいとき*1なので、このようにきびしく使用制限しても問題はないと思います。ε!x.P(x)は、

• the x such that P(x)

と読めばいいでしょう。日本語なら（"the"の感じを出すのが難しいですが）

• P(x)である、その唯一のx

ところで、∃!は新しい論理記号なのでしょうか？ そうではなくて、単なる略記です。∃!x.P(x)は次のように定義できます。

• ∃!x.P(x) :≡ ∃x.P(x) ∧ ∀x, y.(P(x)∧P(y) ⇒ x = y)

論理式が長くなるのを厭わなければ、∃!という記号を使う必要はありません。

一意イプシロン項と名前の導入

一意イプシロン項ε!x.P(x)を使う準備が出来たので、モノイドの単位元の話に戻ります。インフォーマルに書いた

• u := (Unit(y)であるようなy)

は、一意イプシロン項を使えば次のように書けます。

• u := ε!y.Unit(y)

Unitという名前（述語記号）を消したいなら、

• u := ε!y.∀x.(m(y, x) = x ∧ m(x, y) = x)

です。

一意イプシロン項を使うには、使用条件がありました。次の論理式が真であることが要求されるのでした。

• ∃!y.Unit(y)

真であることを証明により保証するなら、∃!y.Unit(y)を事前に証明しておく必要があります。∃!y.Unit(y)は次の論理式と同値です（∃!は不要でした）。

• (∃y.Unit(y)) ∧ ∀y, z.(Unit(y)∧Unit(z) ⇒ y = z)

∧の左側は最初から仮定しているので、右側の ∀y, z.(Unit(y)∧Unit(z) ⇒ y = z) だけを事前に示せばOKです。「二項演算の単位元は（もし在るならば）一意である」という命題です。練習問題としましょう。

ε!y.Unit(y)の使用条件はクリアできたので、論理式のなかでε!y.Unit(y)をそのまま、あるいは名前uとして使っていいことになります。

例えば、「集合Aの要素sを二乗したら単位元になる」というコトは、次のように書けます。

• m(s, s) = ε!y.Unit(y)
• m(s, s) = u

一意イプシロン項と名前の消去

u := ε!y.Unit(y) のようにして新しい名前（この場合は特定のモノを指す固有名詞'u'）を導入することはしばしば行われます。導入された名前は、m(s, s) = u のように論理式を書くときに使用されます。

新しい名前を導入した時点で、論理系で使える記号セット（ボキャブラリ）は増えています。もとの論理系とは変わっています。もとの論理系では許されなかった（解釈不能な）項や論理式が認められるようになっていますからね。

では、拡張されたボキャブラリで書かれた論理式をもとの論理系に戻すにはどうしたらいいでしょうか？ 一意イプシロン項や導入された名前を論理式から追い出す必要があります。もちろん、論理式の意味が変わらないように書き換えるのです。

一般に、P(ε!x.P(x))は成立します。別な言い方をすると、ε!x.P(x)を使い始める時点で、P(ε!x.P(x))という命題（論理式）も使っていい仮定に登録されます。例えば、ε!x.(x² = 2 ∧ x ≧ 0) を使うときは、次の命題は真だと仮定しています。

• ε!x.(x² = 2 ∧ x ≧ 0)² = 2 ∧ ε!x.(x² = 2 ∧ x ≧ 0) ≧ 0

ウヒャ、ゴチャゴチャで見にくい。通常は、生のイプシロン項は見にくいので名前で代用するわけです。

• r := ε!x.(x² = 2 ∧ x ≧ 0)
• r² = 2 ∧ r ≧ 0

さらには、単なる英字じゃない特別な記号を準備して、

• √2 := ε!x.(x² = 2 ∧ x ≧ 0)
• (√2)² = 2 ∧ √2 ≧ 0

モノイドの単位元の例では：

• u := ε!y.Unit(y)
• Unit(u)

Unit(u)を展開するなら：

• u := ε!y.∀x.(m(y, x) = x ∧ m(x, y) = x)
• ∀x.(m(u, x) = x ∧ m(x, u) = x)

一般的には、αを導入された名前（固有名詞）として：

• α := ε!x.P(x)
• P(α)

さて、命題Qのなかに名前αが含まれるとして、これをQ(α)と書きましょう。Qから名前αを消去することが問題でした。αの消去には、Q(α)を次のように書き換えます。

• ∀x.(P(x) ⇒ Q(x))

Q(α)に出現するαは、P(α)として規定されるものでした。つまり、

• P(α)である、そんなαに対して、Q(α)

と主張しています。一意イプシロン項の使用条件から、「P(α)であるα」は一意的なので、変数xを使って「P(x)であるx」と言っても確実に特定物を指します。結局、

• P(x)である、そんなxに対して、Q(x)

と言っても同じで、言い回しを変えれば（意味は変わらない）、

• xがP(x)を満たすようなxならば、Q(x)

あるいは、

• P(x)を満たすようなどんなx（実は1つしかない）に対してもQ(x)

これを論理式で書けば ∀x.(P(x) ⇒ Q(x)) ですね。

モノイドの単位元uを使った m(s, s) = u という論理式からuを消去してみましょう。次のようになります。

• ∀x.(Unit(x) ⇒ m(s, s) = x)

Unitも消去するならば：

• ∀y.(∀x.(m(y, x) = x ∧ m(x, y) = x) ⇒ m(s, s) = y)

混乱を避けるために束縛変数の名付けを調整しています。

0と1を定義してみよう

ここから先は、半形式的（semi-formal）な集合論を使います。半形式的とは、公理的集合論の公理を採用するが、記述や証明はインフォーマルというスタイルのことです。

集合概念だけから、自然数0と1を定義してみます。

まず、集合論の公理から空集合の存在は保証されます。

• ∃y.∀x.¬(x∈y)

空集合の一意性 ∃!y.∀x.¬(x∈y) が証明できるので、一意イプシロン項ε!y.∀x.¬(x∈y)は使用可能です。新しい名前'0'を導入しましょう。

• 0 := ε!y.∀x.¬(x∈y)

これで、自然数0を空集合として定義できました。1は次のように定義します。

• 1 := {0}

中括弧記法に頼らないでやってみます。単元集合の存在は次の定理（公理と思ってもいいです）で保証されます。

• ∀x.(∃!y.(x∈y ∧ ∀z, w.(z∈y∧w∈y ⇒ z = w)))

0に対して、0だけを含む単元集合の存在は、上記命題の特殊ケースで：

• ∃!y.(0∈y ∧ ∀z, w.(z∈y∧w∈y ⇒ z = w))

これは、一意イプシロン項ε!y.(0∈y ∧ ∀z, w.(z∈y∧w∈y ⇒ z = w))の使用条件（使用してよい根拠）になります。このイプシロン項により、新しい名前'1'を導入します。

• 1 := ε!y.(0∈y ∧ ∀z, w.(z∈y∧w∈y ⇒ z = w))

1の定義のなかに出現する名前0を消去するには、前節の書き換えを実行すればいいので、

• 1 := ε!y.(∀x.[∀t.¬(t∈x) ⇒ (x∈y ∧ ∀z, w.[z∈y∧w∈y ⇒ z = w])])

丸括弧と角括弧を併用しているのは単に見やすさのためです。束縛変数の名付けは調整しています。

イチの定義がこれではたまらんなー。まー、普通はこんなことはしませんからご安心を。自然数の概念と数詞（数を指す固有名詞）くらいは自由に使えないと、実際やってられません。

しかし、後から導入された名前は、“コトの名前”にしろ“モノの名前”にしろ消去できることは知っておいてもいいでしょう。

*1:PがP(x, y)のように複数の変数を含むときは、ε!y.P(x, y)は、xを与えてyを返す関数を定義します。関数を定義する目的でイプシロン項を使うこともあります。