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

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

古典的な命題計算は標準的な命題論理です。その意図された意味論は二価であり、その主な特性はそれが強く完全であることです。言い換えると、式が一連の前提から意味的に導かれる場合は常に、そのセットから構文的にも導かれます。多くの異なる同等の完全な公理系が定式化されています。それらは、使用される基本接続子の選択が異なり、すべての場合において機能的に完全でなければなりません(つまり、すべての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}$

${\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}$

メレディスの公理系:

• 第一に: ^{[5] [6] [7]}

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

• 2番目: ^[5]

  ${\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}$

メレディスの公理体系: ^[8]

• 初め：

  ${\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・バークリーは、モーダス・ポネンスを推論規則として用いた、連言と否定に基づく体系を考案した。 ^[9]彼は著書の中で、含意を用いて自身の公理体系を提示した。「」は「 」の略語である。 ${\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 定式化では、ニコドのモーダスポネンス と呼ばれる推論規則を使用します。

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

ニコドの公理系: ^[5]

${\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 の公理系: ^[5]

• 初め：

  ${\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)])]}$

ワイスバーグの公理系: ^[5]

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

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

• 初め：

${\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)]}$^[10]

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

含意命題計算は、含意接続詞のみを許容する古典的な命題計算の一部です。これは機能的には完全ではありませんが(偽と否定を表現する能力がないため)、統語的には完全です。以下の含意計算は、推論規則として modus ponens を使用します。

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

${\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 の公理系:

• まず^[11]

  ${\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番目: ^[11]

  ${\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 の公理系: ^{[12] [11]}

${\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）は直観主義論理の拡張であり、直観主義公理系に公理を加えたもの^{[13]で公理化できる。}

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

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

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

正含意計算は直観主義論理の含意部分です。以下の計算では推論規則として modus ponens を使用します。

Ł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)))}$^[14]

ヒルベルトの公理系:

• 初め：

  ${\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)}$

または公理のペア^[15]

${\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}$

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

${\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}}.}$

井関の公理体系: ^[16]

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

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

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

${\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 の公理系: ^[18]

• 初め：

  ${\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))}$

メレディスの公理体系: ^[18]

• 初め：

  ${\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)}$

カルマンの公理系: ^[18]

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

ウィンカーの公理系: ^[18]

• 初め：

  ${\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公理系: ^[18]

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

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