2023 Fiscal Year Research-status Report
循環証明体系におけるカット除去定理とカット規則の制限
| Project/Area Number |
22K11901
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
木村 大輔 東邦大学, 理学部, 准教授 (90455197)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | 循環証明体系 / 帰納的述語 / カット除去可能性 / 分離論理 |
|---|
| Outline of Annual Research Achievements |
種々の論理に関する循環証明体系の証明論的性質について研究を行ない、以下の成果を得た。
1. 言語を制限した一階述語論理の循環証明体系のカット除去可能性：既に、1引数述語記号と1引数関数記号をもつ一階述語論理の循環証明体系についてはカット除去可能性が不成立であることを示す反例が示されているが、1引数述語記号を含み、関数記号を含まない一階述語論理の循環証明体系のカット除去可能性について調査した。とくに、変数の名前替えを同一視した上での証明中のシーケントの弱い有限性（擬有限性と呼ぶ）をもつ無限証明は循環証明に変換可能であることを示した。無限証明におけるカット除去手続は既に与えられているが、この手続を改良することにより擬有限性を保存するカット除去手続が得られると予想しており、これが示されれば1引数述語、関数記号なしにおけるカット除去可能性が証明される。
2. 帰納的定義節を制限した循環証明体系のカット除去可能性：乗法的連言のみを含むような線形命題論理の循環証明体系において、命題の帰納的定義節を準線形と呼ばれる非常に単純な形に制限してもカット除去可能性が不成立であることを示す反例を与えた。この反例よりただちに、シンボリック・ヒープ分離論理の循環証明体系において、準線形な帰納的定義節に制限してもカット除去可能性が不成立であることが示される。また、同様の体系において、結論に含まれない帰納的述語を用いたカットを利用しなければ証明できない例を示した。
さらに、前年度までの成果を3件の論文の形にまとめ、学術雑誌に投稿した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初、帰納的述語を準線形と呼ばれる非常に単純な形に制限することによりカット除去可能性が成立すると予想していたが、これが成立しない反例を発見した。応用面ではネガティヴな結果であるが、理論的には興味深い結果であり、予想とは異なる形で研究が進展していると考える。
|
| Strategy for Future Research Activity |
準線形な帰納的定義は、任意の帰納的命題に対して意味論的に同値な命題を定義できるようなクラスになっており、帰納的命題の表現力は変わらない。これまでに得られた結果より、帰納的定義の表現力を弱めることなくカット除去可能性を得ることは非常に難しいと考えられるため、帰納的定義に対するより本質的な制限が必要である。今後は、このような制限として適当なものを提案し、その中でカット除去可能性を証明することを目指す。
|
| Causes of Carryover |
国際会議への論文投稿準備が予定より遅れたため、国際会議出張旅費を次年度使用とする必要が発生したため。
|
