証明可能性論理

証明可能性論理は証明論の一分野であり、様相論理の一種です。この論理では、ボックス演算子（または「必然性」演算子）は「～であることが証明可能である」と解釈されます。その目的は、ペアノ算術のような、比較的豊かな形式理論における証明述語の概念を捉えることにあります。

証明可能性論理にはいくつかの種類があり、その一部は§ 参考文献で取り上げられています。基本体系は一般にGL（ゲーデル・レーブの略）またはL、あるいはK4W（Wはwell-foundednessの略）と呼ばれます。これは、レーブの定理の様相論理版を論理K（またはK4 ）に追加することで得られます。

すなわち、GLの公理は、古典命題論理のトートロジーと、以下のいずれかの形式のすべての論理式から構成される。

• 分配法則: □( p → q ) → (□ p → □ q );
• レーブの公理：□(□ p → p ) → □ p。

推論のルールは以下のとおりです。

• 手口: p → qから、 pはqを結論付けます。
• 必要性：${\displaystyle \vdash }$p結論${\displaystyle \vdash }$□ p。

クルト・ゲーデルは1933年に証明可能性論理に関する最初の論文を書いた。^{[ 1 ]}この論文で彼は直観主義命題論理から様相論理への翻訳を紹介し、証明可能性は様相演算子として見なせることを簡単に述べた。^{[ 2 ]}

GLモデルは、 1976年にロバート・M・ソロベイによって初めて提唱されました。それ以来、1996年に亡くなるまで、この分野の主要な推進者はジョージ・ブーロスでした。セルゲイ・N・アルテモフ、レフ・ベクレミシェフ、ギオルギ・ジャパリゼ、ディック・デ・ヨング、フランコ・モンターニャ、ジョバンニ・サンビン、ウラジミール・シャヴルコフ、アルバート・ヴィッサーらも、この分野に多大な貢献をしています。

解釈可能性論理とジャパリゼの多様体論理は、証明可能性論理の自然な拡張である。

• ヒルベルト・ベルネイスの証明可能性条件
• 解釈可能性ロジック
• クリプキ意味論
• ジャパリゼの多様論理
• レーブの定理
• 信念論理

• ジョージ・ブーロス著『証明可能性の論理』ケンブリッジ大学出版局、1993年。
• Giorgi Japaridzeおよび Dick de Jongh、「証明可能性の論理」。S. Buss 編『証明理論ハンドブック』、Elsevier、1998 年、475-546 ページ 。
• Sergei N. ArtemovおよびLev Beklemishev、「証明可能性論理」。D . Gabbay および F. Guenthner 編、 『哲学的論理ハンドブック』第 13 巻、第 2 版、 189–360 頁。Springer、2005 年。
• Per Lindström、「証明可能性論理―入門」、Theoria 62 (1996)、pp.  19–61。
• クレイグ・スモリンスキー著『自己参照と様相論理』、シュプリンガー、ベルリン、1985年。
• Robert M. Solovay、「様相論理の証明可能性解釈」、Israel Journal of Mathematics、第25巻（1976年）：287-304。
• リネケ・フェルブルッヘ、「証明可能性論理」 、スタンフォード哲学百科事典より。

• 「証明可能性ロジック」の項目リネケ・フェルブルージュ著、スタンフォード哲学百科事典