Limit number - limit number

In his 1934 dissertation, Studies in Logical Inference, Gentzen attempted to formalize a natural logical calculation that would directly reflect the inferences normally made in mathematics, and after some technical refinement, introduced a completely new form of first-order predicate logic, LK (known as a Gentzen-type system), and presented a truly beautiful law of logic: any formula that can be proved in LK can be proved without using any syllogisms, i.e., a proof can be given without any roundabout means (Gentzen's Fundamental Theorem). In his 1936 dissertation, Consistency in Pure Number Theory, he formalized pure number theory in LK and proved its consistency by transfinite induction up to the ordinal ε _0. Here, ε ₀ is the smallest ordinal such that ω ^ξ ＝ξ, which is the limit number of . A given proof (a formal proof in a Gentzen-type system) is marked with an ordinal less than ε ₀ to indicate its complexity, in such a way that the reduction to successively simpler proofs ensures that the sequence of ordinals given to the sequence of proofs presented at hand is successively smaller, and such a reduction process can be completed in a finite number of tries.

*Some of the terminology explanations that mention "limit numbers" are listed below.

Source | Heibonsha World Encyclopedia 2nd Edition | Information

…　ゲンツェンは1934年の学位論文《論理的推論の研究》において，数学で通常行われる推論をそのまま反映するような自然な論理計算の形式化を試み，それに技術的な推敲（すいこう）を行って1階の述語論理のまったく新しい形式の体系LK(ゲンツェン･タイプの体系という)を導入し，論理についてのまことに美しい法則〈LKで証明できる論理式は三段論法をまったく用いないで証明できる，すなわち，回り道のない証明を与えることができる〉(ゲンツェンの基本定理)を示したが，上述の36年の論文《純粋数論の無矛盾性》で，純粋数論をLKで形式化し，その無矛盾性を順序数ε₀までの超限帰納法によって証明したのである。ここで，ε₀とはω^ξ＝ξとなるような最小の順序数であって，の極限数である。与えられた証明図(ゲンツェン･タイプの体系での形式的な証明)にその複雑さを表す印としてε₀より小さな順序数を具体的につけ，そのしかたは次々とより簡明な証明図へと還元される過程において目前に示される証明図の列に付される順序数の列が逐次確実に小さくなっていくように与えられ，したがってそのような還元過程は有限回で完了する。…

※「極限数」について言及している用語解説の一部を掲載しています。

出典｜株式会社平凡社世界大百科事典 第２版について | 情報