Bernays-Gödelの公理論的集合論とZermelo-Fraenkel の公理論的集合論の同値について

全文

(1)九州大学学術情報リポジトリ Kyushu University Institutional Repository. Bernays-Gödelの公理論的集合論とZermelo-Fraenkel の公理論的集合論の同値について 篠崎, 喜賢. https://doi.org/10.15017/1448936 出版情報:九州大学教養部数学雑誌. 7 (1), pp.13-21, 1969-09. College of General Education, Kyushu University バージョン: 権利関係:.

(2) Math.. Rep.. VII-1,. 1969.. の公理論 的集合論 と Zermelo-Fraenkel. Bernays-Godel. の公理論 的集合論 の同値 について 篠. 崎. 喜. 賢. 【1969.5.1.】. §1.. Calculus. §2,第1階. §3.. HLC. の 公 理 系 の predicative. Bernays-Godel. § 1.. Calculus. HLC:. Second. の集合 論の同値. HLC. order. の. ramified theory に対 す る formal system. A metamathematical. 竹 内外 吏:. 1.記. extension.. の 集合論と Zermelo-Fraenkel. theorem on functions.. の1つ.. 日本 数 学 会 欧 文 誌,第8巻.. 号. 自 由 対 象 変 数,束. 縛 対 象 変 数,対. 象 記 号,関. 数 記 号,述. 語 記 号 のほ か に. 自 由 述 語 変 数:A,B,C,… 束 縛 述 語 変 数:X,y,Z,… を 用 い る. 論 理 記 号 と し て は 通 常 用 い る, 7,〈,〉,ト,V,S!' の ほ か に λ を 用 い る. な お,a1‑16は(aトb)〈(bL‑a)の. 2.. term. 略 記 号 と し て 用 い る.. は 通 常 の 通 り と す る.. ま た,a(a)が. first order. の. formula で あ る と き. Axa(x) とい う表 現 を許 し,任 意 の. term. t に対. し. (Axa(x)) (t) を formula. と考 え る.こ こでaは. 自 由対 象 変 数 でxはa(a)に. 含 まれ な い束 縛 対.

(3) 象 変 数 とす る. ま た,任. formula. 意の. {(A)に. 対 し,Aが. 自 由 述 語 変 数,Xが. い束 縛 述 語 変 数 で あ る とき,. VX(X),. ,7X(X). も formula で あ る と し,そ 3.証. 3.1.. 明. の ほ か は 普 通 の と お り とす る.. 図. Grundsequenz. :. b ----> b. 3.2.推. 論規則. 3.21.式. の構 造 につ いて の 推 論 図. 増:左. r—>o b, T- ©. 右. 11--*0 r-->o, n. 減:左. h, h, r-->0 b, r--->e. 右. r,o, r-o,. 換:左. l', h, C, 4---> I", c, h, 4—j. 右. 三段論法 3・22.論. 理 記 号(LKに. 7:左. r. 対 す る)に. (1). (2). 4-->©,h,c,r 4--49,c,h,r. b h, 4---i1l ( , 4--i0, 11 つ い て の推 論 図. I',0, a 7a, r,e. 〈:左. 〉 ご左. r,0,. cut). b b b. 右. a, ii,e aAb, T-->e. 右. a, r,e r,e, 7a. r---,o, a 4—ill , t F, 4-->©, 11, nAb. 1, r--->e aAb, r-,©. a, r—d aVh,. h, r-,A r.--4. 右. (1). 1"--z1, a F-4, aVb. (2) r-. ト:左. 1'--,0, a h, 4-11 a l—b, T, 4-49, 11. 右. r--,e, b 4, aVb a, T---)0, b r--, 9, a H— b. 智(A)に. 含 まれ な.

(4) 右. (t), T--›0 VxA(x), r-f0. γ:左. v-*e, 5(a) F-> 9, yx5(x) (aは. (aは. 下 式 に 入 っ て な い も の と す る.). 右. (a), r.-- 4 axi(x), r,4. π:左. 3.23.. の公理 論的集合論の同値. の公理論的集合論 と Zermelo-Fraenkel. Bernays-Godel. r-›4, (t) r--* 4, ax (x). 下 式 に 入 っ て い な い も の とす る.). に対 して追 加 され る論 理 記 号 につ い ての 推 論 図.. λ:左. a(t), P--*0 (Axn(x)) (t), T--@. 右. r---0, a(t) r-49, (Axa(x)) (t). 〆:左. ,(t), P—>0 VX(X),P-->0. 右. r-->o, (A) r-..,O,yXa(X). (Aは. 下 式 に 入 っ て い な い も の とす る.). ii;(A), r,e gxB(x), r->0. a:左. 右. r,e,i(t) r,e, gXA(X). (浸 は 下 式 に 入 っ て い な い も の とす る.). (注. 意) に お い て,V,ト,aに. HLC. aVb,. 関す る. inference rule. al—b, 3xi (x), aX. (X). 7(7b/\a),. (x),. は,. を各 々. 7(7aA7b),. 7Vx7. 7VX7,(X). と定 義 す れ ば本 質 的 に は必 要 な い.. 3,. で も cut-elimination. HLC. に お い て provable. す な わ ち, HLC vable. で あ る.こ. theorem. の 定 理 は,. formula. に お け る cut-elimination. LK Grad LK. の 定 義:1つ. の. と し て のV,aお. formula. 爪. co•m+n. Grad. は,. theorem. formula. が 成 立 す る.. な式 は,三 段 論 法 を 用 い な い で も HLC の. Grad. pro-. を 次 の よ うに定 義 す る こ とに よ って. の証 明 と同 様 に 証 明 す る こ とが 出来 る.. に 表 われ る HLC. よ び 論 理 記 号7,〈,〉,ト,λ. と し て の γ,aの. 個 数 をm,又. の 個 数 をnと し て,そ. の.

(5) と 定 め る.. §2.第1階. A:与. の 公 理 系 の predicative. え られ た first. 今,{(tl,t2,…,tn)の. の公 理 系. order. closed formula の集 合). の. (first order. extension.. こ と を,. Yx1YxL...Yxn,, \X1, x2,..., xn) の specialization. とい う こ とに す れ ば,Aと. vx. (X), yY((Y),.... の集合がAの 1). formula. predicative. とは 次 の1),2)が. extension. vXi (X) が closed formula. 成 立 す る と き で あ る とす る.・. で あ る こ と,. 任意 の Axa(x) に対 して (Axa(x)), がAの (注. ((Axa(x)),••• で あ る こ と.. 公 理 の specialization. 意). 上 述 の こ とは 簡単 の た め に. one. argument. の場 合 に 限 った が,. VXV YA(X, Y) 等 で も よい. 基本定理 first order が HLC. A. culus. (証. の 公理系Aの. predicative. に お い て consistent. (例 えば LK). で. consistent. extension. で あ るた め に は A. を 今Aと. 書 くこ とに す れ ば,. が first order の predicate. cal-. で あ る こ と で あ る.. 明). .AをAと. formula, yX(X),. yY( (y),.... の 集 合 とす る.. Aカ. Vx- (x), が HLC-provable て,. と は,Aの. HLC-inconsistent. 中 の有 限個 の公 理 の列. 「 を と っ た と き,. r-~ と い うこ とで あ る が,し. か らば,ξ,η. … を 自由 対 象 変数 の 列 とし.

(6) V$12)(Ax1a1Y(x1,s1)),$2. (AX2a2('x2,2)),...,. V10(AY1h1(Yl, ?1)),•••, F-~ が LK-proveble A フ. と な っ て し ま う こ と を 示 せ ば 十 分 だ ろ う.. に お い てPを,. HLC. VX (X), F--› の cut,. 3-,. 〉,ト. mula yX(X). の. tnjerenee. に 注 目(1■. を 含 まな い 証 明 図 とす る.証 明図jpに の 列)す れ ば,Pの. の formula. は first-order. お いて for中に次の. 型 の 推論 図 が存 在 す る こ とが分 るだ ろ う.. (Axa(x)), r,,o, vX (X), F1-461 こ の推 論 図 に お げ る chief formula. y,X (X) を ve2 (Axa(x,. き 変 え てや る こ とに よ って 得 られ る新 らた な図 形P'は. )) の 型 の. formula. でお. そ の終 式 が,. v$i"CU (Axlai(xi, $,)),...r-. の 型 とな り,P'がLKに. お げ る1つ. の 証 明 図 と な っ て い る よ うに す る こ とが 出 来 る ・. よ っ て 定 理 が 成 立 す る こ と が 分 る.. (注. の集 合 論 の 同値 ・. の集 合 論 と Zermelo-Fraenkel. Bernays-Godel. §3.. 意). 以下. Bernays-Godel. の集合論 を BG,. の集合 論を. Zermelo-Fraenkel. ZF. と略 記 す. る.. ここで は. Zermelo. に 始 ま り, Fraenkel,. Van. て研 究 され て きた 公理 的 集 合 論 の うち, ZF. Neuman, と. BG. Bernays,. Godel. な どに よ っ. が 「実質 的」 に は全 く同 じで. あ るこ とを 「基 本 定 理」 に よ り証 明 す る. 今 日単 に集 合 論 とい え ば ZF た ず, predicate mann. を 指 す が, ZF. と し て 「=」,「 ∈」 の み を も つ,ま. の 公理 系 に ヒ ン トを得 て新 らた に class. の で predicate と い う predicate 1.. BG. ZF. た. は BG. constant. も function. は Bernays. が Van. も持 Neu-. (類)の 概 念 を 導 入 し これ を改 良 した も. と し て 「=」,「E.1の ほ か にM(*)(集. 合 で あ る),Cl(*)(類. で あ る). の み か らな り,前 者 お よび 後 者 の 公 理 系 は次 の よ うな も ので あ る. の 公 理 系 に つ い て..

(7) Extensionality. 公 理1.. vxvY (yz(zExi—IzEY)Hx=Y) 説 明:二 つ の 集 合 は そ の 要素 が 全体 と して一 致 す る とき等 しい.言. い換 え る と集. 合 は そ の要 素 に よ って決 定 され る とい うこ とで あ る.. 2.. Null Set JxifY(7 yEx). 3.. Unordered Pairs vxvY3zvw. (wEz I—I w=x\/w=y). 説 明:任 意 の二 つ の 集 合 に 対 して,そ. れ らだ け を要 素 に もつ 集 合 が存 在 す る こ と. を主 張 して い る.. 4.. Sum Set Vxgyyz. (zEy I—I qt (zEt/\tEx) ). 5.. Power Set. 6.. Infinity. vxYYvz (zEY I—I vu (uEzi- uEx)). gx(gExAvy(yExI– 説 明:φ. 7.. (y)Ex)). は空 集 合,{y}はyの. み を要 素 に もつ 集 合 を 示 す.. Replacement (Axiom schema) Vt1, ..., Vt11(Y'x3!YAn(x,y, t1, ..., tk) f--VugvB(u, v)) こ こ で,. B(u, v) 2!xA(x). yr (rEv I-I gs(sEuAAn (s, r, t1, ••, t.))) _ a xA(x)/\AYyz(A(v)/\A(z). Hy=z). で あ る.. 説 明:任 意 の 集合aとaの. 要 素 の上 で の 集合 論 の言 葉 に よ って 定 義 され た 関数 ノ. とが あ る とき κ がaの. 要素 を動 く とき のf(x)の. 全体 は1つ の集 合 とな. る こ とを主 張 す る.. 8.. Regularity yxgy. (weak form). (x=q V (yExAVz(zExH—7 zEy))). 説 明:集 合 は 空 で あ るか,「 ∈」 に 関 して minimal. 8'.. Regularity. (strong form). な 要 素 を 必ず 含 む こ とを示 す ・.

(8) xA(x) f-gx(A(x)Ayy7 説 明:集. (A(y)A(yEx))). 合 に つ い て そ の Rank. と い う も の を 考 え る こ と に よ っ て,. 8〈#=>8' を 証 明 す る こ と が 出 来 る.. 以 上 が ZF 2・. に 対 す る公 理 で あ るが,こ の ほ か に 「一」 に 対 す る公 理 が含 まれ る.. の 公 理 系 に つ い て(A,B,C三. BG. 2ユ.A群. の 公 理:基. 公 理1.. 本 的 な も の で あ る.. Cl(x). 説 明:集 合 は class. 2.. 群 よ り成 る.). (類)で あ る.. XEYF-M(X). 説 明:類 の要 素 とな り得 る もの は 集合 に限 る.. 3.. Extensionality yu(uEX i—JuEY) f—X= Y. 説 明:二 つ の 類 は そ の 要 素 が 一 致 す る とき に限 って 等 し くな る.. 4.. Unordered Pairs VxVYYzVW(wEzI—Iw=xVw=y). 2.2.β. 群 の 公 理:類. 5.. の 存 在 に 関 す る も の で あ る.. E Relation XVYVz(<Yz>EXI—IyEz). 6.. Intersection VXV YIZVu. 7.. (uEZ H. (uEXAuE Y) ). Complement VXg YVz(zE Y —I 7 (zEX) ). 8.. Domain VX3YVz (zEYJ—Hau(<uz>EX)). 9.. Direct Product VX7YVzVu(<uz>EY. 10.. Permutation VX,-YVzVu (<zu>EY. 11.. zEX). Permutation. <uz>EX).

(9) VX,iYVzVuw 12.. (<zuv>EY I—I<uvz>EX). Permutation VXg YVzVyuVv(<zuv>EY I—I<zvu>EX). (注. 意) {{X},{κ,y)}を. 〈xy>と. 書 く,又. くX〈yz>>を. 〈xyz>と. 書 く こ と に す る・. (説 明)上 に あ げ た β 群 の 公 理 は, <a1i...,am>A I—Ia (ai, ••., am, A1, ••, Ak) と な る よ うな 類/1の 存 在 と同 値 で あ り,こ の存 在 定 理 を 証 明 す るの に必 要 な公 理 群 で あ る. 2.3.C群. 13.. の 公 理:集. 合 の 存 在 に 関 す る も の で あ る.. Infinity gx(gEx/\yy(yExl—yU{y). 説 明: cEaVcEb. 14.. cEa U b. Ex)). と 書 く.. Sum Set VxayVz(zEy I-I gw(zEw/\wEx)). 15.. Power Set. 16.. Replacement. vxgyvz. (zEy 1-1 vu (uEzf-uEx)). VX (lug! v(<uv>EX) I—vugv の. ction. (VはXに. よ っ て 定 義 さ れ るUの. 上 の. fun-. range)). こ こで 文 章 の 部 分 は,. yt(tEv I-I Jw(wEuA<wt>EX)) の こ と で あ る.. 17.. Regularity VX(X+01—gu (uEXAvy. 以上 が.BGに. 対 す る公 理 で あ る・ さて,ZFとBGの. 理 に お け るAをZ∬ 肌CでAか. らBGの. の公 理 に と りAの. VX(X),. Predicative. 同 値 の 証 明 で あ るが 基 本 定 extension. をAと. す る とき. 公 理 をす べ て証 明 す れ ば それ で十 分 だ ろ う.今,AをA. と 二 つ の formula. の 集 ま り と し て,. (yEX I—7 yEu)) ). VX (X).

(10) (X) を. の公理. を Regularity. 6(x) に とれ ば まず,BGの ま た.8群. の公理. Replacement. と. Replacement. Regularity. は 成 立 す る.. の 公 理 は,. Ax( x1, •••, xn) (x—<x1, •", xn> / \ a(x1r.•., xn, Xi,. , Xm)). を 考 え れ ば よ い. 残 りの 公 理 に 対 し て は,. a EB :. 3x(a=x. /\ xEB). A Eb :. gx(x=A. A xEb). AC :. 3x(x=A. A xEB). a=B :. yx(xEa I-I xEB). A=b :. Vx(xEA I-I xEb). A=B :. Vx(xEA I-1 xEB). ま た,. M(A) : 21x(x=A) Cl(a) :. ,jX(a=X). とす れ ば よい. (注. 意). 選 択 公理 につ い て も,そ の形 式 さ え確 定す れ ば 同 様 に と り扱 え る. 例 え ば,. x4-0H f(x)Ex の 型 に 対 し て は,. Ay(.7x(y=<f(x),. x>)). を 考 えれ ば よい. 文 1.. K. Godel, The conristency. 2.. A. Fraenkel,. 3.竹. 内 外 吏:. Y. Bar-Hillel,. 献. of the continuum hypothesis, 1951. Foundation. A metamathematical. of Set theory, 1958.. theorem on functions. 日本数学会欧文誌,第8巻.

(11)

Updating...

参照

Updating...

関連した話題 :

Scan and read on 1LIB APP