巨大数研究 Wiki
登録
巨大数研究 Wiki
78行目: 78行目:
 
以下が成り立つ.
 
以下が成り立つ.
 
# <math>d_\Omega(\alpha)<\Omega</math>.
 
# <math>d_\Omega(\alpha)<\Omega</math>.
# 任意の<math>\gamma\in K_\Omega(\alpha)</math>に対し<ref>gamma<d_\Omega(\alpha)</ref>.
+
# 任意の<math>\gamma\in K_\Omega(\alpha)</math>に対し<ref>\gamma<d_\Omega(\alpha)</ref>.
# 任意の<math>\gamma\in K_\Omega(\alpha)</math>に対し<math>gamma\leq\alpha</math>.
+
# 任意の<math>\gamma\in K_\Omega(\alpha)</math>に対し<math>\gamma\leq\alpha</math>.
 
# <math>\beta<\Omega</math>かつ任意の<math>\gamma\in K_\Omega(\beta)</math>に対し<math>gamma<d_\Omega(\alpha)</math>であるとき,<math>\beta<d_\Omega(\alpha)</math>である.
 
# <math>\beta<\Omega</math>かつ任意の<math>\gamma\in K_\Omega(\beta)</math>に対し<math>gamma<d_\Omega(\alpha)</math>であるとき,<math>\beta<d_\Omega(\alpha)</math>である.
 
|}
 
|}

2020年7月12日 (日) 23:53時点における版

順序数図形 (ordinal diagram, o.d.) は竹内外史証明論で用いた順序数表記である.例えばでのの順序型はバッハマン・ハワード順序数であり,でのの順序型は竹内・フェファーマン・ブーフホルツ順序数である.

概要

ゲンツェンが無矛盾性証明の際に証明図から順序数を見出したように,竹内外史は証明図に対応させる順序数表記として順序数図形を考案した[1][2].後に順序数図形は簡略化できることを指摘され[3],後は簡略化されたものが用いられることが多い.

竹内は現代的に言えば二階算術の部分体系の無矛盾性証明[4][5],そしての無矛盾性証明を行い[6][注 1],また八杉満利子とともにの無矛盾性証明を行った[9]

他の順序数表記との関係もありシュッテの順序数表記との関係性がレヴィッツ[10]によって,現代的な順序数崩壊関数であるブーフホルツのψ関数との関係性が岡田光弘[11]によって提示されている.

最近のより大きな順序数に対する順序数図形は新井敏康[12][13][14]によって与えられ,それを用いた順序数解析が行われている[15][16][17][18][19][20]

また順序数表記の整列擬順序に対する一般化は岡田・竹内[21]で与えられ,項書き換えやブーフホルツのヒドラの停止性証明にも用いられている[22]

順序数図形

新井敏康[23]にて導入された順序数図形を新井[24]に倣い解説する.これは竹内のに対応するものであり,バッハマン・ハワード順序数までの順序数表記となる.

定義2.1

順序数図形原子図形 (atomic diagram) は記号であり,構成子 (constructor) はからなる.

図形 (diagram) の集合は以下のように帰納的に定義される.

  1. 原子図形は図形である.つまりである.
  2. 以上の自然数でかつであるときである.
  3. であるとき,である.
  4. であるとき,であり,この図形を-図形という.

図形に対し図形の集合[注 2]を帰納的に定める.

とする.

上の変数関係を以下のように定める:

  1. であるとき,でない。
  2. であるとき,である。
  3. を満たす以上の自然数が存在するとき,でない.
  4. を満たすが存在するとき,である.
  5. を満たすが存在するとき,である.

上の変数関係を以下のように再帰的に定める:

  1. であるとき,と同値である.
  2. かつであるとき,でない.
  3. でありかつを満たす以上の自然数が存在するとき,またはと同値である.
  4. を満たす以上の自然数が存在しかつであるとき,と同値である.
  5. を満たす以上の自然数が存在しかつを満たす以上の自然数が存在するとき,は以下のいずれかが成り立つことと同値である:
    1. かつ未満の任意の自然数に対しである.
    2. 未満の自然数であって以下を満たすものが存在する:
      1. 未満の任意の自然数に対しである.
      2. である.
  6. かつであるとき,でない。
  7. かつを満たすが存在するとき,と同値である。
  8. かつを満たすが存在するとき,でない。
  9. を満たすが存在しかつであるとき,は同値である.
  10. を満たすが存在しかつを満たすが存在するとき,は同値である.
  11. を満たすが存在しかつを満たすが存在するとき,は同値である.
  12. を満たすが存在しかつであるとき,でない.
  13. を満たすが存在しかつを満たすが存在するとき,は同値である.
  14. を満たすが存在しかつを満たすが存在するとき,は以下のいずれかが成り立つことと同値である:
    1. 任意のに対しかつである.
    2. を満たすが存在する.
命題2.2

以下が成り立つ.

  1. 任意のに対し[26]
  2. 任意のに対し
  3. かつ任意のに対しであるとき,である.
定義2.3

とし,に対して本質的に小さい (essentially less than) あるいは崩壊しても小さい (collapsibly less than) という.

定義2.3

以下が成り立つ.

  1. ならば
  2. ならば
  3. ならば
  4. または
  5. または
定義2.3

ラティエン・ヴァイアーマンのϑ関数とし,からへの写像を帰納的に定義する.

このとき,からへの埋め込みとなっている.

関連項目

脚注

  1. なお,このとき竹内はまでの超限帰納法を用いており,八杉[7]までは,この超限帰納法が正確に証明論的順序数と一致するかは未解決であった.実際はで十分であることが新井[8]にて指摘された.
  2. 恐らく KoeffizientのKであろう[25]

出典

  1. G. Takeuti. Ordinal diagrams. Journal of the Mathematical Society of Japan 9.4 (1957): 386-394.
  2. G. Takeuti, Ordinal diagrams II, J. Math. Soc. Japan 12(1960), 385-391.
  3. A. Kino. On ordinal diagrams" Journal of the Mathematical Society of Japan 13.4 (1961): 346-356.
  4. G. Takeuti, On the fundamental conjecture of GLC V, J. Math. Soc. Japan 10(1958), 121-134
  5. G. Takeuti, On the fundamental conjecture of GLC VI, Proc. Japan Acad. 37(1961), 440-443.
  6. G. Takeuti, Consistency proofs of subsystems of classical analysis, Annals of Mathematics (2) vol.86, 299–348 (1967).
  7. 八杉満利子. Ordinal Diagram について. 数学 26.2 (1974): 121-136.
  8. T. Arai. An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions. Tsukuba journal of mathematics 8.2 (1984): 209-218.
  9. G. Takeuti. and M. Yasugi, The ordinals of the systems of second order arithmetic with the provably -comprehension axiom and with the -comprehension axiom respectively”, Japanese Journal of Mathematics vol.41, 1-67 (1973).
  10. H. Levitz. On the Relationship Between Takeuti's Ordinal Diagrams and Schütte's System of Ordinal Notations . Studies in Logic and the Foundations of Mathematics. Vol. 60. Elsevier, 1970. 377-405.
  11. M. Okada. A simple relationship between Buchholz's new system of ordinal notations and Takeuti's system of ordinal diagrams. The Journal of symbolic logic 52.3 (1987): 577-581.
  12. T. Arai. Ordinal diagrams for recursively Mahlo universes. Archive for Mathematical Logic 39.5 (2000): 353-391.
  13. Insert reference
  14. T. Arai. Ordinal diagrams for -reflection. The Journal of Symbolic Logic 65.3 (2000): 1375-1394.
  15. T. Arai. Proof theory for theories of ordinals—I: recursively Mahlo ordinals. Annals of Pure and applied Logic 122.1-3 (2003): 1-85.
  16. T. Arai. Proof theory for theories of ordinals II: -reflection. Annals of Pure and Applied Logic 129.1-3 (2004): 39-92.
  17. T. Arai. Proof Theory for Theories of Ordinals III: -Reflection. Gentzen's Centenary. Springer, Cham, 2015. 357-424.
  18. T. Arai. Wellfoundedness Proofs by Means of Non-Monotonic Inductive Definitions I: -Operators. Journal of Symbolic Logic (2004): 830-850.
  19. T. Arai. Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators. Annals of Pure and Applied Logic 162.2 (2010): 107-143.
  20. T. Arai. A Sneak Preview of Proof Theory of Ordinals (< Special Section> Infinity in Philosophy and Mathematics). Annals of the Japan Association for Philosophy of Science 20 (2012): 29-47.
  21. M. Okada and G. Takeuti. (1987): On the theory of quasi-ordinal diagrams. In: Logic and combinatorics (Arcata, Calif., 1985), Contemp. Math. 65, Amer. Math. Soc., Providence, RI, pp. 295–308
  22. M. Okada, and Y. Takahashi. On quasi ordinal diagram systems. Electronic Proceedings in Theoretical Computer Science, EPTCS 288 (2019): 38-49.
  23. 新井敏康. 竹内の基本予想について. 数学 40.4 (1988): 322-337.
  24. T. Arai. An introduction to finitary analyses of proof figures. LONDON MATHEMATICAL SOCIETY LECTURE NOTE SERIES (1999): 1-26.
  25. W. Buchholz. A survey on ordinal notations around the Bachmann–Howard ordinal. Feferman on Foundations. Springer, Cham, 2017. 71-100.
  26. \gamma<d_\Omega(\alpha)