| 研究実績の概要 |
本研究の目的は，形式的理論の証明及び証明可能性に関する性質を構文論的・意味論的側面から分析し，理解を深めることである．
(1) さまざまな derivability conditions を満たす Rosser 証明可能性述語の構成を行うことでArai(1990)による結果を拡張した．今回は異なる３種類の構成を与えたが，特に 2, 3番目の構成は Hilbert-Bernays の条件を満たすものであり，Hilbert-Bernays の条件と Loeb の条件との違い，またこれらの条件と第二不完全性定理との関係，などを明確にすることができた．
(2) Provability predicate が local な D1 と uniform な B_2 を満たせば uniform provable Σ_1-completeness が満たされる，という結果を証明した．これは Buchholz(1993) による，provability predicate が uniform な D1 と D2 を満たせば uniform provable Σ_1-completeness が満たされる，という結果の拡張となっている．更に，local な D1 と uniform な B_2 を満たすが D2 を満たさない Σ_1 provability predicate の存在を示すことで，今回の結果が Buchholz の結果の真の拡張となっていることも示した．
(3) 様相命題論理が uniform Lyndon interpolation property (ULIP) をもつ，という概念を導入し，様々な様相論理が ULIP をもつことを証明した．特に証明可能性の様相命題論理 GL 及び Grz に対する今回の結果から，Smorynski(1978), Boolos(1979), Boolos(1980), Shavrukov(1993), Visser(1996), Shamkanov(2011), Maksimova(2014) によるこれまでに知られている結果が全て系として導かれることを示した．
|
