汎用システムとしての「ラムダ計算 + 論理」

千葉大学総合メディア基盤センター古森雄一 (Yuichi Komori) Institute of Media and Information Technology Chiba University komori@math.s.chiba-u.ac.jp

1 序論

1930 年代に Church がラムダ計算を考案したときは論理定数を含んでいた ([4],[5])。含んでいたというより, Church の論文の表題「A set of postulates for the foundation logic」からは, Church はラムダ計算を論理 (さらに, 数学) の基礎にしようと考えていたことが窺がえる。しかし, その後この体系には矛盾が発見され ([16]), 論理定数は取り除かれラムダ計算の部分だけが主に研究されてきた。論理定数を含む体系も illative combinatory logic として研究されてきたが, 古典述語論理などがシミュレートできるように人為的に作られた感じのものであった。優れた汎用システムはそれぞれ独自の思想を持ち, その思想を簡明に表現しているのが望ましい。 U. Petersen[19] の仕事からヒントを得て, 「ラムダ計算 + 論理」は非常に優れた汎用システムである可能性が高いことが分かってきた。

2 カントールの集合論の矛盾

カントールの集合論で最初に発見された逆理といわれているブラリ-フォルティの逆理 [3] は順序数論ともいえるカントールの集合論には多大な影響を与えたが, 数学の基礎としての論理には影響がなかった。その後発見されたラッセルの逆理 [21] は表現 {x | x ∉ x} を項として認め

任意の項t および任意の論理式α(x) について, t ∈ {x | α(x)} ⟺ α(t)

という原理 (この原理を”代入原理”と呼ぶことにする) さえ認めれば他の (外延性公理など) 公理は一切なしでも出てくるので, 論理の矛盾としてとらえられ深刻な影響を与えた (cf. Frege[9])[注: 当時, ここに書いたように認識していたわけではない。ここでは, 現代の立場でしかも構文論を強調した書き方をした。当時は構文論と意味論の区別もはっきりしていなかった]。これらの逆理を克服するための主流はツェルメロ [30] とフレンケル [7] による公理的集合論である。

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

ここで, ゲンツェンの自然演繹でラッセルの逆理を導いておく。 R を {x | x ∉ x} の省略記号, p を R ∈ R の省略記号とする。この小論に出て来るどの論理でも「¬ (否定)」は「⊃ (ならば)」と「⊥ (偽定数)」を用いて次のように定義可能である: ¬α は α ⊃ ⊥ の省略である。以上のように記号を定めると, 代入原理から「p ⟺ ¬p」が得られる。これから, 次の推論規則が正当化される。

Π p ; ¬p (代入 1),  {Π \atop ¬p} ; p (代入 2)。

この 2 つの規則以外に使われる規則は次の 2 つである:

\begin{matrix}{Π_{1} \atop α ⊃ β} & {Π_{2} \atop α} \\ β \end{matrix} (⊃-E),  k α ; Π ; β ; α ⊃ β k(⊃-I)

ラッセルの逆理の導出

\begin{matrix}\begin{matrix}\begin{matrix}1 p ; ¬p (代入 1) & 1 p \\ ⊥ \end{matrix} & (⊃-E) \\ ¬p \end{matrix} ; 1(⊃-I) & \begin{matrix}\begin{matrix}1 p ; ¬p (代入 1) & 1 p \\ ⊥ \end{matrix} & (⊃-E) \\ ¬p \end{matrix} ; 1(⊃-I) ; p ; (代入 2) \\ ⊥ \end{matrix} ; (⊃-E)

上の導出において, 述語論理についての規則と偽命題につての規則 (偽から何でも出る) は使われていないことを注意しておく。

3 論理を変えた無矛盾な集合論

公理的集合論 ZF はあまりにもうまく行き過ぎた感があり, 他の方法で矛盾を回避するものはいずれも細々としたものであった (cf. [8])。中でも論理を変えて逆理を解消しようという流れは小さな傍流であった。しかし, その歴史は面白いものがあり, Grišin([11], [12]), White[29] の BCK 論理上の集合論として結実する。さらに, 古森 ([17]), Bunder([2]) によりラムダ計算と結び付けられ, チャーチがラムダ計算を考え出した当初の目論見である「論理を含んだラムダ計算により数学を建設する」が復権する可能性がでてきた。

まず, 登場したのがウカシュヴィッツ論理上の集合論である。ウカシュヴィッツは最初に 3 値論理を考えたが [25], その動機の一つがラッセルの逆理の解消であった。その後 ([26]), ウカシュヴィッツとタルスキはそれを一般化して n (2 ≤ n ≤ ω) 値論理を考えている。

ウカシュヴィッツの多値命題論理は模型を使って定義されるが, その無限値論理の公理系は A.Rose と J.B.Rosser[20] により作られ, 次の 6 つの公理型からなるものである。

\begin{matrix}(B) & (β ⊃ γ) ⊃ (α ⊃ β) ⊃ α ⊃ γ \\ (C) & (α ⊃ β ⊃ γ) ⊃ β ⊃ α ⊃ γ \\ (K) & α ⊃ β ⊃ α \\ (L1) & ((α ⊃ β) ⊃ β) ⊃ (β ⊃ α) ⊃ α \\ (L2) & ((α ⊃ β) ⊃ β ⊃ α) ⊃ β ⊃ α \\ (N) & ⊥ ⊃ α \end{matrix}

m が自然数のときのウカシュヴィッツの m 値論理の体系は上の体系に有限個の公理型を付け加えたものになっている。また, 上の体系に前節の公理型 W を付け加えると古典論理になる。

ウカシュヴィッツの 3 値論理に {x | x ∉ x} を項として認めるという包括化 (comprehension) 公理と代入原理を加えても矛盾しないことが証明できる。しかし, M. Shaw-Kwei[23] はウカシュヴィッツの 3 値論理に, 任意の論理式 α(x) について {x | α(x)} を項として認めるという無制限の包括化公理を付け加えると矛盾することを示した。この論文では, 自然数 n に対してはウカシュヴィッツの n 値論理に無制限の包括化公理を付け加えると矛盾することも示している。

Shaw-Kwei の論文には「ウカシュヴィッツの無限値論理の体系に無制限の包括化公理を付け加えると矛盾するか?」が興味深い未解決問題と述べられている。この問題はその 25 年後に R.B. White[28] が「無矛盾である」という形で解決した。解決された現代の目で見ても, この問題は相当な難問であったといえる。

White の結果によりウカシュヴィッツの無限多値論理上の (無制限な包括化公理を持つ) 集合論は無矛盾であることが分かったのであるが, その後その集合論の研究は進展しなかった。その体系が複雑すぎた上に, どうしても必要な複雑さとは思えなかったからであろう。

序論で述べたように包括化公理から矛盾を導くのには縮約規則が必要であった。ゲンツェンのシークエント計算において縮約規則などの構造に関する規則を除いて得られる論理を部分構造論理と 1990 年代に呼ぶようになった (cf. [18], [22])。縮約規則がなければ矛盾しないことに最初に気付いたのは Grišin[11] であった。さらに外延性公理が縮約規則を導き矛盾を導出することも示した ([12])。多値論理上の集合論でも同じような議論をしているのであるが, 縮約規則に焦点を当てていた訳ではなかった。この発見はされてみると大した事がないように見えるが大きな第一歩であった。 Grišin の体系は古典論理から縮約規則を除いたものであった。

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

4 BCK 論理を含む型なしラムダ計算

型なしラムダ計算 (type free lambda calculus) は項 M, N に対して項 MN を N ∈ M と, λx.M を {x | M} と思うことにより論理記号を表す定数があれば集合論の言語と考えられる。しかも, 自然数や順序対などは論理記号なしで定義できるので普通の集合論の言語より表現力が強いものである (ラムダ計算なしで順序対を定義するためにはペア {x, y} の定義が必要である。 {x, y} ≡_{def} {z | z = x or z = y} と定義する際に「or」を加法的なものにするか乗法的なものにするか悩ましいのである)(論理記号を使った表現力は同じである [19])。当然, その論理記号が古典論理や直観主義論理に従うならばラッセルの逆理と同様のカリーの逆理が導出される。チャーチがラムダ計算を考えた当初は論理定数を含んでいたのであるが, Kleene と Rosser[16] がそれが矛盾を含むことを発見してからは, 主に論理定数を除いた体系 (も非常に豊富な内容を含むので) が研究されてきた (cf. [14], [13])。

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

ほぼ古森 [17] にしたがって説明する。ラムダ項は型なしラムダ項のことであり, 可算個の定数を含み, その中には「Ξ, i, c」がある。体系 BCKβη の論理式はラムダ項のことである。体系 BCKβη の推論規則は次の 3 つである:

\begin{matrix}{Π_{1} \atop Ξαβ} & {Π_{2} \atop αγ} \\ βγ \end{matrix} (Ξe),  {k \atop αx} ; Π ; βx ; Ξαβ k(Ξi),  Π α ; β (βη) if α =_{βη} β.

ここで, 規則 (Ξi) においては変数 x は α, β および落ちていない仮定に自由に現われない。また, 一度に落とせる仮定は高々 1 つである, すなわち数字 k は高々 1 ヶ所にしか現われない。

項 Ξαβ の直観的な意味は ∀x(αx ⊃ βx) である。定数 i, c については i が以下の定義で使われてはいるが, それについての推論規則も公理もないので今のところ特別な意味はない。この言語は表現力が豊かで多くの論理記号や述語が以下のように省略記号として定義できる:

α ⊃ β ≡_{def} Ξ(Kα)(Kβ), where K ≡_{def} λxy.x;
⊤ ≡_{def} Ξii;
∀xα ≡_{def} Ξ(K⊤)(λx.α);
α + β ≡_{def} ∀y((α ⊃ y) ⊃ (β ⊃ y) ⊃ y);
α&β ≡_{def} ∀y((α ⊃ β ⊃ y) ⊃ y);
∃xα ≡_{def} ∀y(∀x(α ⊃ y) ⊃ y);
⊥ ≡_{def} ∀xx;
α ∈ β ≡_{def} βα;
α ∧ β ≡_{def} ∀x(∀y((y ⊃ α) ⊃ (y ⊃ β) ⊃ y ⊃ x) ⊃ x);
α ∨ β ≡_{def} ∀y((α ⊃ y) ∧ (β ⊃ y) ⊃ y);
α = β ≡_{def} Ξ(λx.xα)(λx.xβ);
!α ≡_{def} ⊤ = α.

後半の 4 つは [17] には述べられていない。最近になって分かったことである。ただし, この「!」は線形論理の「!」の性質を全ては持っていない。縮約がない体系では論理和と論理積については加法的なものと乗法的なものとの区別が必要であるが, どちらも定義できるのである (Petersen[19])。私が [17] を書いた当時は加法的なものは定義できないと考えていた。

「α = β」については次の推論規則が許される。

{k \atop α = β} ; ⋮ . ; γ ; (α = β) ⊃ γ k(=⊃i).

ただし, (=⊃i) において仮定はいくつでも落とせる。「!」については次の 2 つの推論規則が許される。

{Π \atop !α} ; α (!e),  {k \atop !α} ; Π ; β ; !α ⊃ β k(!⊃i)。

ただし, (!⊃i) において仮定はいくつでも落とせる。

R_{!} を λx.(¬!xx) の省略記号とする。上の二つが許される規則であることを使うと, 次のように R_{!}R_{!} であることが示せる。

\begin{matrix}\begin{matrix}\begin{matrix}{1 \atop !R_{!}R_{!}} ; R_{!}R_{!} & !e \\ ¬!R_{!}R_{!} \end{matrix} ; (代入 1) & {1 \atop !R_{!}R_{!}} \\ ⊥ \end{matrix} & (⊃-E) \\ ¬!R_{!}R_{!} \end{matrix} ; 1(!⊃-I) ; R_{!}R_{!} ; (代入 2)

つまり集合 R_{!} は自分自身を元として含むのである。

この「!」は線形論理の「!」とよく似た性質を持つが, 全く同じであると BCKβη が矛盾することになるので, 無矛盾性から異なる点もあることが分かる。「!」は様相概念の一種であるが, この体系でどのような様相概念が定義できるのかということも興味ある問題である。

5 汎用システム

汎用システムの例

無矛盾な体系無矛盾の仮定の基で
万能チューリング機械公理的自然数論 (Peano Arith.)
ラムダ計算公理的集合論 (ZF, GB)

古典述語論理直観主義述語論理

論文 [17] を書いた直後は, 体系 BCKβη の無矛盾性が容易に証明できるので, 無矛盾性が容易に証明できる体系などはあまり内容がないと考え, すぐに体系の強化を考えた。そして, 直後に書いた論文では, ここで述べた考察からすぐに矛盾することが分かる体系も提案している。確かに, 無矛盾性が容易に証明できる体系では, その中では数学を展開するのは不十分である。しかし, BCKβη は当初思っていたよりも豊かな体系のようである。

公理的集合論は古典述語論理の基で有限公理化される。このことは古典述語論理は無矛盾性は容易に証明できるが優れた汎用システムであることを示している (S.C. Kleene の 1952 年の結果

[15] はこのことを補強している)。体系 BCKβη は汎用システムであるラムダ計算を含んでいるので汎用システムである。しかし, より良い汎用システムになっているかどうかは古典述語論理などの論理のシミュレーションが簡単にできるかどうかにかかっている。

ここでは, 汎用システムとは古典述語論理をシミュレートできる体系で古典述語論理でそのシステムをシミュレートできるものと定義しておく。シミュレートの能力という意味では全ての汎用システムは同等なのであるが, 多くの体系を簡単にシミュレートできる体系がすぐれた汎用システムということになる。例として古典述語論理 CP と直観主義述語論理 IP を考えてみる。

古典述語論理 CP の論理記号として「⊃, ¬, ∃」を採用する。 Glivenko の定理により任意の CP の論理式 α に対して次が成立する:

α が CP で証明可能である ⟺ ¬¬α が IP で証明可能である.

これは古典述語論理が非常に簡単に直観主義述語論理 (の fragment) でシミュレートできることを示している。

一方, 直観主義述語論理を古典述語論理でシミュレートしようとするとやや複雑である。論理式 α に対して, α が任意の Kripke frame で正しいという内容を表す論理式 α^{∗} にする変換^{∗} を考えると次が成立する:

α が IP で証明可能である ⟺ α^{∗} が CP で証明可能である.

この方法が最も簡単に古典述語論理で直観主義述語論理をシミュレートする方法であるが前述の逆のシミュレーションに比べて複雑である。この意味で直観主義述語論理は古典述語論理より優れた汎用システムであるということができる。

6 体系 BCKβη の汎用性

体系 BCKβη はラムダ計算を含んでいるので汎用システムである。ここで問題にするのは優れた汎用システムであるかどうかということである。直観主義述語論理を簡単にシミュレートできる可能性があることを示唆したい。なお, 逆の直観主義述語論理で BCKβη を簡単にシミュレートする方法はなさそうである。つまり以下に述べることが言えると体系 BCKβη の方が直観主義述語論理より優れた汎用システムであるということになる。

α を直観主義述語論理 (NJ) の論理式とする。簡単のため, α には現れる論理記号は「⊃, ⊥, ∀」の 3 つだけで, 関数記号は 2 変数関数記号 f のみ, 述語記号は 2 変数述語記号 p のみが現れるものとする。 BCKβη の論理式 α^{∘} を以下のように帰納的に定義する。左側の α が atomic のとき α^{∘} ≡ α, (α ⊃ β)^{∘} ≡ α^{∘} ⊃ β^{∘}, (∀xα)^{∘} ≡ Ξi(λx.α^{∘})(= ∀x(ix ⊃ α^{∘})).

また, 論理式 A と論理式の列 Σ_{α} を以下のように定義する。

A ≡!(∀x∀y(∀z(xz =!(xz)) ⊃ ∀z(yz =!(yz)) ⊃ (Ξxy) =!(Ξxy)))
Σ_{α} ≡!(∀x∀y(i(fxy))),!(∀x∀y(pxy =!(pxy)))

この定義は定数 i などの解釈を以下のように考えると読みやすい。 ix の意味は x は個体である, 項 α =!α の意味は α は命題であるである。

閉論理式 α にたいして閉論理式 α^{∗} を次のように定義する:

α^{∗} ≡ (ic,!(∀x(ix =!(ix))), ⊥ =!⊥, A, Σ_{α}) ⊃ α^{∘}.

ここで, 論理式の列 Γ ≡ α_{1}, α_{2}, ..., α_{n} にたいして Γ ⊃ β は α_{1} ⊃ α_{2} ⊃ ⋯ α_{n} ⊃ β と定義する。閉でない論理式 α については α の普遍閉包を α^{u} として α^{∗} ≡ (α^{u})^{∗} と定義する。予想 1

α が直観主義述語論理で証明できる⟺ α^{∗} 体系 BCKβη で証明できる.

この予想の「⟹」の部分は (http://www.math.s.chiba-u.ac.jp/˜ komori/masters thesis/2003/ takayama/takayama.dvi にある高山扶美彦の修士論文の主定理と同様に証明できる) ルーチンワークである。「⟸」の部分の証明にはモデルを使う必要があると思われる。すなわち, α を not valid ととする Kripke モデルはから α^{∗} を not valid にする体系 BCKβη のモデルを作ってやればよい。しかし, まだその構成には成功していない。直観主義論理の Kripke モデルはおなじみのものであるが, 古森 ([17]) に述べられている体系 BCKβη のモデルは知られていないので, 体系 BCKβη のモデルの定義を述べてこの小論を終わりにする。

次の 2 つの条件を満たす構造 ⟨M, ∗, 1; ≤⟩ を PO 可換半群という:

1. ⟨M, ∗, 1⟩ は単位可換半群である,

2. ⟨M, ≤⟩ は 1 を最小限とする順序集合で, 任意の l, m, n ∈ M に対して m ≤ n ならば m ∗ l ≤ n ∗ l である.

定義 2 D をラムダ計算の strict Scott-Meyer モデル (cf. [14] p.121) ⟨D, ·, e⟩ とする。 ξ を D の元とする。 M(= ⟨M, ∗, 1, ≤⟩) を単位可換半群, ⊧ を M × D の部分集合とする ((m, a) ∈⊧ を m ⊧ a とかく)。任意の m, n ∈ M と a, b ∈ D についての次の 3 つの条件を満たすとき構造 ⟨M, D, ξ, ⊧⟩ を体系 BCKβη の Kripke モデルという:

1. m ≤ n かつ m ⊧ a ならば n ⊧ a,

2. m ⊧ ξ · a · b ⟺ 任意のc ∈ D と l ∈ M に対してl ⊧ a · c ならばm ∗ l ⊧ b · c,

3. 任意のラムダ項 A, B に対して, λβη ⊢ A = B ならば D ⊧ A − B.

このモデルについては [17] で, 体系 BCKβη に対して完全性定理が証明されている。

参考文献

[1] Martin W. Bunder. Set theory based on combinatory logic. PhD thesis, University of Amsterdam, 1969.

[2] Martin W. Bunder. Some consistency proofs and a characterization of inconsistency proofs in liiative combinatory logic. Journal of Symbolic Logic, 52:89–110, 1986.

[3] Cesare Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo matematico di Palermo, 11:154–164, 1897.

[4] Alonzo Church. A set of postulates for the foundation of logic I. Annals of Mathematics, ser. 2, 33:346–366, 1932.

[5] Alonzo Church. A set of postulates for the foundation of logic II. Annals of Mathematics, ser. 2, 34:839–864, 1933.

[6] Wil Dekkers, Martin Bunder, and Henk Barendregt. Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus. Archive for Mathematical Logic, 37:327–341, 1998.

[7] Abraham A. Fraenkel. Der Begriff “definit” und die Unabhängigkeit des Auswahlsaxioms. Sitzungsberichte der Preussisehen Akademie der Wissenschaften, Physikalischmathematische Klasse, pages 253–257, 1922.

[8] Abraham A. Fraenkel, Yehoshua Bar-Hillel, and Azriel Levy. Foundation Set Theory, volume 67 of Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1973.

[9] Gottlob Frege. Letter to Russell. Translated in [27], 1902.

[10] Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. Translated in [24].

[11] V. N. Grišin. A nonstandard logic, and its application to set theory. In Studies in Formalized Languages and Nonclassical Logics, pages 135–171. “Nauka”, Moscow, 1974. (Russian).

[12] V. N. Grišin. Predicate and set-theoretic calculi based on logic without contractions. Math. USSR Izvestija, 18:41–59, 1982.

[13] J. Roger Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.

[14] J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and λ–calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

[15] Stephen C. Kleene. Two papers on the predicate calculus. Number 10 in Memoirs of the American Mathematical Society. American Mathematical Society, 1952.

[16] Stephen C. Kleene and J. Barkley Rosser. The inconsistency of certain formal logics. Annals of Mathematics, 36:630–636, 1935.

[17] Yuichi Komori. Illative combinatory logic baed on BCK–logic. Mathematica Japonica, 34:585–596, 1989.

[18] Hiroakira Ono and Yuichi Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50:169–201, 1985.

[19] Uwe Petersen. Logic without contraction as based on inclusion and unrestricted abstraction. Studia Logica, 64:365–403, 2000.

[20] Alan Rose and J. Barkley Rosser. Fragments of many-valued statement calculi. Trans. Amer. Math. Soc., 87:1–53, 1958.

[21] Bertrand Russell. Letter to Frege. Translated in [27], 1902.

[22] Peter Schroeder-Heister and Kosta Došen, editors. Substructural Logics, volume 2 of Studies in Logic and Computation. Oxford Univ. Press, 1993.

[23] Moh Shaw-Kwei. Logical paradoxes for many valued systems. Journal of Symbolic Logic, 19:37–40, 1954.

[24] Manfred E. Szabo. The collected papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.

[25] Jan Łukasiewicz. O logice trójwartościowej. Ruch filozoficzny, 5:169–171, 1920.

[26] Jan Łukasiewicz and Alfred Tarski. Untersuchungen über den Aussagenkalkül. Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie, Classe III, 23:30– 50, 1930.

[27] Jean van Heijenoort. From Frege to Gödel. Harvard University Press, third edition, 1976.

[28] Richard B. White. The consistency of the axiom of comprehension in the infinite-valued predicate logic of Łukasiewicz. Journal of Philosophical Logic, 8:509–534, 1979.

[29] Richard B. White. A demonstrably consistent type-free extension of the logic BCK. Mathematica Japonica, 32:149–169, 1987.

[30] Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 65:261–281, 1908.