このアイテムのアクセス数: 211
このアイテムのファイル:
| ファイル | 記述 | サイズ | フォーマット | |
|---|---|---|---|---|
| 2228-05.pdf | 4.22 MB | Adobe PDF | 見る/開く |
| タイトル: | 循環証明体系におけるカット除去の反例について (証明と計算の理論と応用) |
| 著者: | 益岡, 幸弘  |
| 著者名の別形: | Masuoka, Yukihiro |
| キーワード: | 循環証明体系 カット除去 帰納的定義 帰納法 証明論 cyclic/circular proof system cut-elimination inductive definition induction proof theory |
| 発行日: | Aug-2022 |
| 出版者: | 京都大学数理解析研究所 |
| 誌名: | 数理解析研究所講究録 |
| 巻: | 2228 |
| 開始ページ: | 47 |
| 終了ページ: | 58 |
| 抄録: | 循環証明体系とはその証明図がサイクル付きの木の形になっている証明体系である．J. Brotherstonは帰納的定義付き一階述語論理に対する循環証明体系CLKIDWを提案した[4]．彼はCLKIDWにおけるカット除去性が成り立たないと予想した[2]．その予想が正しいことを示した[11]の内容を紹介する．証明は反例を与えることによって行われる．つまり，CLKIかでカットありでは証明可能であるが，カットなしでは証明できないシークエントを具体的に与える．反例となるシークエントには2種類の帰納的述語が出現する．これらの帰納的述語は盾感的にはどちらも自然数の加法を定義していると解釈される．反例となるシークエントがカットありで証明可能なことは具体的な証明図を与えることで示す．反例となるシークエントがカットなしで証明できないことは，そのシークエントのカットなし証明図の存在を仮定し，CLKIDWの証明図の有限性に矛盾させることで示す． |
| URI: | http://hdl.handle.net/2433/279725 |
| 出現コレクション: | 2228 証明と計算の理論と応用 |
このリポジトリに保管されているアイテムはすべて著作権により保護されています。