[記号論理学]McCuneの群のSingle Axiom について

田中一之先生の『数学基礎論序説』が裳華房より刊行された。

数学基礎論序説: 数の体系への論理的アプローチ

数学基礎論序説: 数の体系への論理的アプローチ

懲りもせず買ってしまったわけだが、早くも9ページにて停止した。参考としてマッキューン(McCune)の公理というものが紹介されており、群の3つの公理をひとつの公理(Single Axiom)にまとめてしまうというなかなか楽しそうなネタである。具体的にしめせば、

(w({(x^{-1}w)^{-1}}z))({(yz)^{-1}}y)=x

とかなり複雑。もちろん結合律、左単位元、左逆元の公理はこれから導かれるため、証明されるまでは途中の変形で使ってはいけない。積も逆元の記号もただの関数記号であり、それらの性質は証明されるまで使ってはいけない。この式の変数に何かを入れたり、積を作ってみたりしたものを再度この式を適用して変形していくという方法しかないのだが、ちょっと手で試してみたが、かなり手ごわい。なにかヒントはないかと、McCuneでぐぐってみたところ、この先生は計算機による自動証明の論文を書いておられ、自身でOTTERという計算ソフトを作っているような方である。計算機を使って、力ずくでいろいろな代数の公理系でSingle Axiomを探しているようなことをされている。田中テキストでは1996年の結果となっていたが、これにぴったりの論文はなかった。そこでMcCune先生の1995年の『Single Axioms for Groups and Abelian Groups with Various Operations』という文献を参考にしてみた。この文献中でもいろいろな結果はOTTERによる自動証明に拠っているが、上記のSingle Axiomとまったく同じものはなく、これは自分でOTTERを使ってやるしかないようだ。


幸いOTTERはネット上で配布されており、Windows環境で動くものもあった。マニュアルによると Knuth-Bendix のアルゴリズムにもとづいて、公理のリストとそこから証明したいステートメントの否定を合わせたものから矛盾を引き出すという計算をやるようである。使い方もいまひとつわからんので、さっそく練習として、中に入っているサンプルファイルgroup.inを参考にして群の公理を

ex=x
{x^{-1}}x=e
(xy)z=x(yz)
として、x{x^{-1}}=e を証明させてみた。

インプットファイルに公理系と最後に証明したい文の否定を入れて
----------------------------------------
set(auto).
list(usable).
x = x.
f(e,x) = x.
f(g(x),x) = e.
f(f(x,y),z) = f(x,f(y,z)).
f(x,g(x)) != e.
end_of_list.
----------------------------------------

とすると、証明として次のようなものが出力された。


---------------- PROOF ----------------
1 f(x,g(x))!=e.
4,3 f(e,x)=x.
5 f(g(x),x)=e.
7 f(f(x,y),z)=f(x,f(y,z)).
9 [para_from,3.1.1,1.1.1] g(e)!=e.
10 [para_into,7.1.1.1,5.1.1,demod,4,flip.1] f(g(x),f(x,y))=y.
14,13 [para_into,10.1.1.2,10.1.1] f(g(g(x)),y)=f(x,y).
17 [para_into,10.1.1.2,5.1.1,demod,14] f(x,e)=x.
21 [para_into,17.1.1,5.1.1,flip.1] g(e)=e.
23 [binary,21.1,9.1] $F.
------------ end of proof -------------

横の数字と括弧の中の数字で計算機が式変形をどうやったかわかるようだが、マニュアルを読んでもよくわからんので適当に解釈すると、x{x^{-1}}\neq exeを代入するとe{e^{-1}}\neq eだが ex=xより左辺を整理して、{e^{-1}}\neq eを得る。
一方、(xy)z=x(yz)xx^{-1}, yx, zyを同時に代入すると、({x^{-1}x})y={x^{-1}}(xy)を得る。左辺は({x^{-1}x})y=ey=y なので {x^{-1}}(xy)=y. さらにこのxx^{-1}yxyを同時に代入すると左辺が ({{x^{-1}})^{-1}}({x^{-1}}(xy))={(x^{-1})^{-1}}yとなり、{({x^{-1}})^{-1}}y=xy. これにy{x^{-1}}xを代入すると {({x^{-1}})^{-1}}({x^{-1}}x)=x({x^{-1}}x).
左辺はx、右辺はxeとなるため、xe=x. これのxe^{-1}を代入すると {e^{-1}}e={e^{-1}}.
左辺は公理よりeとなり、e = {e^{-1}} が得られるが、これは先の {e^{-1}}\neq e に矛盾している。

Q.E.D. 証明完了...ってこれダメじゃん。なぜダメなのかというとこれは \exists x(xx^{-1}=e)の証明であって、\forall x(xx^{-1}=e)の証明ではないからである(上記の証明で{e^{-1}}\neq eを導出した時点でもうアウト)。
確かにインプットの最後に加えた否定文は\exists x(x{x^{-1}}=e)の否定であるところの\forall x(x{x^{-1}}\neq e)を意味するものであった。

そこでたぶんxを定数っぽいaに置き換えてたらうまくいくんじゃないかという安直な発想で f(x,g(x)) != e. を f(a,g(a)) != e. に置き換えて再度OTTERを走らせてみた。その結果はこれである。

---------------- PROOF ----------------
1 f(a,g(a))!=e.
4,3 f(e,x)=x.
5 f(g(x),x)=e.
7 f(f(x,y),z)=f(x,f(y,z)).
9 [para_into,7.1.1.1,5.1.1,demod,4,flip.1] f(g(x),f(x,y))=y.
11 [para_into,9.1.1.2,9.1.1] f(g(g(x)),y)=f(x,y).
21 [para_into,11.1.1,5.1.1,flip.1] f(x,g(x))=e.
23 [binary,21.1,1.1] $F.
------------ end of proof -------------

なんかさっきより短いが、証明したい事が強くなったのでより探索条件が狭まったためと推察される。まあ、それはさておき、解釈してみよう。
{x^{-1}}(xy)=yの導出と{({x^{-1}})^{-1}}y=xyの導出は同様。後者の式のyx^{-1}を代入すると左辺は e 、右辺は x{x^{-1}}となるため、確かにこれは証明となっている。

しめしめである。そこでいよいよSingle axiom の証明をさせてみる。Single axiomに標準の群の公理のひとつの否定を加えたものの証明を計算させるのである。たぶん最初に結合律をやらせるのがよいだろうという直感から

----------------------------------------
set(auto).
list(usable).
x=x.
f(f(w,f(g(f(g(x),w)),z)),f(g(f(y,z)),y))=x.
f(a,f(b,c)) != f(f(a,b),c).
end_of_list.
----------------------------------------


でやってみた。結果、証明成功! 証明は次のようである。

---------------- PROOF ----------------
1 f(a,f(b,c))!=f(f(a,b),c).
2 [copy,1,flip.1] f(f(a,b),c)!=f(a,f(b,c)).
4 f(f(x,f(g(f(g(y),x)),z)),f(g(f(u,z)),u))=y.
6 [para_into,4.1.1.2.1.1,4.1.1] f(f(x,f(g(f(g(y),x)),f(g(f(z,u)),z))),f(g(v),f(w,f(g(f(g(v),w)),u))))=y.
12 [para_into,6.1.1.2.2,6.1.1] f(f(x,f(g(f(g(y),x)),f(g(f(z,f(u,f(g(f(g(f(g(v),f(w,f(g(f(g(v6),w)),f(g(f(v7,v8)),v7))))),u)),v8)))),z))),f(g(v),v6))=y.
14 [para_from,6.1.1,4.1.1.1] f(x,f(g(f(y,f(z,f(g(f(g(f(g(u),f(v,f(g(f(g(x),v)),f(g(f(w,v6)),w))))),z)),v6)))),y))=u.
114 [para_into,12.1.1.1.2,14.1.1] f(f(x,y),f(g(y),g(f(g(z),x))))=z.
124 [para_into,114.1.1.1,114.1.1] f(x,f(g(f(g(y),g(f(g(x),z)))),g(f(g(u),f(z,y)))))=u.
136 [para_into,114.1.1.1,4.1.1] f(x,f(g(f(g(f(y,z)),y)),g(f(g(u),f(v,f(g(f(g(x),v)),z))))))=u.
177,176 [para_from,124.1.1,114.1.1.2.2.1] f(f(f(g(f(g(x),g(f(g(g(y)),z)))),g(f(g(u),f(z,x)))),v),f(g(v),g(u)))=y.
312 [para_from,136.1.1,4.1.1.1] f(x,f(g(f(y,g(f(g(x),f(z,f(g(f(g(u),z)),v)))))),y))=f(u,v).
491 [para_into,312.1.1.2.1.1.2.1.2,136.1.1] f(x,f(g(f(y,g(f(g(x),z)))),y))=f(f(u,v),g(f(g(z),f(w,f(g(f(g(u),w)),v))))).
1138,1137 [para_into,491.1.1,312.1.1,flip.1] f(f(x,y),g(f(g(f(z,f(g(f(g(u),z)),v))),f(w,f(g(f(g(x),w)),y)))))=f(u,v).
1395 [para_from,1137.1.1,491.1.1.2.1.1,demod,1138] f(f(x,f(g(f(g(y),x)),z)),f(g(f(y,z)),f(u,v)))=f(u,v).
1445 [para_into,1395.1.1.2.2,176.1.1,demod,177] f(f(x,f(g(f(g(y),x)),z)),f(g(f(y,z)),u))=u.
1453,1452 [para_into,1395.1.1,6.1.1,flip.1] f(x,f(g(f(g(f(y,f(g(f(z,u)),z))),x)),u))=y.
1579 [para_from,1452.1.1,1445.1.1.1] f(x,f(g(f(f(x,f(g(f(y,z)),y)),z)),u))=u.
1623 [para_into,1579.1.1.2.1.1,1445.1.1] f(f(g(f(x,g(x))),y),f(g(y),z))=z.
1625 [para_into,1579.1.1.2.1.1,4.1.1] f(f(g(f(x,g(y))),x),f(g(y),z))=z.
1739,1738 [para_into,1623.1.1,136.1.1,demod,1453,flip.1] g(f(g(x),g(f(y,g(y)))))=x.
1891 [para_into,1625.1.1.1.1.1.2,1738.1.1,demod,1739] f(f(g(f(x,y)),x),f(y,z))=z.
1896,1895 [para_into,1625.1.1.1.1,1738.1.1] f(f(x,g(x)),f(g(f(y,g(y))),z))=z.
1944,1943 [para_into,1891.1.1.2,1445.1.1] f(f(g(f(x,f(y,f(g(f(g(z),y)),u)))),x),v)=f(g(f(z,u)),v).
1952 [para_into,1891.1.1.2,4.1.1,demod,1944] f(g(f(x,y)),x)=f(g(f(z,y)),z).
2049 [para_from,1952.1.1,136.1.1.2.2.1] f(x,f(g(f(g(f(y,z)),y)),g(f(g(f(u,v)),u))))=f(f(w,f(g(f(g(x),w)),z)),v).
2050 [para_from,1952.1.1,136.1.1.2.2.1.2.2] f(x,f(g(f(g(f(y,g(x))),y)),g(f(g(z),f(u,f(g(f(v,u)),v))))))=z.
2103 [copy,2049,flip.1] f(f(x,f(g(f(g(y),x)),z)),u)=f(y,f(g(f(g(f(v,z)),v)),g(f(g(f(w,u)),w)))).
2110 [para_into,1895.1.1.2,1952.1.1] f(f(x,g(x)),f(g(f(y,g(z))),y))=z.
2115 [para_into,1895.1.1.2,312.1.1] f(f(x,g(x)),f(y,z))=f(g(f(u,g(f(g(g(f(v,g(v)))),f(w,f(g(f(g(y),w)),z)))))),u).
2125 [copy,2115,flip.1] f(g(f(x,g(f(g(g(f(y,g(y)))),f(z,f(g(f(g(u),z)),v)))))),x)=f(f(w,g(w)),f(u,v)).
2164 [para_into,2110.1.1.2.1,1738.1.1] f(f(x,g(x)),f(y,g(y)))=f(z,g(z)).
2194 [para_into,2164.1.1,2164.1.1] f(x,g(x))=f(y,g(y)).
2203 [para_from,2164.1.1,1137.1.1.2.1.2] f(f(x,g(g(f(g(x),f(y,g(y)))))),g(f(g(f(z,f(g(f(g(u),z)),v))),f(w,g(w)))))=f(u,v).
2206 [para_from,2164.1.1,312.1.1.2.1.1.2.1.2] f(x,f(g(f(y,g(f(g(x),f(z,g(z)))))),y))=f(u,g(g(f(g(u),f(v,g(v)))))).
2209 [para_from,2164.1.1,136.1.1.2.2.1.2] f(x,f(g(f(g(f(y,g(g(f(g(x),f(z,g(z))))))),y)),g(f(g(u),f(v,g(v))))))=u.
2226,2225 [para_from,2164.1.1,114.1.1.1,demod,1896] g(f(g(x),f(y,g(y))))=x.
2241,2240 [back_demod,2209,demod,2226,2226] f(x,f(g(f(g(f(y,g(x))),y)),z))=z.
2244 [back_demod,2206,demod,2226,2226] f(x,f(g(f(y,x)),y))=f(z,g(z)).
2246,2245 [back_demod,2203,demod,2226,2226] f(f(x,g(x)),f(y,f(g(f(g(z),y)),u)))=f(z,u).
2261 [back_demod,2050,demod,2241] g(f(g(x),f(y,f(g(f(z,y)),z))))=x.
2290,2289 [para_from,2194.1.1,1891.1.1.2] f(f(g(f(x,y)),x),f(z,g(z)))=g(y).
2763,2762 [para_from,2244.1.1,1891.1.1.2,demod,2290,flip.1] f(g(f(x,y)),x)=g(y).
2806,2805 [back_demod,2289,demod,2763] f(g(x),f(y,g(y)))=g(x).
2811,2810 [back_demod,2261,demod,2763,2806] g(g(x))=x.
2837,2836 [back_demod,2125,demod,2811,2246,2763,2811,flip.1] f(f(x,g(x)),f(y,z))=f(y,z).
2841,2840 [back_demod,2115,demod,2837,2811,2837,2763,2811,flip.1] f(x,f(g(f(g(y),x)),z))=f(y,z).
2846 [back_demod,2103,demod,2841,2763,2811,2763,2811] f(f(x,y),z)=f(x,f(y,z)).
2848 [binary,2846.1,2.1] $F.
------------ end of proof ------------

こんなもん、手でできるわけないやろというのが最初の感想。しかし計算時間はほぼ瞬時なので、OTTERはなかなか賢いやつである。
一行一行解説するのも大変なのでそこはご勘弁だが、2194に単位元(らしきもの)の存在、2811に逆元を取る操作(関数g)を二回やるともとにもどるというようなものが見える。


結合律は証明されたので、これを公理に加えて残りの公理の導出がどうなるか見てみよう。
まずは、左単位元の公理。単位元としては上で証明された \forall x \forall y(xx^{-1}=yy^{-1}) に出てくる共通な項を使う。

----------------------------------------
set(auto).
list(usable).
x=x.
f(f(w,f(g(f(g(x),w)),z)),f(g(f(y,z)),y))=x.
f(x,f(y,z)) = f(f(x,y),z).
f(f(a,g(a)),b) != b.
end_of_list.
----------------------------------------

できた証明は、ぐっと短くなった。

---------------- PROOF ----------------
1 f(f(a,g(a)),b)!=b.
3 f(f(x,f(g(f(g(y),x)),z)),f(g(f(u,z)),u))=y.
5 f(x,f(y,z))=f(f(x,y),z).
7,6 [copy,5,flip.1] f(f(x,y),z)=f(x,f(y,z)).
8 [back_demod,3,demod,7,7] f(x,f(g(f(g(y),x)),f(z,f(g(f(u,z)),u))))=y.
10 [back_demod,1,demod,7] f(a,f(g(a),b))!=b.
16,15 [para_into,8.1.1.2.2.2.1.1,6.1.1] f(x,f(g(f(g(y),x)),f(z,f(g(f(u,f(v,z))),f(u,v)))))=y.
22,21 [para_from,8.1.1,6.1.1.1,demod,7,7,7,flip.1] f(x,f(g(f(g(y),x)),f(z,f(g(f(u,z)),f(u,v)))))=f(y,v).
35 [para_into,15.1.1.2.2.2.1.1,8.1.1,demod,7,7,22] f(x,f(g(y),f(z,g(f(g(y),z)))))=x.
44,43 [para_from,15.1.1,6.1.1.1,demod,7,7,7,7,flip.1] f(x,f(g(f(g(y),x)),f(z,f(g(f(u,f(v,z))),f(u,f(v,w))))))=f(y,w).
87 [para_into,35.1.1.2.2.2.1,15.1.1,demod,7,7,7,7,44] f(x,f(y,g(y)))=x.
129 [para_from,87.1.1,6.1.1.1,demod,7,flip.1] f(x,f(y,f(g(y),z)))=f(x,z).
199 [para_from,129.1.1,15.1.1.2.1.1,demod,7,7,16] f(x,f(g(x),y))=y.
201 [binary,199.1,10.1] $F.
------------ end of proof -------------

解釈としては、もとの(x({({y^{-1}}x)^{-1}}z))({(uz)^{-1}}u)=yを結合律より、(x{({y^{-1}}x)^{-1}})(z({(uz)^{-1}}u))=y\quad \cdots (1)と変形。

uuvを代入して結合律をつかうと、({x({y^{-1}}x)^{-1}})(z({(u(vz))^{-1}}(uv)))=y\quad \cdots (2).

({x({y^{-1}}x)^{-1}})(z({(uz)^{-1}}u))=yに右からvをかけてから、結合律を使って、({x({y^{-1}}x)^{-1}})(z({(uz)^{-1}}(uv)))=yv\quad \cdots (3).

ここで(2)でu,v,zに対してそれぞれx, {({y^{-1}}x)^{-1}},z{(uz)^{-1}}uを代入して、(1)を使ってuvz=yと置き換えて、さらに(3)を使うと次が導出できる(文字がぶつからないように適当に入れ替えは必要)。

x({y^{-1}}(z{({y^{-1}}z)^{-1}}))=x

これが証明リストの35式となる。あとの変形は難しくないと思う。証明リストの[]の中に変形方法が書いてあるらしいのだが、まあ、どの式を使うかぐらいのヒントにしかなってないような...OTTERじゃない証明プログラムならもっと親切なのかもしれない。

さて、残るは左逆元の公理の導出。左単位元の公理は加えておく。

----------------------------------------
set(auto).
list(usable).
x=x.
f(f(w,f(g(f(g(x),w)),z)),f(g(f(y,z)),y))=x.
f(x,f(y,z)) = f(f(x,y),z).
f(f(x,g(x)),y) = y.
f(g(a),a) != f(b,g(b)).
end_of_list.
----------------------------------------

証明は次のとおり。

---------------- PROOF ----------------
1 f(g(a),a)!=f(b,g(b)).
2 [copy,1,flip.1] f(b,g(b))!=f(g(a),a).
4 f(f(x,f(g(f(g(y),x)),z)),f(g(f(u,z)),u))=y.
6 f(x,f(y,z))=f(f(x,y),z).
8,7 [copy,6,flip.1] f(f(x,y),z)=f(x,f(y,z)).
9 f(f(x,g(x)),y)=y.
11,10 [copy,9,demod,8] f(x,f(g(x),y))=y.
12 [back_demod,4,demod,8,8] f(x,f(g(f(g(y),x)),f(z,f(g(f(u,z)),u))))=y.
15,14 [para_into,10.1.1.2,10.1.1,flip.1] f(g(g(x)),y)=f(x,y).
16 [para_from,14.1.1,10.1.1.2] f(g(x),f(x,y))=y.
23,22 [para_into,12.1.1.2.1.1,16.1.1,demod,8,11] f(x,f(y,f(g(f(z,y)),z)))=x.
28 [para_into,12.1.1.2.1.1,10.1.1,demod,15,23,8] f(x,f(y,g(y)))=x.
47 [para_from,28.1.1,16.1.1.2] f(g(x),x)=f(y,g(y)).
48 [copy,47,flip.1] f(x,g(x))=f(g(y),y).
49 [binary,48.1,2.1] $F.
------------ end of proof -------------

以上でミッション完了である。てか、田中テキストの本編はちっとも読み進めてないんですが。