「ラムダ計算 + 論理」の体系 BCKβ での集合論のシミュレーション

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

2007 年 11 月 30 日

1 序論

最近, 体系 BCKβ (当然, BCKβη でも) において, 空集合の外延性からも矛盾が出ることが分かった。その結果, 空集合から順次必要な集合を作っていくという方法で BCKβ で外延性公理を持つ集合論をシミュレートすることはできない。色々なおかしな挙動をするクラスの中から性質のよいクラス (それを集合と呼ぼう) を選び出し (選び出すための述語が i), その小さな世界だけで考えると外延性が成り立っている, との考えでシミュレートしてみることにする。しかし, その証明は完成していないので, 問題として提出したい。

2 「ラムダ計算 + 論理」の体系 BCKβ

ほぼ古森 [3] にしたがって説明する。ラムダ項は型なしラムダ項のことであり, 可算個の定数を含み, その中には「Ξ, i」がある。体系 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 については i が以下の定義で使われてはいるが, それについての推論規則も公理もないので今のところ特別な意味はない。この言語は表現力が豊かで多くの論理記号や述語が省略記号として定義できるが以下では後で必要な定義だけを記す:

α ⊃ β ≡_{def} Ξ(Kα)(Kβ), where K ≡_{def} λxy.x;
⊤ ≡_{def} Ξii;
∀xα ≡_{def} Ξ(K⊤)(λx.α);
⊥ ≡_{def} ∀xx;
α = β ≡_{def} ∀x(xα ⊃ xβ);
!α ≡_{def} (⊥ ⊃ ⊥) = α.

ここで定義された ⊃ などについて直観主義論理 NJ の推論規則がそのまま派生規則になっている。ただし, ⊃ の導入 ⊃ i については, 高々 1 つの仮定だけを落とすことができるという制限が付く。また, 「!」は線形論理の「!」に似ているが線形論理の「!」の性質を全ては持っていない。

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

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

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

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

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

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

\begin{matrix}\begin{matrix}\begin{matrix}{1 \atop !QQ} ; QQ & !e \\ ¬!QQ \end{matrix} ; β & {1 \atop !QQ} \\ ⊥ \end{matrix} & ⊃ e \\ ¬!QQ \end{matrix} ; 1(! ⊃ i) ; QQ ; β

つまりクラス Q は自分自身を元として含むのである。

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

縮約規則がなければ無制限な包括化公理を持つ集合論が矛盾しないことに最初に気付いたのは Grišin[1] であった。さらに外延性公理が縮約規則を導き矛盾を導出することも示した ([2])。 U.

Petersen[4] の仕事からは全体集合についての外延性だけで矛盾が出てくることが窺える。ところが最近, 空集合のような小さな集合の外延性だけで矛盾が導き出されるということが分かった。

まず, BCK 論理でも次の形の二重否定を除去する規則が派生規則である。証明は直観主義論理において派生規則であることの証明と同じである。

{¬¬¬α \atop ¬α} D

また, 空集合についての外延性は次のように述べることができる。 ¬α が仮定なしで証明可能なとき, ⊥ ⊃ α および α ⊃ ⊥(≡ ¬α) がともに仮定なしで証明可能である。その結果, 集合 λx.⊥ についての外延性は (λx.⊥) = (λx.α) となる。 λx.⊥ は空集合であるので, 空集合についての外延性を認めるということは, 次の規則を認めるということである。

{¬α \atop (λx.⊥) = (λx.α)} ext2

次の推論図 (その中の δ については δ ≡ λy.x(λx.yu ⊃ ⊥)) を見ていただきたい。

\begin{matrix}{¬α \atop (λx.⊥) = (λx.α)} & ext2 \\ (δ(λx.⊥)) ⊃ (δ(λx.α)) \end{matrix} ; ∀e ; x(⊥ ⊃ ⊥) ⊃ x(¬α) ; β ; !¬α ; ∀i

この規則から次の規則が許容規則 (仮定がすべて落ちているときのみ使える規則) であることが分かる。

{¬α \atop !¬α} ext

R を λx.(¬!¬¬xx) の省略記号とする。次のように空集合の外延性を使うと矛盾が導かれる。

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}{1 \atop !¬¬RR} ; ¬¬RR & !e \\ ¬¬¬!¬¬RR \end{matrix} & β \\ ¬!¬¬RR \end{matrix} ; D & {1 \atop !¬¬RR} \\ ⊥ \end{matrix} & ⊃ e \\ ¬!¬¬RR \end{matrix} ; 1(! ⊃ i) & \begin{aligned}{2 \atop ¬RR} & \begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}{1 \atop !¬¬RR} ; ¬¬RR & !e \\ ¬¬¬!¬¬RR \end{matrix} & β \\ ¬!¬¬RR \end{matrix} ; D & {1 \atop !¬¬RR} \\ ⊥ \end{matrix} & ⊃ e \\ ¬!¬¬RR \end{matrix} ; 1(! ⊃ i) ; RR ; β \\ & ⊥ \end{aligned} ; ¬¬RR ; 2(⊃ i) ; !¬¬RR ; ext \\ ⊥ \end{matrix}

3 体系 BCKβ での集合論のシミュレート

古典論理上の集合論は直観主義論理 (の {⊃, ⊥, ∀}-断片) 上の集合論で容易にシミュレートできる (Glivenko の定理による) ので, 直観主義論理上の集合論のシミュレートを考える。直観主義論理の {⊃, ⊥, ∀}-断片を NJ と呼ぶことにする。集合論の言語としては二項述語 ∈ のみを持つものを考える。

!(iα) と α ⊃!α とをそれぞれ jα と pα と記すことにする。すなわち

jα ≡!(iα) pα ≡ α ⊃!α.

α を NJ 上の論理式とする。 BCKβ の論理式 α^{∘} を以下のように帰納的に定義する。 (⊥)^{∘} ≡ ⊥, (x ∈ y)^{∘} ≡ yx, (α ⊃ β)^{∘} ≡ α^{∘} ⊃ β^{∘}, (∀xα)^{∘} ≡ ∀x(jx ⊃ α^{∘}).

また, 以下の 4 つ論理式を並べた列を Δ とする。

j(λx.⊥)
!(∀x∀y(px ⊃ py ⊃ p(x ⊃ y)))
!(∀x(∀y(jy ⊃ p(xy))) ⊃ p(∀y(jy ⊃ xy)))
!(∀x∀y(jx ⊃ jy ⊃ p(xy)))

この定義は j などの解釈を以下のように考えると読みやすい。 jx の意味は x は集合である, 項 pα の意味は α は命題であるである。

集合論の論理式の列 Σ(≡ α_{1}, α_{2}, ...) (可算無限列でもよい) にたいして Σ^{∘} ≡ α_{1}^{∘}, α_{2}^{∘}, ... とする。

定理 1 Σ を集合論の論理式の列, α を集合論の論理式とすると,

Σ ⊢_{NJ} α ⟹ Σ^{∘}, Δ ⊢_{BCKβ} α^{∘}.

この定理は http://www.math.s.chiba-u.ac.jp/˜ komori/masters thesis/2003/ takayama/takayama.dvi にある高山扶美彦の修士論文の主定理と同様に (少しこちらの方が易しい) 証明できる。その際に補助定理「任意の集合論の論理式 α にたいして, ⊢_{BCKβ} pα^{∘} である」が鍵となる。

この定理の逆はまだ証明できていない。古森 ([5]) では, α は命題であるを α =!α としていたが逆の証明は α は命題であるをここでの定義を採用するほうが易しそうである。いずれにしても, その証明にはモデルを使う必要があると思われる。すなわち, Σ ⊬_{NJ} α を示す Kripke モデルから Σ^{∘}, Δ ⊬_{BCKβ} α^{∘} を示す体系 BCKβ のモデルを作ってやればよい。直観主義論理の Kripke モデルはおなじみのものであるが, 体系 BCKβ のモデルは古森 ([3]) に述べられている。

参考文献

[1] 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).

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

[3] Yuichi Komori. Illative combinatory logic baed on BCK–logic. Mathematica Japonica, 34, 1989. http://www.math.s.chiba-u.ac.jp/˜ komori/papers/illative/.

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

[5] 古森雄一. 汎用システムとしての「ラムダ計算 + 論理」 . 数理解析研究所講究録, 1533:39–48, 2007. http://www.math.s.chiba-u.ac.jp/˜ komori/symposium/suukaiken/komori8.pdf.