2018 Fiscal Year Annual Research Report
Research of the structure of proofs in nonstandard models and formal theories
| Project/Area Number |
16K17653
|
|---|
| Research Institution | Kisarazu National College of Technology |
|---|
Principal Investigator |
倉橋 太志 木更津工業高等専門学校, 基礎学系, 講師 (10738446)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 数理論理学 / 数学基礎論 / 証明可能性述語 / 不完全性定理 / 形式的算術 / 証明可能性 / 算術のモデル / 様相論理 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，形式的理論の証明及び証明可能性に関する性質を構文論的・意味論的側面から分析し，理解を深めることである．
(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) によるこれまでに知られている結果が全て系として導かれることを示した．
|
