存在定理の構成的証明可能性について

存在定理の構成的証明可能性について
藤原誠
数学専攻博士課程後期 3 年 (日本学術振興会特別研究員 DC2)
ラムダ計算と論理の早春セミナー 2015
2015 年 3 月 17 日
1 / 21
数学基礎論
数学を形式化し，数学的に解析する！
2 / 21
数学基礎論
数学を形式化し，数学的に解析する！
数学における定理
≈
(算術的) 公理体系における論理式.
2 / 21
記法
論理式 (e.g. ¬A → ¬B) は論理結合子 (∧, ∨, →, ¬, ∃, ∀)
を用いて記述される.
公理体系は公理と推論規則から成る．
公理体系 Γ と論理式 S に対し，Γ + S は Γ に S を公理と
して加えて得られる公理体系を表す．
Γ ⊢ S (Γ で S が証明できる): Γ の公理から Γ の推論規則
によって S を導出する証明図が存在する．
例. Γ(standard) + (A → B) ⊢ (¬B → ¬A).
A
⋄
A→B
B
→⊥
B
⊥ ⋄
A →⊥ ⋆
¬B → ¬A
⋆
3 / 21
主題．
存在定理の構成 (≈ 計算) 的証明可能性．
4 / 21
主題．
存在定理の構成 (≈ 計算) 的証明可能性．
存在定理の例．(中間値の定理)
全ての f (0) < 0 < f (1) なる連続関数 f : [0, 1] → R に対し，
f (m) = 0 なる m ∈ (0, 1) が存在する．
f
0
m
1
4 / 21
主結果の概要
多くの存在定理 T に対し，以下は同値である．
1
2
T が構成的数学 EL で証明可能．
T が計算可能数学 RCA で一様存在証明可能．
5 / 21
構成的数学 (Constructive Mathematics) と
直観主義論理 (Intuitionistic Logic)
構成的数学 (ブラウアー，マルコフ，ビショップ) は，
その全ての議論において「∼が存在する」を「∼が構
成できる」と解釈する数学．
6 / 21
構成的数学 (Constructive Mathematics) と
直観主義論理 (Intuitionistic Logic)
構成的数学 (ブラウアー，マルコフ，ビショップ) は，
その全ての議論において「∼が存在する」を「∼が構
成できる」と解釈する数学．
構成的数学の始まりはブラウアー (20 世紀初頭) の直観
主義数学 (数学は人間の精神の産物...)．
6 / 21
構成的数学 (Constructive Mathematics) と
直観主義論理 (Intuitionistic Logic)
構成的数学 (ブラウアー，マルコフ，ビショップ) は，
その全ての議論において「∼が存在する」を「∼が構
成できる」と解釈する数学．
構成的数学の始まりはブラウアー (20 世紀初頭) の直観
主義数学 (数学は人間の精神の産物...)．
1930 年代にハイティングとコルモゴロフはブラウアー
の直観主義数学の公理化を試みた．
6 / 21
構成的数学 (Constructive Mathematics) と
直観主義論理 (Intuitionistic Logic)
構成的数学 (ブラウアー，マルコフ，ビショップ) は，
その全ての議論において「∼が存在する」を「∼が構
成できる」と解釈する数学．
構成的数学の始まりはブラウアー (20 世紀初頭) の直観
主義数学 (数学は人間の精神の産物...)．
1930 年代にハイティングとコルモゴロフはブラウアー
の直観主義数学の公理化を試みた．
⇒ 直観主義論理！
6 / 21
BHK(Brouwer-Heyting-Kolmogorov) 解釈
ハイティングやコルモゴロフ，クライゼルらによって提唱
された論理結合子 (∧, ∨, →, ¬, ∃, ∀) の (非形式的) 解釈．
7 / 21
BHK(Brouwer-Heyting-Kolmogorov) 解釈
ハイティングやコルモゴロフ，クライゼルらによって提唱
された論理結合子 (∧, ∨, →, ¬, ∃, ∀) の (非形式的) 解釈．
⊥ の証明はない．
A ∧ B の証明は A の証明 p と B の証明 q のペア (p, q) である．
A ∨ B の証明は自然数 n と証明 p のペア (n, p) であり，n = 0
かつ p は A の証明，または n ̸= 0 かつ p は B の証明である．
A → B の証明は任意の A の証明を B の証明に変換する手続
きである．
∀xA(x) の証明は任意の元 d を A(d) の証明に変換する手続き
である．
∃xA(x) の証明は元 d と証明 p のペア (d, p) であり，p は
A(d) の証明である．
7 / 21
BHK(Brouwer-Heyting-Kolmogorov) 解釈
ハイティングやコルモゴロフ，クライゼルらによって提唱
された論理結合子 (∧, ∨, →, ¬, ∃, ∀) の (非形式的) 解釈．
⊥ の証明はない．
A ∧ B の証明は A の証明 p と B の証明 q のペア (p, q) である．
A ∨ B の証明は自然数 n と証明 p のペア (n, p) であり，n = 0
かつ p は A の証明，または n ̸= 0 かつ p は B の証明である．
A → B の証明は任意の A の証明を B の証明に変換する手続
き p とそれの証明 q のペア (p, q) である．
∀xA(x) の証明は任意の元 d を A(d) の証明に変換する手続き
p とそれの証明 q のペア (p, q) である．
∃xA(x) の証明は元 d と証明 p のペア (d, p) であり，p は
A(d) の証明である．
7 / 21
BHK(Brouwer-Heyting-Kolmogorov) 解釈
ハイティングやコルモゴロフ，クライゼルらによって提唱
された論理結合子 (∧, ∨, →, ¬, ∃, ∀) の (非形式的) 解釈．
⊥ の証明はない．
A ∧ B の証明は A の証明 p と B の証明 q のペア (p, q) である．
A ∨ B の証明は自然数 n と証明 p のペア (n, p) であり，n = 0
かつ p は A の証明，または n ̸= 0 かつ p は B の証明である．
A → B の証明は任意の A の証明を B の証明に変換する手続
き p とそれの証明 q のペア (p, q) である．
∀xA(x) の証明は任意の元 d を A(d) の証明に変換する手続き
p とそれの証明 q のペア (p, q) である．
∃xA(x) の証明は元 d と証明 p のペア (d, p) であり，p は
A(d) の証明である．
(論理式として表される) 命題 T が真 :=T が BHK 証明可能．
7 / 21
直観主義論理
古典論理 = 直観主義論理 + 排中律公理 A ∨ ¬A.
8 / 21
直観主義論理
古典論理 = 直観主義論理 + 排中律公理 A ∨ ¬A.
¬¬A → A
(∀xA(x) → B) → ∃x(A(x) → B)
(A → ∃xB(x)) → ∃x(A → B(x))
直観主義論理
×
×
×
古典論理
◦
◦
◦
8 / 21
直観主義論理
古典論理 = 直観主義論理 + 排中律公理 A ∨ ¬A.
¬¬A → A
(∀xA(x) → B) → ∃x(A(x) → B)
(A → ∃xB(x)) → ∃x(A → B(x))
直観主義論理
×
×
×
古典論理
◦
◦
◦
直観主義二階 (自然数と自然数上の関数を扱える) 算術
EL · · · (選択公理を認めない) 構成的数学の公理体系．
8 / 21
直観主義論理
古典論理 = 直観主義論理 + 排中律公理 A ∨ ¬A.
¬¬A → A
(∀xA(x) → B) → ∃x(A(x) → B)
(A → ∃xB(x)) → ∃x(A → B(x))
直観主義論理
×
×
×
古典論理
◦
◦
◦
直観主義二階 (自然数と自然数上の関数を扱える) 算術
EL · · · (選択公理を認めない) 構成的数学の公理体系．
マルコフ原理 MP : ¬¬∃xAqf (x) → ∃xAqf (x).
· · · プログラム Φ が「停止しないことはない」ならば Φ
は「停止する」．
8 / 21
直観主義論理
古典論理 = 直観主義論理 + 排中律公理 A ∨ ¬A.
¬¬A → A
(∀xA(x) → B) → ∃x(A(x) → B)
(A → ∃xB(x)) → ∃x(A → B(x))
直観主義論理
×
×
×
古典論理
◦
◦
◦
直観主義二階 (自然数と自然数上の関数を扱える) 算術
EL · · · (選択公理を認めない) 構成的数学の公理体系．
マルコフ原理 MP : ¬¬∃xAqf (x) → ∃xAqf (x).
· · · プログラム Φ が「停止しないことはない」ならば Φ
は「停止する」．
事実．
EL ⊊ EL + MP ⊊ EL + (A ∨ ¬A).
8 / 21
(形式化された)Realizability 翻訳 (クリーネ, 1960’s):
存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) が EL で証明可能
⇔ f から g を構成するプログラムがあり，その正当性
が EL で証明できる．
存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) が EL + MP で証明可能
⇔ f から g を構成するプログラムがあり，その正当性
が EL + MP で証明できる．
9 / 21
(形式化された)Realizability 翻訳 (クリーネ, 1960’s):
存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) が EL で証明可能
⇔ f から g を構成するプログラムがあり，その正当性
が EL で証明できる．
存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) が EL + MP で証明可能
⇔ f から g を構成するプログラムがあり，その正当性
が EL + MP で証明できる．
存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) が EL(+MP) で証明可能
≈
f から g を構成するプログラムがあり，かつそのプログラム
の正当性を証明するプログラムがある．
9 / 21
逆数学 (Reverse Mathematics)
目的は「数学の諸定理を論理的複雑さの観点から分類
する」こと．
10 / 21
逆数学 (Reverse Mathematics)
目的は「数学の諸定理を論理的複雑さの観点から分類
する」こと．
数学の諸定理を二階算術の弱い部分公理体系 RCA0 の
上で形式化し，それらと集合存在公理 (e.g. WKL,
ACA) の同値性を調べる．
10 / 21
逆数学現象 (1970 年代∼)
多くの古典的な数学の定理は RCA0 で証明できるか，RCA0
上，弱ケーニヒの補題 WKL または算術的集合存在公理
ACA と同値になる．
RCA0 ⊂ RCA ⊬ WKL.
WKL0 :≡ RCA0 + WKL ⊬ ACA.
ACA0 :≡ RCA0 + ACA ⊢ WKL.
Mathematial Theorems
ACA0
WKL0
RCA0
11 / 21
逆数学の例 (フリードマン，シンプソン，田中 etc.)
ACA
WKL
RCA0
ボルツァーノ＝ワイエルシュトラスの定理.
任意の可算可換環は極大イデアルを持つ．
可算体上の可算ベクトル空間は基底を持つ．
ケーニヒの補題．
可算無限グラフに対する結婚定理．
ブラウアーの不動点定理．
可算個の開集合によって被覆されるコンパクト距
離空間は有限部分被服を持つ．
任意の可算可換環は素イデアルを持つ．
中間値の定理.
ベールの範疇定理.
任意の可算体は代数閉体を持つ．
可算体上の有限生成ベクトル空間は基底を持つ．
可算無限グラフに対する実効的結婚定理．
有限な対象に関する定理．
12 / 21
RCA0 : 算術の基本公理 +∆01 (計算可能) 集合存在公理
+Σ01 数学的帰納法公理．
13 / 21
RCA0 : 算術の基本公理 +∆01 (計算可能) 集合存在公理
+Σ01 数学的帰納法公理．
RCA: 算術の基本公理 +∆01 (計算可能) 集合存在公理 +
数学的帰納法公理.
RCA ≈ 計算可能数学．
13 / 21
RCA0 : 算術の基本公理 +∆01 (計算可能) 集合存在公理
+Σ01 数学的帰納法公理．
RCA: 算術の基本公理 +∆01 (計算可能) 集合存在公理 +
数学的帰納法公理.
RCA ≈ 計算可能数学．
事実．
構成的数学 EL ⊊ EL + MP ⊊ EL + (A ∨ ¬A) = RCA.
13 / 21
存在定理の計算可能性と RCA 証明可能性
計算可能数学 RCA ⊢ ∀f (φ(f ) → ∃g ψ(f , g )) ≈
Muchnik 還元可能性, i.e. φ(f ) を満たす f ごとにオラク
ル付きチューリング機械のプログラム Φ が存在し，
ψ(f , g ) を満たす g は f をオラクルとしてプログラム Φ
で計算可能．
Medvedev 還元可能性, i.e. オラクル付きチューリング機
械のプログラム Φ が一様に存在し，φ(f ) を満たす f に
対し ψ(f , g ) を満たす g は f をオラクルとしてプログラ
ム Φ で計算可能．
14 / 21
存在定理の計算可能性と RCA 証明可能性
計算可能数学 RCA ⊢ ∀f (φ(f ) → ∃g ψ(f , g )) ≈
Muchnik 還元可能性, i.e. φ(f ) を満たす f ごとにオラク
ル付きチューリング機械のプログラム Φ が存在し，
ψ(f , g ) を満たす g は f をオラクルとしてプログラム Φ
で計算可能．
数学 ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) なる原始再帰的
関数項 (≈ プログラム)Φ が存在する．
Medvedev 還元可能性, i.e. オラクル付きチューリング機
械のプログラム Φ が一様に存在し，φ(f ) を満たす f に
対し ψ(f , g ) を満たす g は f をオラクルとしてプログラ
ム Φ で計算可能．
14 / 21
存在定理の計算可能性と RCA 証明可能性
計算可能数学 RCA ⊢ ∀f (φ(f ) → ∃g ψ(f , g )) ≈
Muchnik 還元可能性, i.e. φ(f ) を満たす f ごとにオラク
ル付きチューリング機械のプログラム Φ が存在し，
ψ(f , g ) を満たす g は f をオラクルとしてプログラム Φ
で計算可能．
数学 ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) なる原始再帰的
関数項 (≈ プログラム)Φ が存在する．
Medvedev 還元可能性, i.e. オラクル付きチューリング機
械のプログラム Φ が一様に存在し，φ(f ) を満たす f に
対し ψ(f , g ) を満たす g は f をオラクルとしてプログラ
ム Φ で計算可能．
⇒ 計算可能数学 RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) な
る原始再帰的関数項 (≈ プログラム)Φ が存在する．
14 / 21
定理 A. (藤原.)
φ(f ) が ∀uφqf (f , u) という形，ψ(f , g ) が ∀w ∃sψqf (f , g , w , s)
という形の論理式として形式化される存在定理
∀f (φ(f ) → ∃g ψ(f , g )) に対し，以下は同値である．
1 構成的数学 EL ⊢ ∀f (φ(f ) → ∃g ψ(f , g )).
2 計算可能数学 RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) な
る原始再帰的関数項 (≈ プログラム)Φ が存在する．
15 / 21
定理 A. (藤原.)
φ(f ) が ∀uφqf (f , u) という形，ψ(f , g ) が ∀w ∃sψqf (f , g , w , s)
という形の論理式として形式化される存在定理
∀f (φ(f ) → ∃g ψ(f , g )) に対し，以下は同値である．
1 構成的数学 EL ⊢ ∀f (φ(f ) → ∃g ψ(f , g )).
2 計算可能数学 RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) な
る原始再帰的関数項 (≈ プログラム)Φ が存在する．
適用例.
可算無限グラフに対する実効的結婚定理 EMT は 2 の意味で
構成的証明可能であり，上記の形の論理式として形式化さ
れる．よって EMT は 1 の意味で構成的証明可能である．
15 / 21
定理 B. (藤原)
φ(f ) が ∀u∃v φqf (f , u, v ) という形，ψ(f , g ) が
∀w ∃sψqf (f , g , w , s) という形の論理式として形式化される存
在定理 ∀f (φ(f ) → ∃g ψ(f , g )) に対し，以下は同値である．
1 EL + MP ⊢ ∀f (φ(f ) → ∃g ψ(f , g )).
2 計算可能数学 RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) な
る原始再帰的関数項 (≈ プログラム)Φ が存在する．
16 / 21
(1 → 2) の証明 [1]
(形式化された)Realizability 翻訳 (クリーネ, 1960’s):
φ(f ) が ∀uφqf (f , u) という形，ψ(f , g ) が ∀w ∃sψqf (f , g , w , s)
という形の時，
EL ⊢ ∀f (φ(f ) → ∃g ψ(f , g ))
⇒ EL ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) なる原始再帰的関数
項 (≈ プログラム)Φ が存在する．
⇒ RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) なる原始再帰的関
数項 (≈ プログラム)Φ が存在する．
[1] F. G. Dorais, Classical consequences of continuous choice principles from intuitionistic
analysis, Notre Dame Journal of Formal Logic 55, pp. 25-39, 2014.
17 / 21
(2 → 1) の証明
Negative translation と呼ばれる証明論の手法を用いて以下が
示せる．
補題. (Conservation Result)
φ(f ) が ∀u∃v φqf (f , u, v ) という形のとき,
RCA ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s))
⇒ EL + MP ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s)) .
18 / 21
(2 → 1) の証明
Negative translation と呼ばれる証明論の手法を用いて以下が
示せる．
補題. (Conservation Result)
φ(f ) が ∀u∃v φqf (f , u, v ) という形のとき,
RCA ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s))
⇒ EL + MP ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s)) .
⇒ EL + MP ⊢ ∀f (φ(f ) → ∃g ∀w ∃sψqf (f , g , w , s)).
18 / 21
(2 → 1) の証明
Negative translation と呼ばれる証明論の手法を用いて以下が
示せる．
補題. (Conservation Result)
φ(f ) が ∀u∃v φqf (f , u, v ) という形のとき,
RCA ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s))
⇒ EL + MP ⊢ ∀f (φ(f ) → t | f ↓ ∧ ∀w ∃sψqf (f , t | f , w , s)) .
⇒ EL + MP ⊢ ∀f (φ(f ) → ∃g ∀w ∃sψqf (f , g , w , s)).
さらに，φ(f ) が ∀uφqf (f , u) という形ならば，ダイアレク
ティカ解釈と呼ばれる証明論の手法を用いて MP を取り除
くことができる，つまり，
⇒ EL ⊢ ∀f (φ(f ) → ∃g ∀w ∃sψqf (f , g , w , s)).
定理 A．
18 / 21
定理 B. (藤原)
φ(f ) が ∀u∃v φqf (f , u, v ) という形，ψ(f , g ) が
∀w ∃sψqf (f , g , w , s) という形の論理式として形式化される存
在定理 ∀f (φ(f ) → ∃g ψ(f , g )) に対し，以下は同値である．
1 EL + MP ⊢ ∀f (φ(f ) → ∃g ψ(f , g )).
2 計算可能数学 RCA ⊢ ∀f (φ(f ) → Φ|f ↓ ∧ψ(f , Φ|f )) な
る原始再帰的関数項 (≈ プログラム)Φ が存在する．
注意. (横山&藤原, 2013)
φ(f ) が ∃u∀v φqf (f , u, v ) という形，ψ(f , g ) が
∀w ∃sψqf (f , g , w , s) という形のある論理式
∀f (φ(f ) → ∃g ψ(f , g )) に対し，(1 → 2) は成り立たない！
19 / 21
考察
(逆数学研究における形式化を踏まえると...)
多くの存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) に対して，以下
の 2 つの構成的証明可能性は同値である．
1
2
f から g を構成するプログラムがあり，かつその正当性
を証明するプログラムがある (≈ 構成的数学において証
明可能)．
f から g を構成するプログラムがあり，その正当性が計
算可能数学 (≈ RCA) で証明できる．
20 / 21
考察
(逆数学研究における形式化を踏まえると...)
多くの存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) に対して，以下
の 2 つの構成的証明可能性は同値である．
1
2
f から g を構成するプログラムがあり，かつその正当性
を証明するプログラムがある (≈ 構成的数学において証
明可能)．
f から g を構成するプログラムがあり，その正当性が計
算可能数学 (≈ RCA) で証明できる．
課題.
2 において RCA を (ACA 程度まで) 強めた構成的証明可能性
の EL + α による特徴付け．
20 / 21
考察
(逆数学研究における形式化を踏まえると...)
多くの存在定理 ∀f (φ(f ) → ∃g ψ(f , g )) に対して，以下
の 2 つの構成的証明可能性は構成的に同値である．
1
2
f から g を構成するプログラムがあり，かつその正当性
を証明するプログラムがある (≈ 構成的数学において証
明可能)．
f から g を構成するプログラムがあり，その正当性が計
算可能数学 (≈ RCA) で証明できる．
課題.
2 において RCA を (ACA 程度まで) 強めた構成的証明可能性
の EL + α による特徴付け．
これらの結果の証明は全て (メタに) 構成的である，つ
まり，これらの結果は構成的数学において成り立つ．
20 / 21
PA 及び HA における対応する結果
命題.
φ(x) が ∀uφqf (x, u) という形，ψ(x, y ) が ∀w ∃sψqf (x, y , w , s)
という形の PA の論理式として形式化される存在定理
∀x (φ(x) → ∃y ψ(x, y )) に対し，以下は同値である．
1 PA ⊢ ∀x(φ(x) → ψ(x, f (x)) なる原始再帰的関数 f が存
在する．
2 HA ⊢ ∀x(φ(x) → ∃y ψ(x, y )).
21 / 21
PA 及び HA における対応する結果
命題.
φ(x) が ∀uφqf (x, u) という形，ψ(x, y ) が ∀w ∃sψqf (x, y , w , s)
という形の PA の論理式として形式化される存在定理
∀x (φ(x) → ∃y ψ(x, y )) に対し，以下は同値である．
1 PA ⊢ ∀x(φ(x) → ψ(x, f (x)) なる原始再帰的関数 f が存
在する．
2 HA ⊢ ∀x(φ(x) → ∃y ψ(x, y )).
課題．
同様の証明論的手法を用いて，限定算術に対する同様の主
張が示せないか？
21 / 21

Download Report