Revisiting ordinal notation systems in proof theory: from the viewpoint of linear logic

点击翻译按钮获取中文摘要

19世紀末に創始された数理論理学は、完成した集まりとして無限を扱う実在論と、際限なく続くプロセスとして無限を扱う反実在論という二つの立場に厳密な数学的定式化を与えた。特に、数理論理学の一分野である証明論は、順序数表記系と呼ばれる数体系を導入し、公理系の中の形式的証明を順序数に対応付けることで、その公理系がどの程度の反実在論を表現しているのかについての尺度を与えた。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの枠組みの中で捉える観点をもたらした。本研究の目的は、線形論理がもつゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的反実在論を反省し分析することである。本年度は、順序数とゲームを共存させることのできる枠組みとして型理論に着目し、それについて研究することで次年度以降の研究の準備を行なった。まず、項書換え系と呼ばれる計算規則を単純型付きラムダ計算に加えたときに計算の停止性が保存される条件について研究した。このことを通して、プログラミング言語の一種でもある型理論の計算的側面を探究した。次に、マーティン・レーフ型理論の中で、ユニバース型と呼ばれるデータ型の構成を際限なく繰り返すことのできる演算子を定式化した。ユニバース型からは順序数と類似した構造をもつデータを構成できるため、この演算子の定義を通して、型理論の中で順序数を際限なく構成するアプローチを模索した。