%\documentclass[b5paper,twoside]{jsarticle}
\documentclass[twoside]{jsarticle}
\usepackage{proof}
%\setlength{\textwidth}{125truemm}
%\setlength{\textheight}{200truemm}
%\setlength{\oddsidemargin}{3truemm}
%\setlength{\evensidemargin}{3truemm}
%\setlength{\topmargin}{-5truemm}
%\setlength{\headsep}{5truemm}
%\setlength{\headheight}{5truemm}
%\setcounter{page}{43}
\pagestyle{myheadings}
\renewcommand{\to}{\supset}
\title{ラッセルのパラドックスから部分構造論理上の集合論へ}       
\author{古森 雄一 (千葉大学 理学部)\\ komori@math.s.chiba-u.ac.jp}
\date{2002 年 12 月 9 日}
\begin{document}
\maketitle
\thispagestyle{myheadings}
\section{序論}
カントールの集合論で最初に発見された逆理といわれているブラリ-フォルティの逆理\cite{Burali-Forti1987}は
順序数論ともいえるカントールの集合論には多大な影響を与えたが, 数学の基礎としての論理には
影響がなかった。その後発見されたラッセルの逆理\cite{Russell02}は表現 $\{x\mid x\notin x\}$ を項として認め
\[\mbox{任意の項} t \mbox{および任意の論理式} \ \alpha(x) \ \mbox{について, \ }
 t\in \{x\mid \alpha(x)\} \Longleftrightarrow \alpha(t)\]
という原理(この原理を"代入原理"と呼ぶことにする)さえ認
めれば他の(外延性公理など)公理は一切なしでも出てくるので, 論理の矛盾としてとらえられ深刻な
影響を与えた(cf. Frege\cite{Frege02})[注: 当時, ここに書いたように認識していたわけではない。ここでは, 現代の立場で
しかも構文論を強調した書き方をした。当時は構文論と意味論の区別もはっきりしていなかった]。
これらの逆理を克服するための主流はツェルメロ\cite{Zermelo1908}とフレンケル\cite{Fraenkel1922} による公理的集合論である。
この流れはあまりにもうまく行き過ぎた感があり, 他の流れはどれも細々としたものである(cf. \cite{Fraenkel1973})。
中でも論理を変えて逆理を解消しようという流れは小さな傍流である。しかし, その歴史は面白いものがあり,
ラムダ計算との合体により, チャーチがラムダ計算を考え出した当初の目論見(cf. \cite{Church1932},\cite{Church1933})であ
る「論理を含んだラムダ
計算により数学を建設する」が一部であるが復権することになる。そして小さな傍流が案外大きな流れになる
可能性を秘めているのではないだろうか。

古典論理や直観主義論理では, (W): $(\alpha\to\alpha\to\beta)\to\alpha\to\beta$ \ (足りない括弧は右から補う)が導けること,
ゲンツェンのシークエント計算(\cite{Gentzen})でいうと縮約(contraction)が推論規則であること, 同じくゲンツェンの自然演繹
でいうと一度に 2 つ以上の仮定が落とせること等が, ラッセルの逆理が導けることと密接に関係している。

ここで, ゲンツェンの自然演繹でラッセルの逆理を導いておく。$R$ を $\{x\mid x\notin x\}$ の省略記号,
 $p$ を $R \in R$ の省略記号とする。この小論に出て来るどの論理でも「$\neg$ (否定)」は「$\to$ (ならば)」と
 「$\bot$ (偽定数)」を用いて次のように定義可能である: $\neg \alpha$ は $\alpha\to\bot$ の省略である。
以上のように記号を定めると, 代入原理から「$p \Longleftrightarrow \neg p$」が得られる。これから, 次の
推論規則が正当化される。
\[
\infer[\mbox{(代入1)}]{\neg p}{\deduce{p}{\Pi}}, \hspace{7mm}
\infer[\mbox{(代入2)}]{p}{\deduce{\neg p}{\Pi}}。
\]
この 2 つの規則以外に使われる規則は次の 2 つである:
\[ \infer[\mbox{($\to$-E)}]{\beta}{\deduce{\alpha\to \beta}{\Pi_1}  & \deduce{\alpha}{\Pi_2}},
\hspace{7mm} \infer[k\mbox{($\to$-I)}]{\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}}
\]
{\bf ラッセルの逆理の導出}
\[ \infer[\mbox{($\to$-E)}]{\bot}{\infer[1 \mbox{($\to$-I)}]{\neg p}{\infer[\mbox{($\to$-E)}]{\bot}{
		\infer[\mbox{(代入1)}]{\neg p}{\deduce{p}{1}} & \deduce{p}{1} }}
	&
	\infer[\mbox{(代入2)}]{p}{
		\infer[1 \mbox{($\to$-I)}]{\neg p}{\infer[\mbox{($\to$-E)}]{\bot}{
		\infer[\mbox{(代入1)}]{\neg p}{\deduce{p}{1}} & \deduce{p}{1} }}}}
\]

上の導出において, 述語論理についての規則と偽命題につての規則(偽から何でも出る)は使われていないことを
注意しておく。
%
\section{ウカシュヴィッツの多値論理上の集合論}
ウカシュヴィッツは最初に 3 値論理を考えたが\cite{Lukasiewicz1920}, その動機の一つがラッセルの逆理の解消であった。
その後(\cite{Lukasiewicz1930}), ウカシュヴィッツとタルスキはそれを一般化して $n$ ($2 \leq n \leq\omega$) 値論理を考
えている。

まず, ウカシュヴィッツの多値命題論理 L$_m$($m$ は 2 以上の自然数か $m = \omega$) につい
て概説する。L$_m$ の真理値の集合を $S_m$ とすると,
\begin{eqnarray*}
S_m & = & \left\{0, \frac{1}{m-1}, \frac{2}{m-1},\cdots, \frac{m-2}{m-1}, %
1\right\}(m \neq \omega ) \\
S_\omega & = & [0,1] = \{x\mid 0\leq x\leq 1 \}
\end{eqnarray*}
である。命題変数全体の集合から $S_m$ への写像を $S_m$ の{\bf 付値}
(assignment)という。付値 $f$ を次の(1), (2) に従って, 論
理式全体の集合から $S_m$ への写像に拡張する:
\begin{eqnarray*}
(1)\ \  & f(\alpha\to \beta) & = \mbox{min}(1,1-f(\alpha)+f(\beta)) \\
(2)\ \  & f(\bot) & = 0
\end{eqnarray*}
任意の $S_m$ の付値 $f$ に対して, $f(\alpha)=1$ となっているとき,
論理式 $\alpha$ は $S_m$ で{\bf 恒真}(valid)であるという。$S_m$ で恒真な
論理式をだけをすべて導く体系を, L$_m$ の体系という。L$_3$ の
体系は M.Wajsberg\cite{Wajsberg1931} により, $m$ が 4 以上の自然数のときの L$_m$ の体系は
J.B.Rosser と A.R.Turquette\cite{Rosser1945} により, L$_\omega$ の体系は A.Rose
と J.B.Rosser\cite{Rose1958} により, 1931 年から1958 年の間につくられ
ている。L$_\omega$ の体系は推論規則として分離規則(($\to$-E) と同じもの)をもち, 
次の 6 つの公理型からなるものである。
\[
\begin{array}{ll}
\mbox{(B)} & (\beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma \\
\mbox{(C)} & (\alpha \to \beta \to \gamma) \to \beta \to \alpha \to \ \gamma \\
\mbox{(K)} & \alpha \to \beta \to \alpha \\
\mbox{(L1)} & ((\alpha\to\beta)\to\beta)\to (\beta\to\alpha)\to\alpha \\
\mbox{(L2)} &  ((\alpha\to \beta)\to\beta\to\alpha)\to\beta\to\alpha \\
\mbox{(N)} & \bot \to \alpha
\end{array}
\]
%
$m$ が自然数のときの L$_m$ の体系は L$_\omega$ の体系に有限個の公理
型を付け加えたものになっている。また, L$_\omega$ の体系に前節の公理型 W を付け加えると
古典論理になる。

前節で見たようにラッセルの逆理は $p \Longleftrightarrow \neg p$ がでるという矛盾である。
$S_3$ において $f(p)= 1/2$ とすると $f(p)=f(\neg p)=1/2$ となり
 $p \Longleftrightarrow \neg p$ は矛盾ではなくなる。実際, ウカシュヴィッツの 3 値論理に $\{x\mid x\notin x\}$
 を項として認めるという包括化(comprehension)公理と代入原理を加えても矛盾しないことが証明できる(モデルが作れる)。

しかし, M. Shaw-Kwei\cite{Shaw-Kwei1954} はウカシュヴィッツの 3 値論理に, 任意の論理式 $\alpha(x)$ について
 $\{x\mid \alpha(x)\}$
 を項として認めるという無制限の包括化公理を付け加えると矛盾することを示した。
この論文では, 自然数 $n$ に対してはウカシュヴィッツの $n$ 値論理に無制限の包括化公理を付け加えると
矛盾することも示している。以下にその概略をオリジナルよりやや洗練された方法で述べる。
省略記法「$\alpha\to^n\beta$」を 「$\alpha\to^1\beta$ は $\alpha\to\beta$;\ \ $\alpha\to^{n+1}\beta$ は
 $\alpha\to(\alpha\to^n\beta)$」と帰納的に定義する。
$R_n$ を $\{x\mid (x\in x) \to^n \bot\}$ の省略記号, \ 
 $p_n$ を $R_n \in R_n$ の省略記号とする。
このように記号を定めると, 代入原理からは「$p_n \Longleftrightarrow p_n\to^n\bot$」が得られる。これから, 次の
推論規則が正当化される。
\[
\infer[\mbox{(代入1)}]{p_n\to^n\bot}{\deduce{p_n}{\Pi}}, \hspace{7mm}
\infer[\mbox{(代入2)}]{p_n}{\deduce{p_n\to^n\bot}{\Pi}}。
\]
また, ($\to$-E) を $n$ 回使うと次の規則が得られる:
\[ \infer[\mbox{($\to^n$-E)}]{\beta}{\deduce{\alpha\to^n \beta}{\Pi_1}  & \deduce{\alpha}{\Pi_2}}。\]
$S_{n+1}$ で論理式 (W$_n$): $(\alpha\to^n\alpha\to^n\beta)\to^n\alpha\to^n\beta$ \ は恒真である。
よって L$_{n+1}$ の体系では次の規則 ($\to^n$-I) が許される:
\[\infer[k\mbox{($\to^n$-I)}]{\alpha \to^n \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}}。\]
以上より, 前節と全く同様に($\to$ を $\to^n$ 変えればよい)「$\bot$」に至る証明図を得る。

Shaw-Kwei の論文には「L$_\omega$ の体系に無制限の包括化公理を付け加えると矛盾するか?」が興味深い未解決問題と
述べられている。この問題はその 25 年後に R.B. White\cite{White1979} が「 無矛盾である」という形で解決した。
この問題は相当な難問である。まず, L$_\omega$ の体系が分離規則と 6 つの公理型により得られると述べたが,
それは命題論理の話である。$S_\omega$ で恒真な述語論理の論理式は帰納的可算ではないことが証明されている
(Scarpellini\cite{Scarpellini1962})。よって, 述語論理 \ L$_\omega$ の体系は有限的な推論規則と有限個の公理型では得られない
ことになる。そこで L.S. Hay\cite{Hay1963} は無限的な規則を採用して \ L$_\omega$ の体系を作っている。
White は Hay の体系に無制限の包括化公理を付け加えても無矛盾であることを示している。しかし, もともとの
Shaw-kwei の問題意識はその様なものであったのであろうか。

ウカシュヴィッツの多値論理は模型が先にあり, 後から形式化(=公理化)が行われている。
矛盾を示す場合は, 模型で許される規則の一部を使って矛盾を示せばいいので, 必ずしも
正確な形式化は必要としない。しかし無矛盾を示す場合は, それより強い簡単に形式化できる体系が無矛盾
である場合を除きその様なわけにいかず, 正確な形式化を必要とする。
正確な形式化なしに無矛盾を考えるには---これがウカシュヴィッツの多値論理においては正統なのであろうが---
模型があるかどうかと捉える方法がある。普通の捉え方も模型を使った捉え方も結局は同値であるが, この問題に取り組も
うとした人たちを「どちらで取扱おうかと」悩ませたに違いない。
問題を出した Shaw-kwei はあまりその様なことは深く考えずに出したのであろう。

White の無矛盾性の証明は巧妙である。まず, L$_\omega$ の命題論理の体系に自然な述語論理についての
推論規則を付け加え, さらに無制限な包括化公理を付け加えたた体系を G を定義する。体系 G で証明可能な
論理式は L$_\omega$ の述語論理の体系に無制限の包括化公理を付け加えた体系でも証明可能であるが,
逆は成り立たない。そして体系 G の無矛盾性を証明する(決して容易ではない)。White は模型といういわずに
極大無矛盾系という言葉を使っているが, G の模型が \ $S_\omega$ \ で全ての包括化公理を真にする
模型となっていることを示したのである。これは体系 G は帰納的に公理化できるが, ちょうどそれを特徴付ける
模型を持たないことを意味している。このことは非古典論理を研究しているとよくあることである。
White は体系 G に外延性(extensionality)公理を付け加えると古典論理になり, その結果として矛盾すること
も示している。

White の結果によりウカシュヴィッツの無限多値論理上の(無制限な包括化公理を持つ)集合論は
無矛盾であることが分かったのであるが, その後その集合論の研究は進展しなかった。
その体系が複雑すぎた上に, どうしても必要な複雑さとは思えなかったからであろう。
%
\section{部分構造論理上の集合論と論理を含む型なしラムダ計算}
%
序論で述べたように包括化公理から矛盾を導くのには縮約規則が必要であった。ゲンツェンのシークエント計算において縮約規則などの構造に関する規則を除いて得られる論理を部分構造論理と 1990 年代に呼ぶようになった(cf. \cite{OnoKomo}, \cite{Substructural93})。
縮約規則がなければ矛盾しないことに最初に気付いたのは Gri\v{s}in\cite{Grisin1974} であった。
さらに外延性公理が縮約規則を導き矛盾を導出することも示した(\cite{Grisin1982})。
多値論理上の集合論でも同じような議論をしているのであるが, 縮約規則に焦点を当てていた訳では
なかった。この発見はされてみると大した事がないように見えるが大きな第一歩であった。
Gri\v{s}in の体系は古典論理から縮約規則を除いたものであった。

1987 年に White\cite{White1987} は直観主義論理から縮約規則を取り除いた体系(BCK 論理)に無制限な包括化公理
を付け加えても無矛盾であることを自然演繹を使って証明した。結果そのものは White 自身の多値論理の結果からも
Gri\v{s}in の結果からもでてくるものである(ウカシュヴィッツの無限多値論理も古典論理から縮約を除いたものも
BCK 論理よりは強い論理である)。しかし, その証明は分かりやすく自明ともいえる定理となっている。
落とせる仮定が高々 1 つなので証明図の変形により証明図の大きさが必ず小さくなるというあたりまえともいえる
事実に基づいている。この論文には Gri\v{s}in\cite{Grisin1974} は引用されているが White\cite{White1979} は引用されていない。
おそらく, 25 年も解けなかった難問解決よりも, この易しい結果がよいものであり, 難問解決の途中で
それに気付いてもいいはずだったのにとの思いが White にはあったのであろう。
私もそう思うのであるが, 往々にしてそういうことはあるのであろう。
なお, Shaw-Kwei\cite{Shaw-Kwei1954} の方法は BCK 論理にも使えて, 有限 BCK 論理(有限 BCK 代数を模型にもつ論理)
では, 無制限の包括化公理を付け加えると矛盾する。

型なしラムダ計算(type free lambda calculus)は項 $M, N$ に対して項 $MN$ を $N \in M$ と, $\lambda x. M$ を
 $\{x\mid M\}$ と思うことにより論理記号を表す定数があれば集合論の言語と考えられる。しかも, 自然数や順序対
などは論理記号なしで定義できるので普通の集合論の言語より表現力が強いものである。
当然, その論理記号が古典論理や直観主義論理に従うならばラッセルの逆理と同様のカリーの逆理が導出される。
チャーチがラムダ計算を考えた当初は論理定数を含んでいたのであるが, Kleene と Rosser\cite{Kleene1935} がそれが
矛盾を含むことを発見してからは, 主に論理定数を除いた体系(も非常に豊富な内容を含むので)が研究されてきた
(cf. \cite{Hindley}, \cite{Hindley2})。

古森は White の結果が論理を含む型なしラムダ計算に拡張できることに気が付いたが, それだけでは
あたりまえ過ぎて論文にする価値はないと考え, 論理を含む型なしラムダ計算の模型を考案しそれと共に
論文にした(\cite{Komori89})。このような模型の考案ははじめてのようであった。
M.W. Bunder は論理を含む型なしラムダ計算の研究を近年盛んにしている研究者である。
彼はカリーのもとでの学位論文\cite{Bunder1969} 以来この分野をライフワークとしている(\cite{Bunder1986},\cite{Bunder1998})。
1986 年の論文では古森の結果(模型についての結果を除く)を含む結果を得ているようである。しかし BCK 論理
という縮約がない論理に注目した論文ではなく分かりづらい。

比較的最近の仕事としては白旗による線形論理(cf. \cite{Girard1987}, \cite{Troelstra1992})に無制限の包括化公理を付け加えた体系に
ついての論文\cite{Shirahata1996}がある。
基礎としての論理を線形論理とするのは, 線形論理独特の論理演算子「!」などが BCK 論理上の集合論で
ほぼ定義できることが分かった現在では見直しが必要であろう。
また, U. Petersen\cite{Petersen2000} は普通の外延性公理よりも弱い外延性原理「$\forall x(x \in s \equiv x \in t)$ が仮定なしで
証明できたら $s \in u\to t \in u$ を導いてよい」を 無制限の包括化公理を含む BCK 論理に付け加えても
矛盾することを示した。この論文は見通しのいいものではないが, 「!」がほぼ定義可能であることに気付くと
見通しのいいものになる。この 2 つ論文は言語としてラムダ計算を使っていないが, ラムダ計算を使った方が
いくつかの面倒な問題に関わらなくて済む。
%
\section{BCK 論理に従う論理記号を含むラムダ計算}
%
ほぼ古森\cite{Komori89} にしたがって説明する。
ラムダ項は型なしラムダ項のことであり, 定数として「$\Xi$」を含む。
体系 $BCK\beta\eta$ の論理式はラムダ項のことである。体系 $BCK\beta\eta$ の推論規則は次の 3 つである:
\[ \vcenter{\infer[\mbox{($\Xi$e)}]{\beta\gamma}{\deduce{\Xi\alpha\beta}{\Pi_1}  & \deduce{\alpha\gamma}{\Pi_2}}},
\hspace{7mm} \vcenter{\infer[k\mbox{($\Xi$i)}]{\Xi\alpha\beta}{\deduce{\beta x}{\deduce{\Pi}{\deduce{\alpha x}{k}}}}},
\hspace{7mm} \vcenter{\infer[(\beta\eta)]{\beta}{\deduce{\alpha}{\Pi}}}\mbox{\ \ if \ \ }\alpha=_{\beta\eta}\beta.
\]
ここで, 規則 ($\Xi$i) においては変数 $x$ は $\alpha$, $\beta$ および落ちていない仮定に自由に現われない。また,
一度に落とせる仮定は高々 1 つである, すなわち 数字 $k$ は高々 1 ヶ所にしか現われない。

項 $\Xi\alpha\beta$ の直観的な意味は $\forall x(\alpha x\to \beta x)$ である。この言語は表現力が豊かで
多くの論理記号や述語が以下のように省略記号として定義できる:
\[
\begin{array}{rcl}
\alpha\to\beta & \equiv_{def} & \Xi(\mbox{\bf K}\alpha)(\mbox{\bf K}\beta), \mbox{\ where {\bf K}}\equiv_{def}\lambda xy.x ;\\
\top & \equiv_{def} & \Xi \mbox{\bf II},\mbox{ \ where {\bf I}}\equiv_{def}\lambda x.x ;\\
\forall x\alpha & \equiv_{def} & \Xi (\mbox{\bf K}\top)(\lambda x.\alpha) ;\\
\alpha+\beta & \equiv_{def} & \forall y((\alpha\to y)\to(\beta\to y)\to y) ;\\
\alpha\&\beta & \equiv_{def} & \forall y((\alpha\to\beta\to y)\to y) ;\\
\exists x \alpha & \equiv_{def} & \forall y(\forall x(\alpha\to y)\to y) ;\\
\bot & \equiv_{def} & \forall x x ;\\
\alpha \in \beta & \equiv_{def} & \beta\alpha ;\\
\alpha\wedge\beta & \equiv_{def} & \forall x(\forall y((y\to\alpha)\to(y\to\beta)\to y \to x)\to x) ;\\
\alpha\vee\beta & \equiv_{def} & \forall y((\alpha\to y)\wedge(\beta\to y)\to y) ;\\
!\alpha & \equiv_{def} & \forall x(x\top\to x\alpha) 。
\end{array}
\]

後半の三つは\cite{Komori89}には述べられていない。最近になって分かったことである。ただし, この「!」は
線形論理の「!」の性質を全ては持っていない。縮約がない体系では論理和と論理積については加法的なものと
乗法的なものとの区別が必要であるが, どちらも定義できるのである。私が \cite{Komori89} を書いた当時は加法的なものは
定義できないと考えていた。
%「!」については $(!\alpha\to !\alpha\to\beta)\to !\alpha\to\beta$ が次のように
%証明可能である。
%\[ \]
「!」については次の 2 つの推論規則が許されることが分かる。
\[
\infer[\mbox{(!e)}]{\alpha}{\deduce{!\alpha}{\Pi}}, \hspace{7mm}
\hspace{7mm} \infer[k\mbox{(!$\to$i)}]{!\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{!\alpha}{k}}}} 。
\]
ただし, (!$\to$i) において仮定はいくつでも落とせる。


$R_!$ を $\lambda x.(\neg !xx)$ の省略記号とする。上の二つが許される規則であることを使うと,
次のように $R_!R_!$ であることが示せる。
\[
\infer[\mbox{(代入2)}]{R_!R_!}{\infer[1 \mbox{(!$\to$-I)}]{\neg !R_!R_!}{\infer[\mbox{($\to$-E)}]{\bot}{
		\infer[\mbox{(代入1)}]{\neg !R_!R_!}{
			\infer[!e]{R_!R_!}{\deduce{!R_!R_!}{1}}} 
		& \deduce{!R_!R_!}{1} }}}
\]
つまり 集合 $R_!$ は自分自身をを元として含むのである。

線形論理の「!」については, 「$\alpha$ が "!" が先頭に現われる仮定だけから導けるならば, 同じ仮定から $!\alpha$
を導いてよい」という推論規則が許される。$BCK\beta\eta$ で, それが許されるとすると矛盾が出るので, 無矛盾性から
許される規則でないことが分かる。もっと弱い (*)「$\alpha$ が仮定なしで導けるならば, $!\alpha$
を導いてよい」という推論規則が認めても, 上の推論図から $!R_!R_!$ が証明できて, 矛盾が出てしまう。
(*) は全体集合 $\lambda x.\top$ についての弱い外延性原理である。一般の弱い外延性原理ではなく全体集合に限って
弱い外延性原理を認めても体系 $BCK\beta\eta$ は矛盾してしまうのである。
この結果自身は Petersen\cite{Petersen2000} の結果から分かるのであるが彼の方法は不動点定理を使う分かりづらいものである。
不動点定理を使うとさらに驚くべき結果も得られる。空集合 $\lambda x.\bot$ についての弱い外延性原理から
矛盾が出るのである。全体集合のような大きな集合についての外延性が矛盾を導くとしても驚かないが, 空集合のような
有限集合の外延性から矛盾がでることは驚きである。

Petersen の論文はラムダ計算を使用していないための分かりづらさがある。ラムダ計算なしで順序対を定義するためには
ペア $\{x, y\}$ の定義が必要である。$\{x, y\} \equiv_{def} \{z\mid z = x \mbox{ or } z=y\}$ と定義する際に 「or」
を加法的なものにするか乗法的なものにするか悩ましいのである。言語をラムダ計算にすると順序対や個々の自然数などは
論理記号なしで定義できる。体系 $BCK\beta\eta$ が無矛盾であることが分かっているので, 言語にラムダ計算を採用しな
い理由は見当たらない。

論文\cite{Komori89} を書いた直後は, 体系 $BCK\beta\eta$ の無矛盾性が容易に証明できるので, 無矛盾性が容易に証明できる体系な
どはあまり内容がないと考え, すぐに体系の強化を考えた。そして, 直後に書いた論文では, ここで述べた考察からすぐに矛盾
することが分かる体系も提案している。確かに, 無矛盾性が容易に証明できる体系では, その中では数学を展開するのは
不十分である。しかし, $BCK\beta\eta$ は当初思っていたよりも豊かな
体系のようである。
体系 $BCK\beta\eta$ の強化を考える前に $BCK\beta\eta$ についてもっと深く知る必要があり, そうしないとすぐ
矛盾に落ちてしまう。いろいろ面白い結果が出ているが, ラムダ計算に比べてここが非常に豊かになったところであるという
決定打はまだ見つかっていないのではないだろうか。当初, 安易にそのようなものはないと思い込んだのであるが, ここに述べ
たことが分かってくるに連れて, その様な決定打があるのではないかと思っている。
\nocite{Heijenoort}\nocite{Szabo}
\bibliography{logic.bib}
\bibliographystyle{plain}
\end{document}
