Basic predictions - Kihonyosou

... When it comes to real number theory or analysis, which essentially goes beyond arithmetic, it is extremely difficult to prove their consistency because they inevitably include the concept of sets. In 1953, Tonofumi Takeuchi extended LK to formalize higher-order predicate logic as a Gentzen type (called GLC), and made a conjecture (called the fundamental conjecture) that a theorem similar to Gentzen's Fundamental Theorem also holds for GLC. He showed that if the fundamental conjecture can be proven in a finite constructive way, the consistency of analysis can be solved in one fell swoop. Takeuchi repeatedly solved the partial solution of the fundamental conjecture, and introduced the concept of ordinal diagram, a type of constructive ordinal number, as an auxiliary means, and worked to develop and strengthen the theory, proving the consistency of a partial system of analysis with a wide range of content. ...

*Some of the terms used in reference to "base forecasts" are explained below.

Source | Heibonsha World Encyclopedia 2nd Edition | Information

…　本質的に算術を超える内容をもつ実数論ないしは解析学となると，不可避的に集合概念を含むためその無矛盾性の証明は極度に困難である。竹内外史は，53年にLKを拡張して高階の述語論理をゲンツェン･タイプで形式化(GLCと呼ばれる)し，GLCに対してもゲンツェンの基本定理と同様な定理が成り立つという予想(基本予想と呼ばれる)を立て，基本予想が有限的構成的しかたで証明できれば，解析学の無矛盾性は一挙に解決されることを示した。竹内は基本予想の部分的解決を重ねるとともに，その補助手段として構成的順序数の一種であるオーディナル･ダイヤグラムordinal diagramなる概念を導入，その理論の発展と整備補強に努め，広範な内容をもつ解析学の部分体系の無矛盾性を証明した。…

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

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