論理における公理系の一覧

この記事には、命題論理のサンプルヒルベルト スタイルの 演繹システムの一覧が含まれています。

古典的な命題計算システム

古典的な命題論理は標準的な命題論理である。その意図する意味論は二価性を持ち、その主な性質は強完全性である。つまり、ある式が前提の集合から意味的に導かれる場合、その前提の集合から構文的にも導かれる、ということである。多くの異なる、同等の完全な公理系が定式化されてきた。それらは、使用される基本接続詞の選択において異なり、いずれの場合も基本接続詞は機能的に完全でなければならない（つまり、すべてのn項真理値表を合成によって表現できる）。また、選択された接続詞の基底における公理の完全な選択においても異なる。

含意と否定

ここでの定式化では、含意と否定を機能的に完全な基本接続詞の集合として用いている。あらゆる論理体系には、少なくとも1つの非零項推論規則が必要である。古典的な命題計算では、典型的には、法因数分解の規則が用いられる。 ${\displaystyle \{\to ,\neg \}}$

${\displaystyle {\frac {A,A\to B}{B}}.}$

特に明記しない限り、このルールは以下のすべてのシステムに含まれているものと想定します。

フレーゲの公理系：^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle A\to \neg \neg A}$

ヒルベルトの公理系: ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (A\to B)\to ((\neg A\to B)\to B)}$

Łukasiewiczの公理系: ^[1]

• 初め：

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (\neg A\to A)\to A}$

  ${\displaystyle A\to (\neg A\to B)}$

• 2番目：

  ${\displaystyle ((A\to B)\to C)\to (\neg A\to C)}$

  ${\displaystyle ((A\to B)\to C)\to (B\to C)}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• 三番目：

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

新井の公理系：^[2]

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (\neg A\to B)\to ((B\to A)\to A)}$

Łukasiewicz とTarskiの公理系: ^[3]

${\displaystyle [(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)}$

メレディスの公理系:

${\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}$

メンデルソンの公理系：^[4]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}$

ラッセルの公理系：^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

ソボチンスキーの公理系：^[1]

• 初め：

  ${\displaystyle \neg A\to (A\to B)}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• 2番目：

  ${\displaystyle (A\to B)\to (\neg B\to (A\to C))}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to B)\to ((A\to B)\to B)}$

含意と偽り

否定の代わりに、機能的に完全な接続詞のセットを使用して古典論理を定式化することもできます。 ${\displaystyle \{\to ,\bot \}}$

Tarski- Bernays -Wajsberg の公理系:

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (B\to A)}$

${\displaystyle ((A\to B)\to A)\to A}$. ^[5]

${\displaystyle \bot \to A}$

チャーチの公理体系:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle ((A\to \bot )\to \bot )\to A}$

メレディスの公理系:

• 1番目: ^{[6] [7] [8]}

  ${\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}$

• 2番目：^[6]

  ${\displaystyle ((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))}$

否定と選言

古典論理は、含意の代わりに、機能的に完全な接続詞の集合を用いて定式化することもできます。これらの定式化では、以下の推論規則が使用されます。 ${\displaystyle \{\neg ,\lor \}}$

${\displaystyle {\frac {A,\neg A\lor B}{B}}.}$

ラッセル・バーネイズの公理系:

${\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}$

${\displaystyle \neg (A\lor B)\lor (B\lor A)}$

${\displaystyle \neg A\lor (B\lor A)}$

${\displaystyle \neg (A\lor A)\lor A}$

メレディスの公理体系：^[9]

• 初め：

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))}$

• 2番目：

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))}$

• 三番目：

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))}$

双対的に、古典的な命題論理は、連言と否定のみを使用して定義できます。

接続詞と否定

ロッサー・J・バークリーは、連言と否定に基づく体系を構築し、推論規則としてモーダス・ポネンスを用いた。 ^[10]彼は著書の中で、含意を用いて自身の公理体系を提示した。「」は「 」の略語である。 ${\displaystyle \{\wedge ,\neg \}}$ ${\displaystyle C\rightarrow D}$ ${\displaystyle \neg (C\wedge \neg D)}$

• ${\displaystyle A\rightarrow A\wedge A}$
• ${\displaystyle A\wedge B\rightarrow A}$
• ${\displaystyle \left(A\rightarrow B\right)\rightarrow \left(\neg \left(B\wedge C\right)\rightarrow \neg \left(C\wedge A\right)\right)}$

略語を使用しない場合、公理スキームは次の形式になります。

• ${\displaystyle \neg (A\wedge \neg (A\wedge A))}$
• ${\displaystyle \neg ((A\wedge B)\wedge \neg A)}$
• ${\displaystyle \neg \left(\neg \left(A\wedge \neg B\right)\wedge \neg \neg \left(\neg \left(B\wedge C\right)\wedge \neg \neg \left(C\wedge A\right)\right)\right)}$

また、modus ponensは次のようになります。

• ${\displaystyle {\frac {A,\neg \left(A\wedge \neg B\right)}{B}}}$

シェファー脳卒中

シェファーのストローク（NAND演算子とも呼ばれる）は関数的に完全であるため、命題論理の完全な定式化を作成するために使用できます。NAND定式化では、ニコドのモーダスポネンスと呼ばれる推論規則が使用されます。

${\displaystyle {\frac {A,A\mid (B\mid C)}{C}}.}$

ニコドの公理系：^[6]

${\displaystyle (A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Łukasiewicz の公理系: ^[6]

• 初め：

  ${\displaystyle (A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

• 2番目：

  ${\displaystyle (A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

ワイスバーグの公理体系：^[6]

${\displaystyle (A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]}$

アルゴンヌ公理系: ^[6]

• 初め：

${\displaystyle (A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]}$

• 2番目：

${\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}$^[11]

アルゴンヌ国立研究所によるコンピュータ解析により、NAND命題計算を定式化するために使用できる60以上の追加の単一公理系が明らかになりました。^[8]

含意命題計算

含意的命題計算は、含意接続詞のみを許容する古典的な命題計算の一部である。これは機能的には完全ではない（偽と否定を表現できないため）が、統語的には完全である。以下の含意的計算は、推論規則としてモーダス・ポネンスを用いる。

バーネイズ・タルスキ公理系: ^[12]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle ((A\to B)\to A)\to A}$

Łukasiewicz と Tarski の公理系:

• まず^[12]

  ${\displaystyle [(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G}$

• 2番目：^[12]

  ${\displaystyle [(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])}$

• 三番目：

  ${\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}$

• 4番目：

  ${\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}$

Łukasiewicz の公理系: ^{[13] [12]}

${\displaystyle ((A\to B)\to C)\to ((C\to A)\to (D\to A))}$

直観主義と中間論理

直観主義論理は古典論理のサブシステムです。一般的には、（機能的に完全な）基本接続詞の集合として定式化されます。排中律A∨¬Aやパースの法則((A→B)→A)→A)を欠いているため、統語論的には完全ではありません。これらの法則は論理の矛盾を生じさせることなく追加できます。^{[異論あり（理由：これらの原則は直観主義論理に追加できますが、そうすると事実上古典論理になってしまうため）。–議論]}直観主義論理は推論規則としてモーダス・ポネンスを持ち、以下の公理を持ちます。 ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

${\displaystyle \bot \to A}$

あるいは、直観主義論理は、基本接続詞の集合として を用いて公理化され、最後の公理を に置き換えること もできる。 ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

中間論理は、直観主義論理と古典論理の中間に位置します。以下に中間論理をいくつか挙げます。

• ヤンコフ論理（KC）は直観主義論理の拡張であり、直観主義公理系に公理^{[14]を加えたものによって公理化できる。}

${\displaystyle \neg A\lor \neg \neg A.}$

• ゲーデル・ダメット論理（LC）は、直観主義論理に次の公理を加えることで公理化できる^[14]

${\displaystyle (A\to B)\lor (B\to A).}$

正の含意計算

正含意計算は直観主義論理の含意部分である。以下の計算は、推論規則としてモーダス・ポネンスを用いる。

Łukasiewiczの公理系:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

メレディスの公理系:

• 初め：

  ${\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}$

• 2番目：

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}$

• 三番目：

  ${\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}$^[15]

ヒルベルトの公理系:

• 初め：

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• 2番目：

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• 三番目：

  ${\displaystyle A\to A}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

肯定的命題計算

正値命題計算は、（機能的に完全ではない）接続詞のみを用いた直観主義論理の一部である。これは、正値含意計算のための前述の計算のいずれかと、以下の公理との組み合わせによって公理化することができる。 ${\displaystyle \{\to ,\land ,\lor \}}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

オプションとして、接続詞と公理 も含めることができます。 ${\displaystyle \leftrightarrow }$

${\displaystyle (A\leftrightarrow B)\to (A\to B)}$

${\displaystyle (A\leftrightarrow B)\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to A)\to (A\leftrightarrow B))}$

ヨハンソンの極小論理は、正値命題計算の公理系のいずれかによって公理化でき、その言語をヌラリ接続詞 で拡張することで、追加の公理スキーマなしで公理化できる。あるいは、正値命題計算を公理で拡張することで言語で公理化することもできる。 ${\displaystyle \bot }$ ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

あるいは公理のペア

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle A\to \neg \neg A}$

否定を含む言語における直観主義論理は、次の公理のペアによって正積分学上で公理化できる。

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg A\to (A\to B)}$

あるいは公理のペア^[16]

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

言語における古典論理は、正定理に次の公理を加えることによって得られる。 ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

あるいは公理のペア

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

フィッチ計算は、正の命題計算の公理系のいずれかを採用し、公理を追加する^[16]

${\displaystyle \neg A\to (A\to B)}$

${\displaystyle A\leftrightarrow \neg \neg A}$

${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}$

${\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}$

最初の公理と 3 番目の公理は直観主義論理でも有効であることに注意してください。

同値計算

同値計算は、古典的な命題計算のサブシステムであり、ここでは と表記される（機能的に不完全な）同値接続詞のみを許容する。これらのシステムで使用される推論規則は以下のとおりである。 ${\displaystyle \equiv }$

${\displaystyle {\frac {A,A\equiv B}{B}}.}$

井関の公理体系：^[17]

${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

井関・新井公理系: ^[18]

${\displaystyle A\equiv A}$

${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

${\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}$

新井の公理系;

• 初め：

  ${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

• 2番目：

  ${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

Łukasiewicz の公理系: ^[19]

• 初め：

  ${\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}$

• 2番目：

  ${\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}$

• 三番目：

  ${\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}$

メレディスの公理体系：^[19]

• 初め：

  ${\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}$

• 2番目：

  ${\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}$

• 三番目：

  ${\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}$

• 4番目：

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}$

• 5番目：

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}$

• 6番目：

  ${\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}$

• 7番目：

  ${\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}$

カルマンの公理系：^[19]

${\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}$

ウィンカーの公理系：^[19]

• 初め：

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}$

• 2番目：

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}$

XCB公理系: ^[19]

${\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}$

参照

• 矛盾論理 §ヒルベルトスタイルの矛盾論理の公理スキーマのリストが含まれています

参考文献

1. 今井康之、井関潔、「命題計算の公理系について（I）」、日本学士院紀要、第41巻第6号（1965年）、436-439。
2. 新井良成「命題計算の公理系についてII」日本学士院紀要第41巻第6号（1965年）、440-442ページ。
3. 第13部：田中正太郎. 命題計算の公理系について, XIII. 日本学士院論文集, 第41巻, 第10号 (1965), 904–907.
4. エリオット・メンデルソン『数学論理学入門』ヴァン・ノストランド、ニューヨーク、1979年、31ページ。
5. ピアースの法則
6. [Fitelson, 2001] Branden Fitelson著「いくつかの文論理の新しいエレガントな公理化」
7. (アルゴンヌ国立研究所によるコンピュータ分析により、これが命題論理学における最小の変数を持つ最短の単一公理であることが明らかになりました。)
8. 「自動推論を用いた論理計算におけるいくつかの新しい結果」、Zac Ernst、Ken Harris、Branden Fitelson、http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf
9. C. Meredith、「2値命題計算のシステム (C, N)、(C, 0)、(A, N) の単一の公理」、Journal of Computing Systems、pp. 155–164、1954年。
10. ロッサー・J・バークレー「数学者のための論理学」ニューヨーク、マグロウヒル、1953年。[1]
11. 、p. 9、自動推論の応用範囲、ラリー・ウォス; arXiv:cs/0205078v1
12. 論理、意味論、メタ数学における文的計算の調査：1923年から1938年までの論文、アルフレッド・タルスキ著、コーコラン、J.、ハケット編。第1版、JHウッドガー編・翻訳、オックスフォード大学出版局（1956年）
13. Łukasiewicz, Jan (1948). 「命題の含意計算の最短公理」. Proceedings of the Royal Irish Academy. Section A: Mathematical and Physical Sciences . 52 : 25–33 . ISSN  0035-8975. JSTOR  20488489.
14. A. チャグロフ、M. ザハリヤシェフ、様相論理、オックスフォード大学出版局、1997 年。
15. C. Meredith、「正値論理の単一公理」、Journal of Computing Systems、p. 169–170、1954年。
16. LH Hackstaff, Systems of Formal Logic、Springer、1966年。
17. 井関潔「命題計算の公理系について」第15章、日本学士院紀要、第42巻第3号（1966年）、217-220。
18. 新井良成「命題計算の公理系について」XVII、日本学士院紀要、第42巻第4号（1966年）、351-354。
19. XCB、古典等価計算のための最後の最短単一公理、ラリー・ウォス、ドルフ・ウルリッヒ、ブランドン・フィテルソン; arXiv:cs/0211015v1

Retrieved from "https://en.wikipedia.org/w/index.php?title=List_of_axiomatic_systems_in_logic&oldid=1286810246"