世界大百科事典（旧版）内のordinaldiagramの言及
【数学基礎論】より
…竹内外史は，53年にLKを拡張して高階の述語論理をゲンツェン･タイプで形式化(GLCと呼ばれる)し，GLCに対してもゲンツェンの基本定理と同様な定理が成り立つという予想(基本予想と呼ばれる)を立て，基本予想が有限的構成的しかたで証明できれば，解析学の無矛盾性は一挙に解決されることを示した。竹内は基本予想の部分的解決を重ねるとともに，その補助手段として構成的順序数の一種であるオーディナル･ダイヤグラムordinal diagramなる概念を導入，その理論の発展と整備補強に努め，広範な内容をもつ解析学の部分体系の無矛盾性を証明した。この証明は有限の立場からはなお若干の不満はあるものの，今日まで証明論で得られている最良の結果である。…
※「ordinaldiagram」について言及している用語解説の一部を掲載しています。
出典｜株式会社平凡社「世界大百科事典（旧版）」