循環証明体系におけるカット除去の反例について (証明と計算の理論と応用)

Autor: Masuoka, Yukihiro
Jazyk: japonština
Rok vydání: 2022
Předmět:
Zdroj: 数理解析研究所講究録. 2228:47-58
ISSN: 1880-2818
Popis: 循環証明体系とはその証明図がサイクル付きの木の形になっている証明体系である．J. Brotherstonは帰納的定義付き一階述語論理に対する循環証明体系CLKIDWを提案した[4]．彼はCLKIDWにおけるカット除去性が成り立たないと予想した[2]．その予想が正しいことを示した[11]の内容を紹介する．証明は反例を与えることによって行われる．つまり，CLKIかでカットありでは証明可能であるが，カットなしでは証明できないシークエントを具体的に与える．反例となるシークエントには2種類の帰納的述語が出現する．これらの帰納的述語は盾感的にはどちらも自然数の加法を定義していると解釈される．反例となるシークエントがカットありで証明可能なことは具体的な証明図を与えることで示す．反例となるシークエントがカットなしで証明できないことは，そのシークエントのカットなし証明図の存在を仮定し，CLKIDWの証明図の有限性に矛盾させることで示す．
Databáze: OpenAIRE
Externí odkaz: