ファイル置き場 Sendai Logic Homepage UGent2012 3

❖♥ ❛ ●❛♣ ❜❡t✇❡❡♥ ❚r✉t❤ ❛♥❞ Pr♦✈❛❜✐❧✐t②✿ ❙♦♠❡ ♦❢ ❚♦t❛❧

❋✉♥❝t✐♦♥s ❆r❡ ◆♦t ❵Pr♦✈❛❜❧②✬ ❚♦t❛❧✳

❙❡♠✐♥❛r ▲♦❣✐❝ ❛♥❞ ❆♥❛❧②s✐s

✳ ❋r✐❞❛② ✷✺ ▼❛②✱ ✷✵✶✷

◆❛♦❤✐ ❊❣✉❝❤✐

▼❛t❤❡♠❛t✐❝❛❧ ■♥st✐t✉t❡✱ ❚♦❤♦❦✉ ❯♥✐✈❡rs✐t②✱ ❏❛♣❛♥

❡❣✉❝❤✐❅♠❛t❤✳t♦❤♦❦✉✳❛❝✳❥♣

✶ ■♥tr♦❞✉❝t✐♦♥

❼ ❇② ●ö❞❡❧✬s s❡❝♦♥❞ ✐♥❝♦♠♣❧❡t❡♥❡ss t❤❡♦r❡♠✱ ❢♦r ❛♥② ❝♦♥s✐st❡♥t ❛①✐♦♠❛t✐❝ s②st❡♠ T

♦❢ ▼❛t❤❡♠❛t✐❝s✱ t❤❡r❡ ❡①✐sts ❛ st❛t❡♠❡♥t A ❡①♣r❡ss❡❞ ❜② t❤❡ ❧❛♥❣✉❛❣❡ ♦❢ T s✉❝❤ t❤❛t

A^N _{✐s tr✉❡✱}

✇❤❡r❡ A^N ❞❡♥♦t❡s t❤❡ r❡s✉❧t ♦❢ ✐♥t❡r♣r❡t✐♥❣ A ♦✈❡r t❤❡ ♥❛t✉r❛❧ ♥✉♠❜❡rs N✱

❜✉t A ✐s ♥♦t ❛ t❤❡♦r❡♠ ♦❢ T ✳

❼ ❍❡♥❝❡✱ ❢♦r ❛♥② ❝♦♥s✐st❡♥t ❛①✐♦♠❛t✐❝ s②st❡♠ T ♦❢ ▼❛t❤❡♠❛t✐❝s✱ t❤❡r❡ ❡①✐sts ❛ st❛t❡✲

♠❡♥t A❼x, y➁ ❡①♣r❡ss❡❞ ❜② t❤❡ ❧❛♥❣✉❛❣❡ ♦❢ T s✉❝❤ t❤❛t

➛m ❃ N✱ ➜!n ❃ N s✳t✳ A^N❼m, n➁ ✐s tr✉❡✱

❜✉t ➛x➜!yA❼x, y➁ ✐s ♥♦t ❛ t❤❡♦r❡♠ ♦❢ T ✳

❼ ◆❛♠❡❧②✱ ❢♦r ❛♥② ❝♦♥s✐st❡♥t ❛①✐♦♠❛t✐❝ s②st❡♠ T ♦❢ ▼❛t❤❡♠❛t✐❝s✱ t❤❡r❡ ❡①✐sts ❛ t♦t❛❧

❢✉♥❝t✐♦♥ f ✂ N ^Ns✉❝❤ t❤❛t

➛x➜!y“f❼x➁ y^➐➐ ✐s ♥♦t ❛ t❤❡♦r❡♠ ♦❢ T ✱

✐✳❡✳✱ t♦t❛❧✐t② ♦❢ f ✐s ♥♦t ♣r♦✈❛❜❧❡ ✐♥ T ✳

◗✉❡st✐♦♥✳ ❍♦✇ ❝❛♥ ✇❡ ✜♥❞ t❤❡ ❜♦✉♥❞❛r② ♦❢ t♦t❛❧ ❢✉♥❝t✐♦♥s ♣r♦✈❛❜❧② t♦t❛❧ ✐♥ ❛ ❣✐✈❡♥

❝♦♥s✐st❡♥t ❛①✐♦♠❛t✐❝ s②st❡♠❄

❻❙❡♠✐♥❛r ▲♦❣✐❝ ❛♥❞ ❆♥❛❧②s✐s ✲ ●❤❡♥t ❯♥✐✈❡rs✐t②✿ ❤tt♣✿✴✴❝❛❣❡✳✉❣❡♥t✳❜❡✴③✇❝✴❧♦❣❛♥s❡♠✐♥❛r✳❡♥✳❤t♠❧

✶

✷ ●❡♥❡r❛❧ ✐❞❡❛s

▲❡t T ❜❡ ❛♥ ❛①✐♦♠❛t✐❝ s②st❡♠ ♦❢ ▼❛t❤❡♠❛t✐❝s ❛♥❞ Thm❼T ➁ ✂ ➌A ❙ A ✐s ❛ t❤❡♦r❡♠ ♦❢ T ➑✳ Pr♦❜❧❡♠✳ ■♥ ❣❡♥❡r❛❧ Thm❼T ➁ ☞ N✳ ❍❡♥❝❡ t❤❡ s✐③❡ ✭♦r t❤❡ ❝❛r❞✐♥❛❧✐t②✮ ♦❢ Thm❼T ➁ ❞♦❡s

♥♦t ❤❡❧♣ t♦ ❦♥♦✇ t❤❡ str❡♥❣t❤ ♦❢ t❤❡ ♣r♦✈✐♥❣ ♣♦✇❡r ♦❢ T ✳

❙♦❧✉t✐♦♥✭❄✮✳ ❊♠♣❧♦② ♦r❞✐♥❛❧ ♥✉♠❜❡rs t♦ ♠❡❛s✉r❡ t❤❡ ♣r♦✈✐♥❣ ♣♦✇❡r ♦❢ T ✳

■♥❢♦r♠❛❧ ✐❞❡❛✳

✶✳ ❉❡✜♥❡ ❛♥ ❡♥✉♠❡r❛t✐♦♥ α ✭ A^α ♦❢ st❛t❡♠❡♥ts ❜② ♦r❞✐♥❛❧ ♥✉♠❜❡rs✱ ❛♥❞

✷✳ ❆ss♦❝✐❛t❡ ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α^T ✇✐t❤ T s✉❝❤ t❤❛t Thm❼T ➁ ❜ ➌A^α❙ α ❅ α^T➑✳

■t ❤♦❧❞s t❤❛t α^T ❅ ω¹ ➥¹ ✭t❤❡ ❧❡❛st ✉♥❝♦✉♥t❛❜❧❡ ♦r❞✐♥❛❧✮ s✐♥❝❡ Thm❼T ➁ ✐s ❝♦✉♥t❛❜❧❡✳

✸ ❖r❞✐♥❛❧ ♥✉♠❜❡rs

❖r❞✐♥❛❧ ♥✉♠❜❡rs ❛r❡ ❛♥ ❡①t❡♥s✐♦♥ ♦❢ ♥❛t✉r❛❧ ♥✉♠❜❡rs t♦ ✐♥✜♥✐t❡ ♥✉♠❜❡rs✿ 0, 1, 2, . . . ω, ω✔ 1, . . . ω ✔ ω, . . . ω^{2, . . . ωω, . . . ωω , . . .}

✇❤❡r❡ ω ❞❡♥♦t❡s t❤❡ ❧❡❛st ✐♥✜♥✐t❡ ♦r❞✐♥❛❧ ♥✉♠❜❡r✳

❊①❛♠♣❧❡ ✶✳ ✶✳ ω ☞ ❵0, 1, 2, . . .❡ ☞ ❵1, 2, 3, . . .❡ ☞ ❵0, 2, 4, . . .❡✳

✷✳ ω ✔ 1 ☞ ❵1, 2, 3, . . . 0❡ ❛♥❞ ω ✔ ω ☞ ❵0, 2, 4, . . . 1, 3, 5, . . .❡✳

✸✳ ω^{2 ω ω supm}_❅ω^{ω m} ❛♥❞ ω^{ω supm}_❅ω^ωm✳

✹ ❆ ❜♦✉♥❞✐♥❣ ❢✉♥❝t✐♦♥ G

❉❡✜♥✐t✐♦♥ ✷✳ ✭❙♦♠❡ ❡①❛♠♣❧❡s ♦❢✮ ✐♥❞✉❝t✐✈❡ ❞❡✜♥✐t✐♦♥s ♦❢ G^α ♦♥ α ❇ ω^ω✳ G0_❼m➁ m_{✔ 1,} Gω_{❼k✔1➁❼m➁} Gω k_{✔m✔1❼m➁,}

Gk_✔1❼m➁ Gk_{❼m➁ ✔ 1,} Gω²_❼m➁ Gω_{❼m✔1➁❼m➁,}

Gω_❼m➁ Gm_✔1❼m➁, Gω^k✔1❼m➁ ^Gωk_❼m✔1➁❼m➁, Gω_{✔k✔1❼m➁} Gω_{✔k❼m➁ ✔ 1,} Gω^ω_❼m➁ Gω^m✔1_❼m➁.

Pr♦♣♦s✐t✐♦♥ ✸✳ ▲❡t k ❇ m✳

❚❤❡♥ G^k❼m➁ ❅ G^ω❼m➁✱ G^{ω k}❼m➁ ❅ G^ω2❼m➁✱ ❛♥❞ G^ωk❼m➁ ❅ G^ωω❼m➁✳ Pr♦♦❢✳ ❇② ✐♥❞✉❝t✐♦♥ ♦♥ k✳

▲❡♠♠❛ ✹✳ ▲❡t 0 ❇ k✳

❚❤❡♥ G^k❼m➁ m ✔ k ✔ 1✱ G^{ω k}❼m➁ k❼m ✔ 1➁✱ ❛♥❞ ❼m ✔ 1➁^k❇ G^ωk❼m➁✳ Pr♦♦❢✳ ❆❣❛✐♥ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ k✳

✷

✺ ❆①✐♦♠❛t✐❝ s②st❡♠ T

❢♦r ♦r❞❡r❡❞ s❡♠✐✲r✐♥❣s

❉❡✜♥✐t✐♦♥ ✺ ✭❆①✐♦♠❛t✐❝ s②st❡♠ T^OSR✮✳

❼ ❚❤❡ ❧❛♥❣✉❛❣❡ ♦❢ T^OSR ❝♦♥s✐sts ♦❢ ✔, , 0, 1, ❅✳

❼ ❚❤❡ ❛①✐♦♠s ♦❢ T^OSR ❝♦♥s✐st ♦❢ t❤♦s❡ ❛①✐♦♠s ❢♦r ♦r❞❡r❡❞ s❡♠✐✲r✐♥❣s✳

Pr♦♣♦s✐t✐♦♥ ✻✳ ❋♦r ❛♥② f ✂ N ^N✱ ✐❢ ➛x➜!y“f❼x➁ y^➐➐ ✐s ❛ t❤❡♦r❡♠ ♦❢ T^OSR✱ t❤❡♥ t❤❡r❡

❡①✐sts ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α ❅ ω^ω s✉❝❤ t❤❛t f❼m➁ ❇ G^α❼m➁ ❢♦r ❛❧❧ m✳

▲❡♠♠❛ ✼✳ ■❢ ➛x➜yA❼x, y➁ ✐s ❛ t❤❡♦r❡♠ ♦❢ T^OSR✱ t❤❡♥ t❤❡r❡ ❡①✐sts ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α_{❅ ω}^ω s✉❝❤ t❤❛t ➛m ❃ N✱ ➜n ❇ G^α❼m➁ s✳t✳ A^N❼m, n➁ ✐s tr✉❡✳

Pr♦♦❢✳ ❇② ✐♥❞✉❝t✐♦♥ ♦✈❡r t❤❡ ❢♦r♠❛❧ ♣r♦♦❢ ♦❢ t❤❡ t❤❡♦r❡♠ ➛x➜yA❼x, y➁ ✐♥ T^OSR✭❛ss✉♠✐♥❣

♥♦r♠❛❧ ❢♦r♠s ♦❢ T^OSR✲♣r♦♦❢s✮✳

✻ ❊①t❡♥❞✐♥❣ T

❜② ❛♥ ❡①♣♦♥❡♥t✐❛❧ ❢✉♥❝t✐♦♥

❉❡✜♥✐t✐♦♥ ✽ ✭❆①✐♦♠❛t✐❝ s②st❡♠ T^EXP✮✳

❼ ❚❤❡ ❧❛♥❣✉❛❣❡ ♦❢ T^EXP ❝♦♥s✐sts ♦❢ t❤❡ ♦♥❡ ♦❢ T^OSR ❛♥❞ 2^x✳

❼ ❚❤❡ ❛①✐♦♠s ♦❢ T^EXP ❝♦♥s✐st ♦❢ t❤♦s❡ ♦❢ T^OSR ❛♥❞ ➛x➜!y❼2^{x y}➁✳

Pr♦♣♦s✐t✐♦♥ ✾✳ ❋♦r ❛♥② f ✂ N ^N✱ ✐❢ ➛x➜!y“f❼x➁ y^➐➐ ✐s ❛ t❤❡♦r❡♠ ♦❢ T^EXP✱ t❤❡♥ t❤❡r❡

❡①✐sts ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α ❅ ω^ω s✉❝❤ t❤❛t f❼m➁ ❇ G^α❼m➁ ❢♦r ❛❧❧ m✳

✼ ❆♥♦t❤❡r ❜♦✉♥❞✐♥❣ ❢✉♥❝t✐♦♥ F

❉❡✜♥✐t✐♦♥ ✶✵✳ ✭❙♦♠❡ ❡①❛♠♣❧❡s ♦❢✮ ✐♥❞✉❝t✐✈❡ ❞❡✜♥✐t✐♦♥s ♦❢ F^α ♦♥ α ❇ ω^ω✳ F0_❼m➁ m_{✔ 1,} Fω_{❼k✔1➁❼m➁} Fω k_{✔m✔1❼m➁,}

Fk_✔1❼m➁ Fk_❼Fk_❼m➁➁, Fω²_❼m➁ Fω_{❼m✔1➁❼m➁,}

Fω_❼m➁ Fm_✔1❼m➁, Fω^k✔1❼m➁ ^Fω^k_❼m✔1➁❼m➁, Fω_{✔k✔1❼m➁} Fω_✔k❼Fω_{✔k❼m➁➁,} Fω^ω_❼m➁ Fω^m✔1_❼m➁.

Pr♦♣♦s✐t✐♦♥ ✶✶✳ ▲❡t k ❇ m✳

❚❤❡♥ F^k❼m➁ ❅ F^ω❼m➁✱ F^{ω k}❼m➁ ❅ F^ω2❼m➁✱ ❛♥❞ Fω^k❼m➁ ❅ F^ωω❼m➁✳ Pr♦♦❢✳ ❇② ✐♥❞✉❝t✐♦♥ ♦♥ k✳

▲❡♠♠❛ ✶✷✳ F^k❼m➁ m ✔ 2^k✱ F^ω❼m➁ m ✔ 2^m✔1 ❛♥❞ 2

2

2^m_↔➝➝

➜➝➝➙ k 2_✬s

❅ F^{ω k}❼m➁✳ Pr♦♦❢✳ ❆❣❛✐♥ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ k✳

✸

✽ ❊①t❡♥❞✐♥❣ T

❜② t❤❡ ✐♥❞✉❝t✐♦♥ s❝❤❡♠❛

❉❡✜♥✐t✐♦♥ ✶✸ ✭❆①✐♦♠❛t✐❝ s②st❡♠ T^IND✮✳

❼ ❚❤❡ ❧❛♥❣✉❛❣❡ ♦❢ T^IND ✐s t❤❡ ♦♥❡ ♦❢ T^EXP✳

❼ ❚❤❡ ❛①✐♦♠s ♦❢ T^IND ❝♦♥s✐st ♦❢ t❤♦s❡ ♦❢ T^EXP ❛♥❞ t❤❡ ✐♥❞✉❝t✐♦♥ s❝❤❡♠❛✿ A❼0➁ & ➛x❼A❼x➁ ^A❼x ✔ 1➁➁ ➛xA❼x➁

❘❡♠❛r❦ ✶✹✳ T^IND ✐s ♠♦r❡ ❝♦♠♠♦♥❧② ❦♥♦✇♥ ❛s P❡❛♥♦ ❛r✐t❤♠❡t✐❝✱ PA✳

Pr♦♣♦s✐t✐♦♥ ✶✺ ✭●❡♥t③❡♥ ✬✸✻✱ ❈✐❝❤♦♥✲❲❛✐♥❡r ✬✽✸✱ ❇✉❝❤❤♦❧③✲❲❛✐♥❡r ✬✽✼✮✳ ❋♦r ❛♥② f ✂ N N✱ ✐❢ ➛x➜!y“f❼x➁ y^➐➐ ✐s ❛ t❤❡♦r❡♠ ♦❢ T^IND✱ t❤❡♥ t❤❡r❡ ❡①✐sts ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α_{❅ ω}^ω s✉❝❤ t❤❛t f❼m➁ ❇ F^α❼m➁ ❢♦r ❛❧❧ m✳

Pr♦♣♦s✐t✐♦♥ ✶✻✳

✶✳ ❋♦r ❛♥② ♦r❞✐♥❛❧ ♥✉♠❜❡r α ❅ ω^ω ✱ ➛x➜!y“F^α❼x➁ y^➐➐ ✐s ❛ t❤❡♦r❡♠ ♦❢ T^IND✳

✷✳ ❋♦r ❛♥② ♦r❞✐♥❛❧ ♥✉♠❜❡r α ❈ ω^ω ✱ ➛x➜!y“F^α❼x➁ y^➐➐ ✐s ♥♦t ❛ t❤❡♦r❡♠ ♦❢ T^IND✳

▲❡♠♠❛ ✶✼ ✭●❡♥t③❡♥ ✬✸✻✮✳ ❋♦r ❛♥② ♦r❞✐♥❛❧ ♥✉♠❜❡r α ❅ ω^ω ✱ t❤❡ ❢♦❧❧♦✇✐♥❣ ✐s ❛ t❤❡♦r❡♠

♦❢ T^IND✿

✏❚❤❡r❡ ✐s ♥♦ ❞❡s❝❡♥❞✐♥❣ ❝❤❛✐♥ α ❆ α¹❆ α²❆ ✆✑

✾ ❙✉♠♠❛r②

❼ ❋r♦♠ ●ö❞❡❧✬s s❡❝♦♥❞ ✐♥❝♦♠♣❧❡t❡♥❡ss t❤❡♦r❡♠✱ ❣✐✈❡♥ ❛ ❝♦♥s✐st❡♥t ❛①✐♦♠❛t✐❝ s②st❡♠

♦❢ ▼❛t❤❡♠❛t✐❝s✱ s♦♠❡ ♦❢ t♦t❛❧ ❢✉♥❝t✐♦♥s ❛r❡ ♥♦t ♣r♦✈❛❜❧② t♦t❛❧ ✐♥ t❤❡ s②st❡♠✳

❼ ❆ ❤✐❡r❛r❝❤② ❼F^α➁^α_❅ω1 ♦❢ t♦t❛❧ ❢✉♥❝t✐♦♥s ✐s ❞❡✜♥❡❞✳

❼ ❲✐t❤ ❛ ❣✐✈❡♥ ❛①✐♦♠❛t✐❝ s②st❡♠ T ✱ ❛♥ ♦r❞✐♥❛❧ ♥✉♠❜❡r α^T ❅ ω¹ ✐s ❛ss♦❝✐❛t❡❞✱ ✇❤✐❝❤

❡♥❥♦②s t❤❛t F^α ✐s t♦t❛❧ ✐♥ T ✐❢ α ❅ α^T✱ ❛♥❞ t❤❛t F^α ✐s ♥♦t t♦t❛❧ ✐♥ T ✐❢ α^T ❇ α✳

❼ ❚❤❡ ♦r❞✐♥❛❧ ♥✉♠❜❡r α^T ✐♥❞✐❝❛t❡s ❛ ❜♦✉♥❞❛r② ♦❢ t❤❡ ♣r♦✈✐♥❣ ♣♦✇❡r ♦❢ T ✳

✶✵ ❈♦♥❝❧✉❞✐♥❣ r❡♠❛r❦s

▼♦st t❤❡♦r✐❡s ♦❢ ▼❛t❤❡♠❛t✐❝s ❛r❡ ❛①✐♦♠❛t✐③❛❜❧❡ ✐♥ RCA⁰✱ WKL⁰✱ ACA⁰✱ ATR⁰♦r Π¹1✏CA⁰✳

✭❘❡❝❛❧❧ Thm❼RCA⁰➁ ø Thm❼WKL⁰➁ ø Thm❼ACA⁰➁ ø Thm❼ATR⁰➁ ø Thm❼Π¹1✏CA⁰➁✮

❼ α^RCA0 αWKL0 ω^ω _{❛♥❞ α}ACA0 αT_IND ω^ω _✳

❼ α^ATR0 ❛♥❞ αΠ¹

1✏CA⁰ ❛r❡ ❛❧s♦ ❦♥♦✇♥✳

❼ ❚❡❝❤♥✐❝❛❧❧② αΠ¹

2✏CA⁰ ❤❛s ❜❡❡♥ ❛❝❝❡♣t❡❞ t♦ ❜❡ ❛ ❧✐♠✐t t❤❛t ❝❛♥ ❜❡ ❛ss♦❝✐❛t❡❞ ✇✐t❤

❛①✐♦♠❛t✐❝ s②st❡♠s✳

❼ ❆ss♦❝✐❛t✐♥❣ s✉❝❤ ❛♥ ♦r❞✐♥❛❧ ✇✐t❤ Π¹k✏CA⁰ ❢♦r ❛♥ ❛r❜✐tr❛r② k ✐s ❛ ❜✐❣ ❝❤❛❧❧❡♥❣❡✳

✹