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)に
含 まれ な い束 縛 対
象 変 数 とす る.
ま た,任
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)に
含 まれ な
右
(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と し て,そ
の
と 定 め る.
§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-~
と い うこ とで あ る が,し
か らば,ξ,η
… を 自由 対 象 変数 の 列 とし
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(*)(類
で あ る)
の み か らな り,前 者 お よび 後 者 の 公 理 系 は次 の よ うな も ので あ る
の 公 理 系 に つ い て.
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)
な 要 素 を 必ず 含 む こ とを示 す ・
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)
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)
(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巻
© Copyright 2024 ExpyDoc
