証明可能性論理

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

証明可能性論理 (: Provability logic) は、ボックス(または"必然性")演算子が'〜は証明可能である'と解釈されるような様相論理である。その要点は、ペアノ算術のような合理的で豊かな形式理論の証明述語の概念を捉えることである。

数々の証明可能性論理が存在し、そのいくつかは参考文献が示されている。基本的な体系は、一般的にGL (Gödel-Löb)、L または K4W として言及される。それは、Löbの定理の様相バージョンを論理 K (または K4) に加えることで得られる。それは、Robert M. Solovayによって1976年に開拓された。それから1996年までは、その分野の第一人者はGeorge Boolosであった。この分野への主要な貢献者は、Sergei Artemov、Lev Beklemishev、Giorgi JaparidzeDick de Jongh、Franco Montagna、Vladimir Shavrukov、Albert Visserらである。解釈可能性論理は証明可能性論理の自然な拡張を表現する。

関連項目[編集]

参考文献[編集]

執筆の途中です この「証明可能性論理」は、論理学に関連した書きかけ項目です。この記事を加筆・訂正して下さる協力者を求めていますPortal:論理学)。