2018 Fiscal Year Research-status Report
| Project/Area Number |
18K00036
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
黒川 英徳 金沢大学, GS教育系, 准教授 (30710230)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | logical constant / nested sequent / Belnap's criteria / stability / DoI / impredicativity / squeezing argument / logical consequence |
|---|
| Outline of Annual Research Achievements |
本研究では、２０１８年度、次のような３つの研究を行った。
一つ目の研究では、ネステッド・シークエント上の反映原理によって導入された論理定項が、ベルナップによって提案された、論理定項の満たすべき十全性条件（同一性、保存的拡張可能性）の観点からどのように評価されるかを検討した。我々の結論は、ネステッド・シークエント上の反映原理に基づく論理定項はベルナップの要求する条件を十分に満たすが、我々はむしろベルナップの条件の正しさを再検討してみなければならないというものである。
また本研究の一部として、アルベルト・ナイボ、マティア・ペトローロとの共同研究を行い、論理定項を特徴付ける（自然演繹上の）推論規則が満たすべきものとしてダメットが与えた「安定性（stability」という条件を、シークエント計算によって特徴付けるという研究を行なった。これはナイボ－ペトローロにより提案された、論理定項を特徴付ける概念（deducibility of identials）という概念に関する研究を更に先に進めるものであり、また自然演繹上では判明になっていなかった安定性という概念のもつ意義をシークエント計算という証明論的な枠組みを採ることによって明らかにするものである。
さらに、日本を代表する論理学者であった竹内外史の論理思想に関する研究を行なった。特に、竹内が日本語で著した論文を中心に、竹内が取り組んだ高階の述語論理の証明論が、非可術的な集合概念の分析にどのように寄与しうるかという点に関する竹内の議論を分析した。
その他、ワルター・ディーンとクライゼルの「押しつぶし論法」（squeezing argument）と呼ばれる、述語論理の完全性定理の意義に関する議論を分析する研究を行なった。特にそれに関連する準備作業として、モデル論的な観点からの論理的帰結関係の分析を歴史的・哲学的観点から分析した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の主な目的の一つは、サンビンの反映原理により証明論的な仕方で論理定項の特徴付けを行い、その意義を論じることにあるが、今年度までの研究において、その準備となる数学的な成果を得る見通しはほぼついており、また哲学的な問題についても、上述の一つ目、二つ目の研究などにおいて、確実な進捗をみている。とりわけ、安定性の概念のシークエント計算による特徴付けは、既成の議論を明晰化する潜在性をもつものであり、現在得ている成果のみに基づいて論文発表できる段階にある。また一つ目の研究は、すでにconference proceedingsという形で論文として発表されている。
竹内外史の論理思想の研究は、当初本研究の研究計画に入れてはいなかったが（とはいえ２階の論理の証明論的意味論と密接に関係している）、高階論理の論理体系に現れる高階の量化子の「論理性」についてどのように考えたらよいかということは、いわゆる「竹内の基本予想」と呼ばれる、論理学の証明論的研究と数学の基礎を結びつける予想の概念的な位置付けを考える際、重要な課題になる。そのため竹内の論理思想についての研究を本研究の中に位置づけ、本年度は竹内の日本語論文の内容分析までを行った。なお、この研究の成果はすでに一部conference proceedingsの形で投稿済みである。
クライゼルの議論は主として論理学の意味論的な扱いの基礎という文脈で扱われることが多いが、しかし意味論の基礎にある証明論的な問題意識を背景にして与えられたものである。この議論についての研究は究極的には「構成の理論」に関するワルター・ディーンとの共同研究の準備となるものであるが、それ自身としても独立の意味を持っている。現在までに、クライゼルの議論を扱う準備作業としての論理的帰結についての先行研究のサーベイ、またクライゼルのテキストの分析がほぼ終わっている。
|
| Strategy for Future Research Activity |
今後の研究、特に今年度中の研究の推進方策は以下の通りである。
まずネステッド・シークエント上の反映原理による、論理定項の特徴付けについては、これまでに定式化できている数多くの体系について、証明論における基本定理であるカット除去定理の（すでに基本的には出来ている）証明を論文の形にする。
アルベルト・ナイボ、マティア・ペトローロとの共同研究である安定性概念のシークエント計算による特徴付けという研究については、すでにこれまでに得られている成果を論文にすることが第一の課題であり、それを今年度中に完了する予定である。その後は安定性の概念と、deducibility of identicalsの関係、またこの研究において使用した、いわゆるhigher-level rulesと呼ばれる、特殊な規則が論理定項の特徴付けに関して果たす役割とは何かという問題、さらにhigher-level rulesを持つ証明体系とネステッド・シークエントがどのように関係しているのかといった問題に取り組む予定である。
竹内の論理思想については、竹内の後期の思想にさらに研究を広げる予定である。特に、ゲーデルの影響下に考えられたと思われる「infinite mind」なる概念による集合論の公理の哲学的動機づけの研究と、それまでの証明論的研究の関係に焦点を当てて竹内の議論を分析する。
クライゼルのsqueezing argumentについては、クライゼルの議論の歴史的、哲学的背景、特にクライゼルのinformal rigourというより広い方法論的な概念との関係を中心に議論する論文を本年度中に執筆予定である。
|
Research Products
(8 results)
