LK

…In fact, in 1936, G. Gentzen achieved the groundbreaking work of achieving consistency in arithmetic (pure number theory) by further developing the position of finiteness. In his doctoral dissertation in 1934, “Studies on Logical Inference,” Gentzen attempted to formalize natural logical calculations that would directly reflect the inferences usually performed in mathematics, and after technical refinements, introduced a completely new form of system LK (called the Gentzen-type system) of first-order predicate logic, and presented a truly beautiful law of logic: “A logical formula that can be proven in LK can be proven without using any syllogisms, that is, a proof without detours can be given” (Gentzen’s Fundamental Theorem). In the above-mentioned dissertation in 1936, “Consistency in Pure Number Theory,” he formalized pure number theory in LK and proved its consistency by transfinite induction up to the ordinal number ε _0. Here, ε ₀ is the smallest ordinal number such that ω ^ξ ＝ξ, which is the limit number of . …

*Some of the terminology that mentions "LK" is listed below.

Source | Heibonsha World Encyclopedia 2nd Edition | Information

…実際に，36年にゲンツェンG.Gentzenは有限の立場を一段と深化発展させることにより算術(純粋数論)の無矛盾性を達成するという画期的な仕事を行った。　ゲンツェンは1934年の学位論文《論理的推論の研究》において，数学で通常行われる推論をそのまま反映するような自然な論理計算の形式化を試み，それに技術的な推敲（すいこう）を行って1階の述語論理のまったく新しい形式の体系LK(ゲンツェン･タイプの体系という)を導入し，論理についてのまことに美しい法則〈LKで証明できる論理式は三段論法をまったく用いないで証明できる，すなわち，回り道のない証明を与えることができる〉(ゲンツェンの基本定理)を示したが，上述の36年の論文《純粋数論の無矛盾性》で，純粋数論をLKで形式化し，その無矛盾性を順序数ε₀までの超限帰納法によって証明したのである。ここで，ε₀とはω^ξ＝ξとなるような最小の順序数であって，の極限数である。…

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

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