日々の流転

λ. Beyond Classical Domain Theory by Alex Simpson

これは面白い。Synthetic Domain Theory って、昔、長谷川立氏のチュートリアル「パラメトリック・ポリモルフィズム」で

• 「この節では，パラメトリシティ原理を満たすモデルを幾つか紹介してみたい．いずれもかなり重たい数学を用いるので，深入りはしないことにしておく」
• 「もう1つのモデルは，直観主義的宇宙を用いる方法で得られる．これにはさらに難しい数学が必要なので，表面的なことを述べるだけにする」

と難しいことが随分強調されていたので、きっと難しいのだろうなと思って近づいていなかったんだけど、このスライドは分かりやすかった。effective topos とか realizability interpretation とか計算可能性とか、そういう難しいことを一切知らなくても、直観主義論理と圏論さえ知っていれば使えそうだと感じた。

そういえば、Synthetic Domain Theory については、長谷川真人氏の「自己言及の論理と計算」(参考: ヒビルテ(2003-06-29))の「Advanced Topic 直観主義的抜け道について」でも触れられていたな。ついでに、以下のように書いてあったので、今CLTT読書会で読んでいるCLTTにもそういう話が出てくるらしい。

これらの事柄はかなり専門的であり，今のところ研究論文以外に情報源はあまりないが，B. Jacobs: Categorical Logic and Type Theory (North-Holland, 1999) には，そのような直観主義的集合論のモデルに関するくわしい解説が含まれている．

以下、読んでいて気づいた点のメモや練習問題を解いてみたりしたもの。

Simple constructions (20)

集合の直積が集合なのは、A×B = {z | ∃x∈A, y∈B. z=(x,y)} = ∪_x∈A ∪_y∈B {z | z=(x,y) ∨ z=(x,y)} で、Indexed union axiom と pairing axiom から。

クラスA, 集合X に対してのクラス A^X の定義は、⊆の定義をクラスに一般化すれば、P(A)の定義もクラスに一般化されるので、Aが集合の場合と同じでよいはず。

• A⊆B ⇔ (∀x. x∈A ⇒ x∈B)
• P(A) = {z | z⊆A}
• A^X = {f ∈ P(X×A) | ∀x∈X. ∃!y∈A. (x,y)∈f}

Countable choice (22)

• axiom of choice を ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. φ[f(x)/y]
• countable choice を ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. φ[f(n)/y]

と書いてあるが、これらはそれぞれ

• ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. ∀x∈X. φ[f(x)/y] と
• ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. ∀n∈N. φ[f(n)/y]

の誤りだろう。

【2010-12-23 追記】 それはそれとして、型理論やBHK解釈に慣れ親しんでいると、選択公理は推論規則から自明に証明できてしまう気がするけど、こう書いてあるということは、ここではそうではないということで、なんだか少し気持ち悪い。どういう体系になっているのか、気になるところ。

Truth values (23)

⌜_⌝に関する幾つかの性質

• ⌜φ⌝=⊤ ⇔ {∅ | φ}={∅} ⇔ φ
• ⌜φ⌝=⊥ ⇔ {∅ | φ} = {φ | ⊥} ⇔ ¬φ
• X∈Ωに対して、∅∈⌜X=⊤⌝={∅ | X=⊤} ⇔ X=⊤ ⇔ ∅∈X より、 ⌜X=⊤⌝=X

以降では ⌜φ⌝=⊤ のことを単に ⌜φ⌝ と書いているようだ。

P(X) ≅ X→Ω の証明は、

• F: P(X)→(X→Ω)
  F(A) = {(x, ⌜x∈A⌝) | x∈X}
• G: (X→Ω)→P(X)
  G(f) = {x∈X | f(x)=⊤}

とおけば、

• GF(A) = {x | ⌜x∈A⌝=⊤} = {x | x∈A} = A かつ
• FGf = {(x, ⌜f(x)=⊤⌝) | x∈X} = {(x, f(x)) | x∈X} = f

なので言える。

Booleans (24)

Ω⊆2がLEM(排中律)と同値であることの証明。

LEMを仮定すると、以下より Ω⊆2

x∈Ω
⇒ (∃y. y∈x)∨¬(∃y. y∈x)  {- by LEM -}
⇔ x=⊤ ∨ x=⊥
⇔ x∈{x | x=⊤ ∨ x=⊥}=2

逆にΩ⊆2とすると、任意のφに対して、⌜φ⌝∈Ω⊆2 ⇒ ⌜φ⌝=⊤ ∨ ⌜φ⌝=⊥ ⇔ φ ∨ ¬φ なので、LEMが成り立つ。

Semidecidable properties and Markov's principle (25)

p,q∈Σ ⇒ p∧q ∈ Σ の証明

• p∈Σ より、P: N→2 が存在して p=⌜∃n∈N. P(n)⌝
• q∈Σ より、Q: N→2 が存在して q=⌜∃n∈N. Q(n)⌝

R(n) = P(π1(n))∩Q(π2(n)) とおくと、p∧q = {∅ | ∅∈p ∧ ∅∈q} = {∅ | ∃n∈N. P(n) ∧ ∃n∈N. Q(n)} = {∅ | ∃n∈N. R(n)} ∈ Σ

「p: N→Σ ならば (∃n∈N. p(n)) ∈ Σ」というのがあるけど、結論部は (∨_n∈N p(n)) ∈ Σ のことだろう。 ∀n∈N. p(n)∈Σ より ∀n∈N. ∃Q:N→2. p(n)=⌜∃m∈N. Q(m)=⊤⌝ で、ここで可算選択公理(countable choice)を使うと、 f : N→N→2 が存在して ∀n∈N. p(n)=⌜∃m∈N. f(n)(m)=⊤⌝ 。R(n) = f(π1(n))(π2(n)) とおくと、∨_n∈N p(n) = ∪_n∈N p(n) = {x | ∃n∈N. x∈p(n)} = {x | ∃n∈N. ⌜∃m∈N. f(n)(m)=⊤⌝=⊤} = {x | ∃n∈N, m∈N. f(n)(m)=⊤} = {x | ∃n∈N. R(n)=⊤} ∈ Σ

Towards synthetic domain theory (27)

N, 2, Q が fixpoint property を持たないこと。

Nの場合sが不動点を持たない。P={n∈N|s(n)≠n)とおくと、s(0)≠0なので0∈P、n∈Pとするとs(n)≠nなのでs(s(n))≠s(n)でs(n)∈P 。よって P=N 。

Ωの場合 not: Ω→Ω を not(x) = ⌜∅∉x⌝ とすると not(x)=x ⇔ ⌜∅∉x⌝=⌜∅∈x⌝ ⇒ ⊥ より、notには不動点が存在しない。

2の場合も、not を 2→2 に制限すれば同じ。

Basic propertis of probabilistic domains (66)

「Then (I,0,⊕) ⋌ η_D since (I,0,⊕) is an object of ProbDom'_⊥⊕」というのが理解できず悩んでしまったが、これはまさにユニットの性質そのもの。