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

この記事は、命題論理のための代表的なヒルベルト流演繹体系の一覧を含む。

古典命題計算の体系 古典命題計算は標準的な命題論理である。その意図された意味論は二値的であり、その主要な性質は、それが強完全であること、言い換えれば、ある論理式がある前提の集合から意味論的に帰結するときにはいつでも、その前提の集合から統語論的にも帰結するということである。多くの異なる同値な完全公理系が定式化されてきた。それらは、用いられる基本的な結合子の選択によって異なっており、いずれの場合も、その結合子は（すなわち、合成によってすべての n 項の真理値表を表現できるという意味で）関数完全でなければならず、また、選ばれた結合子の基底の上でのちょうどよい完全な公理の選び方によっても異なる。

含意と否定 ここでの定式化では、基本的な結合子の関数完全な集合として含意と否定 を用いる。あらゆる論理体系は、少なくとも1つの非0項推論規則を必要とする。古典命題計算は典型的にはモーダスポネンスの規則を用いる。

特に断りのない限り、以下のすべての体系にはこの規則が含まれるものとする。

フレーゲの公理系Yasuyuki Imai, Kiyoshi Iséki, On axiom systems of propositional calculi, I, Proceedings of the Japan Academy. Volume 41, Number 6 (1965), 436–439.：

ヒルベルトの公理系：

ウカシェヴィッチの公理系： 第1：

第2：

第3：

新井の公理系Yoshinari Arai, On axiom systems of propositional calculi, II, Proceedings of the Japan Academy. Volume 41, Number 6 (1965), 440–442.：

ウカシェヴィッチとタルスキの公理系Part XIII: Shôtarô Tanaka. On axiom systems of propositional calculi, XIII. Proc. Japan Acad., Volume 41, Number 10 (1965), 904–907.：

メレディスの公理系：

メンデルソンの公理系Elliott Mendelson, Introduction to Mathematical Logic, Van Nostrand, New York, 1979, p. 31.：

ラッセルの公理系：

ソボチンスキの公理系： 第1：

第2：

含意と偽 否定の代わりに、古典論理は関数完全な結合子の集合 を用いて定式化することもできる。

タルスキ＝ベルナイス＝の公理系：

。パースの法則

チャーチの公理系：

メレディスの公理系： 第1：[Fitelson, 2001] "New Elegant Axiomatizations of Some Sentential Logics" by Branden Fitelson（アルゴンヌによるコンピュータ解析により、これが命題計算における変数が最少の最短の単一公理であることが明らかになっている。）"Some New Results in Logical Calculi Obtained Using Automated Reasoning", Zac Ernst, Ken Harris, & Branden Fitelson, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf

第2：

否定と選言 含意の代わりに、古典論理は関数完全な結合子の集合 を用いて定式化することもできる。これらの定式化では以下の推論規則を用いる。

ラッセル＝ベルナイスの公理系：

メレディスの公理系C. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus, Journal of Computing Systems, pp. 155–164, 1954.： 第1：

第2：

第3：

双対的に、古典命題論理は連言と否定のみを用いて定義することもできる。

連言と否定 ロッサー・J・バークリーは、連言と否定 に基づき、モーダスポネンスを推論規則とする体系を作った。彼はその著書Rosser J. Barkley, "Logic for Mathematicians", New York, McGraw-Hill, 1953. の中で、自らの公理図式を提示するために含意を用いた。「」は「」の略記である。

この略記を用いない場合、公理図式は次のような形になる。

また、モーダスポネンスは次のようになる。

シェファーストローク （NAND演算子とも呼ばれる）は関数完全であるため、これを用いて命題計算全体の定式化を作ることができる。NANDによる定式化では、ジャン・ニコのモーダスポネンスと呼ばれる推論規則を用いる。

ニコの公理系：

ウカシェヴィッチの公理系： 第1：

第2：

ワイスバーグの公理系：

アルゴンヌの公理系： 第1：

第2： , p. 9, A Spectrum of Applications of Automated Reasoning, Larry Wos; arXiv:cs/0205078v1

アルゴンヌによるコンピュータ解析により、NAND命題計算を定式化するために用いることのできる、さらに60を超える単一公理系が明らかにされている。

含意命題計算 含意命題計算は、含意結合子のみを許容する古典命題計算の断片である。それは（偽と否定を表現する能力を欠くため）関数完全ではないが、統語論的には完全である。以下の含意計算はいずれも推論規則としてモーダスポネンスを用いる。

ベルナイス＝タルスキの公理系Investigations into the Sentential Calculus in Logic, Semantics, Metamathematics: Papers from 1923 to 1938 by Alfred Tarski, Corcoran, J., ed. Hackett. 1st edition edited and translated by J. H. Woodger, Oxford Uni. Press. (1956)：

ウカシェヴィッチとタルスキの公理系： 第1：

第2：

第3：

第4：

ウカシェヴィッチの公理系：

直観主義論理と中間論理

直観主義論理は古典論理の部分体系である。これは通常、（関数完全な）基本結合子の集合として を用いて定式化される。これは、論理を矛盾させることなく付け加えることのできる排中律 A∨¬A あるいはパースの法則 ((A→B)→A)→A を欠くため、統語論的に完全ではない。これは推論規則としてモーダスポネンスを持ち、以下の公理を持つ。

別法として、直観主義論理は、基本結合子の集合として を用いて公理化することもでき、その場合は最後の公理を次のもので置き換える。

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

ヤンコフ論理（KC）は直観主義論理の拡張であり、直観主義の公理系に次の公理を加えることで公理化できるA. Chagrov, M. Zakharyaschev, Modal logic, Oxford University Press, 1997.。

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

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

ウカシェヴィッチの公理系：

メレディスの公理系： 第1：

第2：

第3： C. Meredith, A single axiom of positive logic, Journal of Computing Systems, p. 169–170, 1954. ヒルベルトの公理系： 第1：

第2：

第3：

正命題計算 正命題計算は、直観主義論理のうち、（関数完全ではない）結合子 のみを用いる断片である。これは、上述の正の含意計算のための公理系のいずれかに、次の公理を合わせることで公理化できる。

任意で、結合子 と次の公理を含めることもできる。

のは、正命題計算のための公理系のいずれかを用いて、その言語に0項結合子 を追加することにより、追加の公理図式なしに公理化できる。別法として、これは言語 において、正命題計算に次の公理を追加することによっても公理化できる。

あるいは次の公理の組によっても公理化できる。

否定を伴う言語における直観主義論理は、正計算の上に次の公理の組を加えることで公理化できる。

あるいは次の公理の組によっても公理化できるL. H. Hackstaff, Systems of Formal Logic, Springer, 1966.。

言語 における古典論理は、正命題計算に次の公理を加えることで得られる。

あるいは次の公理の組によっても得られる。

フィッチ計算は、正命題計算のための公理系のいずれかを取り、次の公理を加えたものである。

第1と第3の公理は直観主義論理においても成り立つことに注意されたい。

同値計算 同値計算は、古典命題計算の部分体系であり、（関数的に不完全な）同値結合子のみを許容する。ここではこの結合子を と表す。これらの体系で用いられる推論規則は次の通りである。

伊関の公理系Kiyoshi Iséki, On axiom systems of propositional calculi, XV, Proceedings of the Japan Academy. Volume 42, Number 3 (1966), 217–220.：

伊関＝新井の公理系Yoshinari Arai, On axiom systems of propositional calculi, XVII, Proceedings of the Japan Academy. Volume 42, Number 4 (1966), 351–354.：

新井の公理系： 第1：

第2：

ウカシェヴィッチの公理系XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus, LARRY WOS, DOLPH ULRICH, BRANDEN FITELSON; arXiv:cs/0211015v1： 第1：

第2：

第3：

メレディスの公理系： 第1：

第2：

第3：

第4：

第5：

第6：

第7：

の公理系：

の公理系： 第1：

第2：

XCB公理系：

関連項目 矛盾許容論理 — ヒルベルト流の矛盾許容論理のための公理図式の一覧

出典