命題計算

命題計算 [ ^a]は論理学の一分野である。^[1] これは（一階）命題論理^[2] 、文論理^[1] 、文計算^[3] 、文論理^[1]、あるいはゼロ階論理[ ^4]とも呼ばれる。^[5]これは命題^[1]（真または偽）^[6]と命題間の関係^[7]を扱い、それらに基づく議論の構築も含む。^{[8]複合命題は、}連言、選言、含意、二条件、否定の真理値関数を表す論理接続詞で命題を接続することで形成される。^{[9] [10] [11] [12]}いくつかの情報源には、次の表のように他の接続詞が含まれている。

一階論理とは異なり、命題論理は非論理的オブジェクト、それらに関する述語、または量指定子を扱いません。ただし、命題論理のすべての仕組みは、一階論理と高階論理に含まれています。この意味で、命題論理は一階論理と高階論理の基礎です。

命題論理は、通常、命題が命題変数と呼ばれる文字で表される形式言語を用いて研究される。これらは、接続詞の記号とともに、複合命題を作るのに使われる。このため、命題変数は形式ゼロ階言語の原子式^{と呼ばれる。 [10] [2]原子命題は通常、}アルファベットの文字で表されるが、^[10]論理接続詞を表す表記法は多様である。次の表は、命題論理における各接続詞の主な表記法のバリエーションを示している。

命題論理の中で最も徹底的に研究されている分野は古典的な真理関数命題論理であり、^[1]この論理式は、2つの可能な真理値、つまり真の真理値または偽の真理値のうちの1つだけを持つと解釈される。^[15]二値原理と排中律が支持されている。一階述語論理と比較すると、真理関数命題論理はゼロ階論理であると考えられる。^{[4] [5]}

命題論理（命題計算とも呼ばれる）は、以前の哲学者によって示唆されていましたが、紀元前3世紀にクリュシッポスによって形式論理（ストア論理）に発展し^[16]、その後継者であるストア派によって拡張されました。この論理は命題に焦点を当てていました。これは、項に焦点を当てた伝統的な三段論法論理とは異なっていました。しかし、元の文献のほとんどは失われ^[17]、西暦3世紀から6世紀の間にストア論理は忘れ去られ、命題論理の（再）発見をきっかけに20世紀になってようやく復活しました。^[18]

命題論理を洗練させる上で重要となる記号論理は、17/18世紀の数学者ゴットフリート・ライプニッツによって初めて開発されたが、彼の微積分推論器は論理学界全体には知られていなかった。その結果、ライプニッツが達成した進歩の多くは、ライプニッツとはまったく独立したジョージ・ブールやオーガスタス・ド・モルガンなどの論理学者によって再現された。^[19]

ゴットロープ・フレーゲの 述語論理は命題論理を基盤としており、「三段論法論理と命題論理の際立った特徴」を組み合わせたものとして説明されている。^[20]結果的に、述語論理は論理の歴史に新しい時代をもたらした。しかし、フレーゲの後にも、自然演繹、真理木、真理表など、命題論理の進歩は続いた。自然演繹はゲルハルト・ゲンツェンとスタニスワフ・ヤシュコフスキによって発明された。真理木はエバート・ウィレム・ベートによって発明された。^[21]しかし、真理表の発明の帰属は定かではない。

^{フレーゲ[22]}とバートランド・ラッセル[ ^23]の著作には、真理表の発明に影響を与えたアイデアが含まれている。表形式構造そのもの（表の形式）は、一般的にルートヴィヒ・ヴィトゲンシュタインかエミール・ポスト（あるいは両者とも独立して）の功績とされている。^[22]フレーゲとラッセルの他に、真理表に先立つアイデアを考案したとされる人物には、フィロ、ブール、チャールズ・サンダース・パース [24] 、エルンスト・シュレーダーがいる。表^構造を考案したとされる人物には、ヤン・ルカシェヴィチ、アルフレッド・ノース・ホワイトヘッド、ウィリアム・スタンレー・ジェヴォンズ、ジョン・ヴェン、クラレンス・アーヴィング・ルイスがいる。^[23]最終的に、ジョン・ショスキーのように「誰か一人に真理表の『発明者』という肩書きを与えるべきかどうかは、まったく明らかではない」と結論づける者もいる。^[23]

現在大学で研究されている命題論理は、命題接続詞の意味のみを考慮して文の真偽の条件を評価する、あるいは文が他の文または文のグループから論理的に導かれるかどうかを評価する論理的帰結の基準を規定したものである。^[2]

命題論理は、真理値を持つ宣言文として定義される文を扱います。 ^{[25] [1]}文の例には以下が含まれます。

• Wikipedia は誰でも編集できる無料のオンライン百科事典です。
• ロンドンはイギリスの首都です。
• Wikipedia 編集者は全員、少なくとも 3 つの言語を話します。

平叙文は、「ウィキペディアとは何ですか？」のような質問や、「この記事の主張を裏付ける引用を追加してください。」のような命令文と対比されます。 ^{[26] [27]}このような非平叙文には真理値がなく、^[28]エロティック論理や命令型論理と呼ばれる非古典的な論理でのみ扱われます。

命題論理では、文は1つ以上の他の文を部分として含むことができる。^[1] 複文はより単純な文から形成され、構成文間の関係を表現する。^[29]これは、それらを論理接続詞と組み合わせることによって行われる。^{[29] [30]}複文の主な種類は、否定、接続詞、選言、含意、および双条件文であり、^[29]これらは、対応する接続​​詞を使用して命題を接続することによって形成される。^{[31] [32]}英語では、これらの接続詞は「and」（接続詞）、「or」（選言）、「not」（否定）、「if」（物質的条件文）、「if and only if」（双条件文）という単語で表現される。^{[1] [9]}このような複文の例としては、次のものが考えられる。

• Wikipedia は誰でも編集できる無料のオンライン百科事典で、すでに 何百万人もの 人が利用しています。 (接続詞)
• Wikipedia 編集者全員が少なくとも 3 つの言語を話すというのは真実ではありません。 (否定)
• ロンドンはイングランドの首都であるか、ロンドンはイギリスの首都であるか、あるいはその両方である。 (論理和) ^[b]

文に論理接続詞がない場合、それは単文^[1]または原子文^[30]と呼ばれます。また、文に1つ以上の論理接続詞が含まれている場合は、複文^[29]または分子文^[30]と呼ばれます。

文接続詞は、論理接続詞を含むより広いカテゴリです。^{[2] [30]}文接続詞とは、文を結合して新しい複合文を作成したり、^{[2] [30]}単一の文を屈折させて新しい文を作成したりする言語粒子です。^[2]論理接続詞、または命題接続詞は、それが作用する元の文が命題である（または命題を表現する）場合、その適用から生じる新しい文も命題である（または命題を表現する）という特徴を持つ一種の文接続詞です。^[2]哲学者の間では、命題が正確には何であるか、^{[6] [2]}だけでなく、自然言語のどの文接続詞を論理接続詞として数えるべきかについても意見が分かれています。^{[30] [2]}文接続詞は文関数子とも呼ばれ、^{[33]論理接続詞は}真理関数子とも呼ばれます。^[33]

議論は、前提と呼ばれる一連の文^[c]と結論と呼ばれる文のペアとして定義されます。^{[34] [30] [33]}結論は前提から導かれると主張され、 ^[33]前提は結論を支持すると主張されます。 ^[30]

以下は命題論理の範囲内での議論の例です。

前提 1: 雨が降っている場合は曇りです。

前提2:雨が降っています。

結論：曇りです。

この議論の論理形式はmodus ponens ^[35]として知られており、これは古典的に 有効な形式です。^[36]したがって、古典論理では、議論は有効ですが、特定のコンテキストでの気象事実に応じて、妥当である場合もそうでない場合もあります。この例の議論は、 § 形式化を説明するときに再利用されます。

議論が有効となるのは、その前提がすべて真であれば結論も真になる必要がある場合であり、その場合に限ります。 ^{[34] [37] [38]}あるいは、結論が偽である限りすべての前提が真になることが不可能である場合であり、その場合に限ります。 ^{[38] [34]}

妥当性は健全性と対比される。^[38]議論が健全であるのは、それが有効であり、その前提がすべて真である場合に限る。^{[34] [38]そうでなければ、それは}不健全である。^[38]

論理学は一般に、有効な議論を正確に特定することを目的としています。^[30]これは、結論が前提の論理的帰結である議論として有効な議論を定義することによって行われます。 ^[30]これは、意味的帰結として理解される場合、前提が真であるが結論が真ではないケースは存在しないことを意味します^[30] – 下の§ 意味論を参照してください。

命題論理は、通常、形式言語の式が命題を表現するために解釈される形式システムを通じて研究されます。この形式言語は証明システムの基礎であり、証明システムにより、前提から結論を導き出すことができるのは、それが前提の論理的帰結である場合のみです。このセクションでは、§ 例の議論を形式化することで、これがどのように機能するかを示します。命題論理の形式言語は、§ 言語で完全に指定され、証明システムの概要は、§ 証明システムで示されます。

命題論理は、論理接続詞によって分解できなくなる点を超えた命題の構造には関与しないため、^{[35] [1]}通常は、そのような原子（分割できない）文を、文を表す変数（命題変数）として解釈されるアルファベットの文字に置き換えて研究されます。^[1]命題変数を使用すると、§ 例の議論は次のように記号化されます。

前提1: ${\displaystyle P\to Q}$

前提2: ${\displaystyle P}$

結論： ${\displaystyle Q}$

P が「雨が降っている」、Q が「曇っている」と解釈されると、これらの記号表現は自然言語の元の表現と正確に対応します。それだけでなく、同じ論理形式を持つ他の推論とも対応します。

形式体系を使用して形式論理を表現する場合、ステートメント文字 (通常は、、やなどの大文字のローマ字) のみが直接表現されます。解釈時に生じる自然言語命題は、体系の範囲外であり、形式体系とその解釈の関係も同様に、形式体系自体の範囲外です。 ${\displaystyle P}$${\displaystyle Q}$${\displaystyle R}$

モーダスポネンスの妥当性が公理として受け入れられていると仮定すると、同じ§例の議論は次のように表すこともできます。

${\displaystyle {\frac {P\to Q,P}{Q}}}$

この表示方法は、自然演繹とシーケント計算のためのゲンツェンの表記法である。^[39]前提は、推論線と呼ばれる線の上に示され、^[11]前提の組み合わせを示すコンマで区切られる。 ^[40]結論は推論線の下に書かれる。^[11]推論線は統語的帰結を表し、^[11]演繹的帰結と呼ばれることもあり、^[41] ⊢で表すこともできる。^{[42] [41]}そのため、上記は と1行で書くこともできる。^[d]${\displaystyle P\to Q,P\vdash Q}$

統語的帰結は意味的帰結^[43]と対比され、⊧で表されます。^{[42] [41]}この場合、自然演繹推論規則であるモーダスポネンスが仮定されているため、結論は統語的に導かれます。推論規則の詳細については、以下の証明システムのセクションを参照してください。

命題計算の言語（一般には と呼ばれる）^{[41] [44] [30]}は次のように定義される: ^{[2] [10]}${\displaystyle {\mathcal {L}}}$

1. 原子式、原子文、 [ ^{35] [30]} 原子、^[45] プレースホルダー、プライム式、^[45] 命題文字、文文字、^[35]または変数と呼ばれる一連の基本記号、および
2. 演算子記号の集合。接続詞^{[14] [1] [46]} 論理接続詞[ ^1] 論理演算子^[1] 真理関数接続詞^[1] 真理関数子[ ^33]または命題接続詞^[2]と呼ばれる。

整形式式とは、任意の原子式、または文法規則に従って演算子記号を使用して原子式から構築できる任意の式です。言語は、整形式式の集合と同一であるか、 ^{[44]その集合（たとえば、接続詞と変数の集合と一緒に）}を含むかのいずれかとして定義されます。^{[10] [30]}${\displaystyle {\mathcal {L}}}$

通常、の構文は、次に示すように、いくつかの定義によって再帰的に定義されます。一部の著者は、言語の構文を定義する際に括弧を句読点として明示的に含めますが、 ^{[30] [47]}他の著者はコメントなしで括弧を使用します。^{[2] [10]}${\displaystyle {\mathcal {L}}}$

原子命題変数の集合、、、、...、および命題接続子の集合、、、、...、、、、、...、、、、...が与えられた場合、命題論理の式はこれらの定義によって再帰的に定義される：^{[2] [10] [46] [e} ]${\displaystyle p_{1}}$${\displaystyle p_{2}}$${\displaystyle p_{3}}$${\displaystyle c_{1}^{1}}$${\displaystyle c_{2}^{1}}$${\displaystyle c_{3}^{1}}$${\displaystyle c_{1}^{2}}$${\displaystyle c_{2}^{2}}$${\displaystyle c_{3}^{2}}$${\displaystyle c_{1}^{3}}$${\displaystyle c_{2}^{3}}$${\displaystyle c_{3}^{3}}$

定義 1 : 原子命題変数は式です。

定義 2 : が命題接続詞であり、A、B、C、…が m 個の式 (原子である可能性はあるが必ずしも原子とは限らず、異なる可能性はあるが必ずしも異なるとは限らない) のシーケンスである場合、これをA、B、C、…に適用した結果は式になります。${\displaystyle c_{n}^{m}}$${\displaystyle \langle }$${\displaystyle \rangle }$${\displaystyle c_{n}^{m}}$${\displaystyle \langle }$${\displaystyle \rangle }$

定義 3:それ以外は式ではありません。

A、B、C、…に適用した結果を関数表記法で(A、B、C、…) と書くと、整形式の式の例は次のようになります。 ${\displaystyle c_{n}^{m}}$${\displaystyle \langle }$${\displaystyle \rangle }$${\displaystyle c_{n}^{m}}$

• ${\displaystyle p_{5}}$
• ${\displaystyle c_{3}^{2}(p_{2},p_{9})}$
• ${\displaystyle c_{3}^{2}(p_{1},c_{2}^{1}(p_{3}))}$
• ${\displaystyle c_{1}^{3}(p_{4},p_{6},c_{2}^{2}(p_{1},p_{2}))}$
• ${\displaystyle c_{4}^{2}(c_{1}^{1}(p_{7}),c_{3}^{1}(p_{8}))}$
• ${\displaystyle c_{2}^{3}(c_{1}^{2}(p_{3},p_{4}),c_{2}^{1}(p_{5}),c_{3}^{2}(p_{6},p_{7}))}$
• ${\displaystyle c_{3}^{1}(c_{1}^{3}(p_{2},p_{3},c_{2}^{2}(p_{4},p_{5})))}$

上で定義 2として与えられたものは、式の構成に関係しており、コリン・ハウソンはこれを構成原理と呼んでいます。^{[35] [f]言語の構文の}定義におけるこの再帰 こそが、命題変数を指すのに「原子」という語の使用を正当化するものです。なぜなら、言語のすべての式は、究極の構成要素として原子から構築されるからです。^[2]複合式 (原子以外のすべての式) は、分子^[45]または分子文^[30]と呼ばれます。 (これは化学との不完全な類似です。化学分子は、単原子ガスのように、原子が 1 つだけの場合もあります。) ^[45]${\displaystyle {\mathcal {L}}}$

定義3で示した「それ以外は式ではない」という定義は、構文の他の定義で特に要求されていない式を言語から除外します。^[33]特に、無限に長い式は整形式ではないとみなされます。^[33]

上記の構文定義の代替案は、言語の文脈自由（CF）文法をバッカスナウア記法（BNF）で記述することです。 ^{[49] [50]これは、}哲学よりもコンピュータサイエンスで一般的です。^[50]これはさまざまな方法で行うことができますが、^[49]そのうちの特に短い方法は、一般的な5つの接続詞のセットに対する次の単一の節です。^{[50] [51]}${\displaystyle {\mathcal {L}}}$

${\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\&~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }$

この節は、自己参照的な性質（の定義のいくつかの分岐に があるため）のため、再帰的な定義としても機能し、したがって言語全体を指定します。これを拡張して様相演算子を追加するには、節の末尾に… を追加するだけです 。 ^[50]${\displaystyle \phi }$${\displaystyle \phi }$${\displaystyle |~\Box \phi ~|~\Diamond \phi }$

数学者は、命題定数、命題変数、スキーマを区別することがあります。命題定数は特定の命題を表しますが、[ ^52]命題変数はすべての原子命題の集合にわたります。^[52]しかし、スキーマ、つまりスキーマ文字はすべての式にわたります。^{[33] [1]}（スキーマ文字はメタ変数とも呼ばれます。）^{[34]命題定数は}A、B、Cで表され、命題変数はP、Q、Rで表され、スキーマ文字はギリシャ文字であることが多く、最もよく使われるのはφ、ψ、χです。^{[33] [1]}

しかし、著者の中には、形式体系では「命題定数」を2つしか認めない人もいます。それは、「真理」と呼ばれる特別な記号で、常にTrueと評価され、また、 「偽」と呼ばれる特別な記号で、常にFalseと評価されます。^{[53] [54] [55]}他の著者も、同じ意味を持つこれらの記号を含めていますが、それらを「ゼロ位真理関数」^[33]または同等の「ヌル項接続子」であると考えています。^[46]${\displaystyle \top }$${\displaystyle \bot }$

与えられた自然言語の論理のモデルとして機能するためには、形式言語は意味的に解釈されなければならない。^[30]古典論理では、すべての命題は2つの真理値、つまりTrueまたはFalseのいずれかに評価される。^{[1] [56]}たとえば、「Wikipedia は誰でも編集できる無料の オンライン百科事典です」はTrueと評価されるが、^{[57] 「Wikipedia は}紙の 百科事典です」はFalseと評価される。^[58]

その他の点では、以下の形式意味論はあらゆる命題論理の言語に適用できるが、意味値が2つしかない（二価性）、言語内の各式には2つのうちの1つだけが割り当てられる（無矛盾）、すべての式に値が割り当てられる（排中律）という仮定は、古典論理の特徴である。^{[56] [59] [33]} 3つ以上の真理値を持つ非古典論理とその独自の意味論については、「多値論理」、「3値論理」、「有限値論理」、および「無限値論理」の記事を参照するとよい。

与えられた言語 に対して、解釈^[60]、評価^[47]またはケース^{[30] [g]}は、の各式に意味値を割り当てることです。^[30]古典論理の形式言語では、ケースは、 の各式に、真理値 、つまり真 ( T 、または 1) と偽 ( F 、または 0) のいずれか一方 (両方ではない) を割り当てることとして定義されます。[ 61 ] [ 62 ]古典論理の規則に従う解釈は^、ブール評価 と呼ばれることがあります。 [ ^{47] [63]古典論理の形式言語の解釈は、しばしば}真理値表 で表現されます。^{[64] [1]}各式には単一の真理値のみが割り当てられているため、解釈は、定義域が、値域が意味値 、 [2] または である関数と^見なすことができます。^[30]${\displaystyle {\mathcal {L}}}$ ${\displaystyle {\mathcal {L}}}$${\displaystyle {\mathcal {L}}}$${\displaystyle {\mathcal {L}}}$${\displaystyle {\mathcal {V}}=\{{\mathsf {T}},{\mathsf {F}}\}}$${\displaystyle {\mathcal {V}}=\{1,0\}}$

異なる命題記号には、異なる解釈の可能性があります。たとえば、任意の特定の記号 に対して、 にTが割り当てられるか、 にFが割り当てられるかのいずれかの解釈が可能です。 のペアについては、両方にTが割り当てられるか、両方にFが割り当てられるか、にTが割り当てられてFが割り当てられるか、 にFが割り当てられてTが割り当てられるかのいずれかの解釈が可能です。^[64]には、つまり可算な数の命題記号があるため、 があり、したがって全体としては無数に異なる解釈が可能です。 ^[64]${\displaystyle n}$${\displaystyle 2^{n}}$${\displaystyle a}$${\displaystyle 2^{1}=2}$${\displaystyle a}$${\displaystyle a}$${\displaystyle a}$${\displaystyle b}$${\displaystyle 2^{2}=4}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle {\mathcal {L}}}$${\displaystyle \aleph _{0}}$${\displaystyle 2^{\aleph _{0}}={\mathfrak {c}}}$${\displaystyle {\mathcal {L}}}$

が解釈で、が公式を表す場合、§ 議論 で与えられた議論の定義は、 のペアとして述べることができます。ここで、 は前提の集合で、 は結論です。議論の妥当性の定義、つまり という性質は、反例 が存在しないことで述べることができます。ここで、反例は、議論の前提がすべて真であるが結論が真ではないケースとして定義されます。 ^{[30] [35] § 意味的真実性、妥当性、帰結 でわかるように、これは結論が前提の}意味的帰結であると言うことと同じです。 ${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \langle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\},\psi \rangle }$${\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}}$${\displaystyle \psi }$${\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}\models \psi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}}$${\displaystyle \psi }$

解釈は原子式に直接意味値を割り当てる。^{[60] [30]}分子式には、使用される接続詞に応じて、その構成原子の値の関数が割り当てられる。 ^{[60] [30]}接続詞は、接続詞を含む原子から構成される文の真理値が、接続詞が適用されている原子の真理値のみに依存するように定義される。 [ ^{60] [30]この仮定は、}コリン・ハウソンによって接続詞の真理機能の仮定と呼ばれている。^[35]

論理接続詞は、それが適用される命題変数が2つの可能な真理値のいずれかを取るときに取る真理値の観点からのみ意味的に定義されるため、 ^{[1] [30]}接続詞の意味的定義は通常、各接続詞の真理値表として表され、 ^{[1] [30] [65]}以下に示すようになります。

この表は、主要な5つの論理接続詞^{[9] [10] [11] [12]} それぞれをカバーしています。接続詞（ここではp ∧ qと表記）、選言（p ∨ q）、含意（p → q）、双条件（p ↔ q）、否定（状況に応じて¬pまたは¬q）です。これは、これらの演算子のそれぞれの意味を決定するのに十分です。^{[1] [66] [30]さまざまな種類の接続詞の真理値表については、「}真理値表」の記事を参照してください。

一部の著者（すなわち、この節で引用したすべての著者）は、接続詞の意味を表ではなく文のリストを使って書き出している。この形式では、の解釈として、5つの接続詞は次のように定義される：^{[33] [47]}${\displaystyle {\mathcal {I}}(\varphi )}$${\displaystyle \varphi }$

• ${\displaystyle {\mathcal {I}}(\neg P)={\mathsf {T}}}$もし、そしてその場合に限り、${\displaystyle {\mathcal {I}}(P)={\mathsf {F}}}$
• ${\displaystyle {\mathcal {I}}(P\land Q)={\mathsf {T}}}$もし、そして、もし、そして、${\displaystyle {\mathcal {I}}(P)={\mathsf {T}}}$${\displaystyle {\mathcal {I}}(Q)={\mathsf {T}}}$
• ${\displaystyle {\mathcal {I}}(P\lor Q)={\mathsf {T}}}$または、${\displaystyle {\mathcal {I}}(P)={\mathsf {T}}}$${\displaystyle {\mathcal {I}}(Q)={\mathsf {T}}}$
• ${\displaystyle {\mathcal {I}}(P\to Q)={\mathsf {T}}}$が真であるとき、そしてその場合に限り、${\displaystyle {\mathcal {I}}(P)={\mathsf {T}}}$${\displaystyle {\mathcal {I}}(Q)={\mathsf {T}}}$
• ${\displaystyle {\mathcal {I}}(P\leftrightarrow Q)={\mathsf {T}}}$もし、もし、もし、もし、もし、もし、もし、もし、${\displaystyle {\mathcal {I}}(P)={\mathsf {T}}}$${\displaystyle {\mathcal {I}}(Q)={\mathsf {T}}}$

の代わりに、 の解釈はと書き表されることもある。 ^{[33] [67]}あるいは、上記のような定義では、単に英語の文「 には値が与えられる」と書くこともできる。^[47]しかし、他の著者^{[68] [69]は、言語の}タルスキアンモデルについて話すことを好むかもしれない。その場合、代わりに という表記法を使用する。これは と言うことと同等であり、 はの解釈関数である。^[69]${\displaystyle {\mathcal {I}}(\varphi )}$${\displaystyle \varphi }$${\displaystyle |\varphi |}$${\displaystyle {\mathcal {I}}(\varphi )={\mathsf {T}}}$${\displaystyle \varphi }$${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathfrak {M}}}$${\displaystyle {\mathfrak {M}}\models \varphi }$${\displaystyle {\mathcal {I}}(\varphi )={\mathsf {T}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathfrak {M}}}$

これらの接続詞のいくつかは、他の接続詞を使って定義できる。例えば、含意 p → q は、¬p ∨ q; ^[70]のように、選言と否定を使って定義でき、選言は、¬(¬p ∧ ¬q) のように、否定と連言を使って定義できる。^[47]実際、古典的な命題トートロジーがすべてかつ唯一定理であるという意味で、真理機能的に完全なシステム^{[h]は、選言と否定だけを使って（}ラッセル、ホワイトヘッド、ヒルベルトが行ったように）^[2]導出できるし、含意と否定だけを使って（フレーゲが行ったように） [2]導出できるし、連言と否定だけを使って^{[ 2]導出できるし、}ジャン・ニコが行ったように、「かつではない」という接続詞（シェファーストローク）を 1 つだけ使っても^{[3] [2]}導出できる。^[2]結合否定接続詞（論理NOR ）は、それ自体で他のすべての接続詞を定義するのに十分であるが、^[47]他の接続詞にはこの性質がない。^[47]

ハウソン^[35]やカニンガム^[72]といった著者の中には、同値と二条件文を区別する者もいる。(同値については、ハウソンはそれを「真理機能的同値」と呼び、カニンガムはそれを「論理的同値」と呼んでいる。) 同値は ≡ で表され、メタ言語記号であるのに対し、二条件文は ↔ で表され、対象言語の論理接続詞である。いずれにせよ、同値または二条件文は、それによって接続された式があらゆる解釈で同じ意味値を割り当てられている場合にのみ真である。他の著者はしばしばこの区別をせず、対象言語の二条件文接続詞を表すために「同値」という単語^[11]や記号 ≡ ^[73]を使用する。 ${\displaystyle {\mathcal {L}}}$

とを言語の式（または文） 、を の解釈（またはケース）^[i]として与えると、次の定義が適用されます。^{[64] [62]}${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle {\mathcal {L}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {L}}}$

• 場合による真理値: ^[30]の文は、 がに真理値T を割り当てる場合、解釈の下で真である。^{[62] [64]}が の下で真である場合、 はのモデルと呼ばれる。^[64]${\displaystyle \varphi }$${\displaystyle {\mathcal {L}}}$ ${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$
• 場合による偽: ^{[30] は} 、が の解釈の下で偽であり、かつが の解釈の下で真である場合に限ります。^{[64] [74] [30]}これは、場合による偽の「否定の真理」定義です。^[30]場合による偽は、「補」定義によって定義することもできます。 は、が の解釈の下で偽であり、かつ が の解釈の下で真でない場合に限ります。^{[62] [64]}古典論理では、これらの定義は同等ですが、非古典論理では同等ではありません。^[30]${\displaystyle \varphi }$ ${\displaystyle {\mathcal {I}}}$${\displaystyle \neg \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$ ${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {I}}}$
• 意味的帰結：の文は、が真であり が真ではないという解釈が存在しない場合に、その文の意味的帰結（ ）となる。 ^{[62] [64] [30]}${\displaystyle \psi }$${\displaystyle {\mathcal {L}}}$${\displaystyle \varphi \models \psi }$${\displaystyle \varphi }$${\displaystyle \varphi }$${\displaystyle \psi }$
• 有効な式（トートロジー）：の文が論理的に有効（）である（ ^[j]またはトートロジー ）、^{[75] [76] [47]}とは、あらゆる解釈において真である、またはあらゆる場合に真であることを意味する。^{[62] [64] [30]}${\displaystyle \varphi }$${\displaystyle {\mathcal {L}}}$${\displaystyle \models \varphi }$
• 矛盾のない文：の文は、少なくとも一つの解釈において真であれば矛盾がない。矛盾があるとは、矛盾がないことを意味する。 ^{[62] [64]}矛盾した式は自己矛盾的とも呼ばれる。 [ ^1]また、自己矛盾[ ^1]または単に矛盾[ ^{77] [78] [79]}とも呼ばれる。ただし、この後者の名称は、特に という形式の文に用いられることがある。^[1]${\displaystyle {\mathcal {L}}}$${\displaystyle (p\land \neg p)}$

の解釈（ケース）では、次のような定義が与えられることがあります。 ${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {L}}}$

• 完全なケース:ケースが完全であるとは、 内の任意の に対してが 内で真であるか内で真である場合に限ります。^{[30] [80]}${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \neg \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {L}}}$
• 矛盾のないケース:ケースが矛盾のないものであるのは、との両方がにおいて真となる がに存在しないときのみである。^{[30] [81]}${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {L}}}$${\displaystyle \varphi }$${\displaystyle \neg \varphi }$${\displaystyle {\mathcal {I}}}$

古典論理では、すべてのケースが完全かつ一貫していると仮定しており、^[30]次の定理が適用される。

• 与えられた解釈に対して、与えられた式はその解釈の下では真か偽かのどちらかである。^{[64] [74]}
• いかなる公式も、同じ解釈の下では真と偽の両方になることはない。^{[64] [74]}
• ${\displaystyle \varphi }$は、 が の下で偽である場合にのみ、の下で真である。^{[64] [74] は}、 が の下で真である場合にのみ、の下で真である。^[64]${\displaystyle {\mathcal {I}}}$${\displaystyle \neg \varphi }$${\displaystyle {\mathcal {I}}}$ ${\displaystyle \neg \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {I}}}$
• と が両方とも の下で真ならば、 は の下で真である。^{[64] [74]}${\displaystyle \varphi }$${\displaystyle (\varphi \to \psi )}$${\displaystyle {\mathcal {I}}}$${\displaystyle \psi }$${\displaystyle {\mathcal {I}}}$
• かつならば。[ ^64]${\displaystyle \models \varphi }$${\displaystyle \models (\varphi \to \psi )}$${\displaystyle \models \psi }$
• ${\displaystyle (\varphi \to \psi )}$が の下で真であり、かつ がの下で真でないか、 がの下で真である場合に限ります。^[64]${\displaystyle {\mathcal {I}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {I}}}$${\displaystyle \psi }$${\displaystyle {\mathcal {I}}}$
• ${\displaystyle \varphi \models \psi }$が論理的に有効である場合、そしてその場合に限り、つまり、が が論理的に有効である場合に限り、である。^{[64] [74]}${\displaystyle (\varphi \to \psi )}$${\displaystyle \varphi \models \psi }$${\displaystyle \models (\varphi \to \psi )}$

命題論理における証明体系は、依存する論理的帰結の種類によって、意味的証明体系と統語的証明体系に大まかに分類できる。^{[82] [83] [84]}意味的証明体系は意味的帰結 ( ) に依存し、^[85]統語的証明体系は統語的帰結 ( ) に依存する。^[86]意味的帰結は、あらゆる解釈における命題の真理値を扱い、統語的帰結は、形式体系内の規則と公理に基づく前提から結論を導出することに関係する。^[87]このセクションでは、証明体系の種類のごく簡単な概要を示し、各証明体系に関するこの記事の関連セクションと、各証明体系に関する個別の Wikipedia 記事への リンクを示す。${\displaystyle \varphi \models \psi }$${\displaystyle \varphi \vdash \psi }$

意味論的証明システムは、 と表記される意味的帰結の概念に依存しており、これは、が真であれば、あらゆる解釈において も真でなければならないことを示している。^[87]${\displaystyle \varphi \models \psi }$${\displaystyle \varphi }$${\displaystyle \psi }$

真理値表は、あらゆる可能性のあるシナリオにおける命題論理式の真理値を決定するために使用される意味論的証明方法です。^[88]真理値表は、その構成原子の真理値を網羅的にリストすることにより、命題が真か偽か、同義語か矛盾かを示すことができます。^[89] § 真理値表による意味論的証明を参照してください。

意味的タブローは、命題の真実性を体系的に探究する別の意味証明技術である。^[90]これは、各ブランチが関連する命題の可能な解釈を表すツリーを構築する。^[91]すべてのブランチが矛盾につながる場合、元の命題は矛盾であると見なされ、その否定はトートロジーと見なされます。^[35] § タブローによる意味証明を参照。

対照的に、統語的証明システムは、特定の規則に従った記号の形式的な操作に焦点を当てています。統語的帰結の概念は、形式システムの規則を使用することで導出できることを意味しています。 ^[87]${\displaystyle \varphi \vdash \psi }$${\displaystyle \psi }$${\displaystyle \varphi }$

公理系とは、他の命題（定理）が論理的に導き出される公理または仮定の集合である。^[92]命題論理では、公理系は自明に真であると考えられる命題の基本集合を定義し、定理はこれらの公理に演繹規則を適用することによって証明される。^[93] § 公理による統語的証明を参照。

自然演繹は、通常の推論を反映した直感的な規則を使用して前提から結論を導き出すことを重視する統語的証明方法です。^[94]各規則は特定の論理接続詞を反映し、それをどのように導入または除去できるかを示します。^[94] §自然演繹による統語的証明を参照してください。

シークエント計算は、論理的演繹を式のシーケンスまたは「シークエント」として表現する形式システムです。^[95]ゲルハルト・ゲンツェンによって開発されたこのアプローチは、論理的演繹の構造的特性に焦点を当てており、命題論理内のステートメントを証明するための強力なフレームワークを提供します。^{[95] [96]}

意味論的妥当性の概念（あらゆる解釈において真であること）を利用すると、真理値表 を使って式の妥当性を証明することができます。真理値表は、式のあらゆる可能な解釈（変数への真理値の割り当て）を示します。^{[89] [45] [33]}真理値表のすべての行が真になる場合にのみ、式は意味的に妥当です（あらゆる解釈において真です）。^{[89] [45]}さらに、 が（そして が）妥当である場合、 は矛盾しています。^{[77] [78] [79]}${\displaystyle \neg \varphi }$${\displaystyle \varphi }$

例えば、この表は「p → (q ∨ r → (r → ¬p))」が無効であることを示している：^[45]

3行目の最後の列の計算は次のように表示されます。^[45]

さらに、が成り立つ場合、かつその場合に限り、が成り立つという定理を用いると、^{[64] [74]}真理値表を用いて、ある式が一連の式の意味論的帰結であることを証明することができる。すなわち、が成り立つ場合、かつその場合に限り、その式に対して全て真となる真理値表を作成することができる（つまり、が成り立つ）。^{[97] [98]}${\displaystyle \varphi \models \psi }$${\displaystyle (\varphi \to \psi )}$${\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}\models \psi }$${\displaystyle \left(\left(\bigwedge _{i=1}^{n}\varphi _{i}\right)\rightarrow \psi \right)}$${\displaystyle \models \left(\left(\bigwedge _{i=1}^{n}\varphi _{i}\right)\rightarrow \psi \right)}$

真理値表はn個の変数に対して2 ⁿ行あるため、nの値が大きいと長くなりすぎることがある。^[35]解析的表はより効率的だが、それでも機械的な^[65]意味論的証明方法である。解析的表は、「前提を偽にするか結論を真にする真理値分布を調べても推論の妥当性については何も学べない。演繹的妥当性を検討する際に関連する分布は、明らかに前提を真にするか結論を偽にする分布だけである」という事実を利用している。^[35]

命題論理の解析的表式は、以下の図式で述べられる規則によって完全に規定される。^[47]これらの規則は「符号付き式」を使用する。ここで、符号付き式は式またはであり、 は言語 の（符号なし）式である。^[47] （非公式には、は「真」と読み、 は「偽」と読む。）^[47] それらの正式な意味定義は、「どのような解釈においても、 が真の場合は符号付き式は真と呼ばれ、が偽の場合は偽と呼ばれるが、 が真の場合は符号付き式は偽と呼ばれ、が偽の場合は真と呼ばれる。」である。 ^[47]${\displaystyle TX}$${\displaystyle FX}$${\displaystyle X}$${\displaystyle {\mathcal {L}}}$${\displaystyle TX}$${\displaystyle X}$${\displaystyle FX}$${\displaystyle X}$${\displaystyle TX}$${\displaystyle X}$${\displaystyle X}$${\displaystyle FX}$${\displaystyle X}$${\displaystyle X}$

${\displaystyle {\begin{aligned}&1)\quad {\frac {T\sim X}{FX}}\quad &&{\frac {F\sim X}{TX}}\\{\phantom {spacer}}\\&2)\quad {\frac {T(X\land Y)}{\begin{matrix}TX\\TY\end{matrix}}}\quad &&{\frac {F(X\land Y)}{FX|FY}}\\{\phantom {spacer}}\\&3)\quad {\frac {T(X\lor Y)}{TX|TY}}\quad &&{\frac {F(X\lor Y)}{\begin{matrix}FX\\FY\end{matrix}}}\\{\phantom {spacer}}\\&4)\quad {\frac {T(X\supset Y)}{FX|TY}}\quad &&{\frac {F(X\supset Y)}{\begin{matrix}TX\\FY\end{matrix}}}\end{aligned}}}$

この表記法では、規則 2 はが の両方を生成するのに対し、は に分岐することを意味します。この表記法は、規則 3 と 4 についても同様に理解されます。^[47]古典論理の表では、符号付き式表記法が簡略化されることが多く、 は単に、 と書かれ、と書かれます。これが規則 1 を「二重否定の規則」と名付けた理由です。^{[35] [65]}${\displaystyle T(X\land Y)}$${\displaystyle TX,TY}$${\displaystyle F(X\land Y)}$ ${\displaystyle FX,FY}$${\displaystyle T\varphi }$${\displaystyle \varphi }$${\displaystyle F\varphi }$${\displaystyle \neg \varphi }$

一連の式のタブローを構築するには、すべての行が使用されるまで規則を適用して、より多くの行とツリーの枝を作成し、完全なタブローを作成します。場合によっては、枝がと の両方を含むようになり、これは矛盾です。その場合、枝は を閉じると言われます。^[35]ツリー内のすべての枝が閉じている場合、ツリー自体が閉じていると言われます。^[35]タブローの構築規則により、閉じた木は、それを構築するために使用された元の式、または式の集合自体が自己矛盾であり、したがって偽であったことの証明です。 [ ^35]逆に、タブローは論理式がトートロジーであることを証明することもできます。つまり、式がトートロジーである場合、その否定は矛盾であるため、その否定から構築されたタブローは閉じます。^[35]${\displaystyle TX}$${\displaystyle FX}$${\displaystyle X}$

議論 のタブローを作成するために、まず前提式の集合 を書き、各行に 1 つの式を で署名します(つまり、集合の各 について)。 ^[65]そして、それらの式とともに (順序は重要ではありません)、結論 も書き、で署名します(つまり)。^[65]次に、規則に従ってこれらすべての行を使用して真理値木 (解析タブロー) を作成します。^[65]閉じた木は、 の場合、そして の場合に限り、が矛盾する ( とも表記される)という事実により、議論が有効であったことの証明になります。 [ ^65]${\displaystyle \langle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\},\psi \rangle }$${\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}}$${\displaystyle T}$${\displaystyle T\varphi }$${\displaystyle T\varphi }$${\displaystyle \psi }$${\displaystyle F}$${\displaystyle F\psi }$${\displaystyle \varphi \models \psi }$${\displaystyle \{\varphi ,\sim \psi \}}$${\displaystyle \varphi ,\sim \psi \models }$

真理値表や意味表などの意味検証方法を使用してトートロジーや意味的帰結を検証すると、古典論理では、次の古典的な議論形式が意味的に有効である、つまり、これらのトートロジーと意味的帰結が成り立つことが示されます。^[33] ⟚ は、との同値性を示すために使用します。つまり、と の両方の省略形です。 ^[33]記号の読み方を補助するために、各式の説明を示します。説明では、記号 ⊧ (「ダブルターンスタイル」と呼ばれる) を「したがって」と読みます。これは一般的な読み方です。^{[33] [99]}ただし、多くの著者は、それを「伴う」と読むことを好みます。 ^{[33] [100]}または「モデル」と読むことを好みます。^[101]${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \varphi \models \psi }$${\displaystyle \psi \models \varphi }$

自然演繹は統語論的証明の方法であるため、典型的な接続詞の集合を持つ言語に対して推論規則（証明規則とも呼ばれる）^[34]を提供することによって規定される。これらの規則以外の公理は使用されない。^[104]規則については以下で説明し、その後に証明例を示す。 ${\displaystyle \{-,\&,\lor ,\to ,\leftrightarrow \}}$

推論規則を与える著者はそれぞれ多少異なるため、それについては後述します。しかし、証明の見た目や雰囲気でより印象的なのは、表記法の多様性です。先ほど簡単に説明しましたが、§ ゲンツェン表記法は、積み重ねることで大きなツリー型の自然演繹証明を作成できます^{[39] [11]} —「真理値木」と混同しないでください。「真理値木」は解析的タブローの別名です^[65]。スタニスワフ・ヤシュコフスキによるスタイルもあり、証明の数式はさまざまな入れ子になったボックス内に書かれています^{[39]。また、}フレドリック・フィッチによるヤシュコフスキのスタイルの簡略化(フィッチ表記法) もあり、ボックスは、仮定の導入部の下に単純な水平線、仮定の下の線の左側に垂直線に簡略化されています。^[39]最後に、この論文で実際に使用される唯一の表記法は、Patrick Suppes [39] によるものですが、^EJ LemmonとBenson Mates ^[105]によって広く普及しました。この方法の利点は、グラフィカルに作成および表示するのに最も労力がかからないことです。そのため、他の方法では証明を作成するために必要な 複雑なLaTeXコマンドを理解していない、この部分の論文を書いた編集者にとっては自然な選択でした。

そして、サッペス・レモン記法スタイル^[39]に従ってレイアウトされた証明は、文を含む行のシーケンスであり、^[34]各文は仮定、またはシーケンス内の前の文に証明規則を適用した結果のいずれかです。^[34]各証明行は、証明文、その注釈、仮定セット、および現在の行番号で構成されます。^[34]仮定セットは、行番号によって参照される、特定の証明文が依存する仮定をリストします。^[34]注釈は、現在の文を生成するために、どの証明規則が以前のどの行に適用されたかを指定します。^[34] §自然演繹の証明の例を参照してください。

自然演繹推論規則は、最終的にはゲンツェンによるもので、以下に示す通りである。^[104]証明には10の基本規則があり、仮定規則、二項接続詞の導入規則と除去規則の4組、および不合理帰結規則である。^[34]選言三段論法は、適切な∨-除去のより簡単な代替手段として使用することができ、^[34] MTTとDNは一般的に与えられている規則であるが、^[104]これらは基本的ではない。^[34]

以下の証明^[34]はMPPとRAAのみを使用してから導出され、MTTは他の2つの規則から導出できるため、原始的な規則ではないことを示しています。 ${\displaystyle -P}$${\displaystyle P\to Q}$${\displaystyle -Q}$

証明を公理的に行うことも可能であり、これは、特定のトートロジーを自明なものとして扱い、推論規則としてモーダスポネンス、および任意の整形式の式をその置換インスタンスに置き換えることを許可する置換規則を使用して、さまざまな他のトートロジーをそこから演繹することを意味する。^[107]あるいは、公理の代わりに公理スキーマを使用し、置換規則は使用しない。^[107]

このセクションでは、命題論理に関する歴史的に著名な公理系の公理をいくつか示します。その他の例や、そのような公理系に特有のメタ論理的定理 (完全性や一貫性など) については、「公理系 (論理)」の記事を参照してください。

公理的証明は、有名な古代ギリシャの教科書であるユークリッドの『幾何学原論』以来使われてきましたが、命題論理においては、ゴットロープ・フレーゲの1879年の 『Begriffsschrift 』にまで遡ります。^{[33] [107]}フレーゲの体系は、結合子として含意と否定のみを使用し、 ^[2] 6つの公理を持ち、^[107]以下の通りでした: ^{[108] [109]}

• 命題1:${\displaystyle a\supset (b\supset a)}$
• 命題2:${\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}$
• 命題8:${\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}$
• 提案28:${\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}$
• 提案31:${\displaystyle \neg \neg a\supset a}$
• 提案41:${\displaystyle a\supset \neg \neg a}$

フレーゲはこれらを、モーダス・ポネンスや置換規則（使用されたが、正確に述べられたことはなかった）とともに使用して、古典的な真理関数命題論理の完全かつ一貫した公理化を実現した。^[108]

ヤン・ルカシェヴィチは、フレーゲの体系では「3番目の公理は前の2つの公理から導き出せるので不要であり、最後の3つの公理は「」という1つの文に置き換えることができる」ことを示した。^{[109]これは、ルカシェヴィチの}ポーランド語表記法から現代の表記法に置き換えると、次のようになる。したがって、ルカシェヴィチは^[107]この3つの公理の体系の考案者とされている。 ${\displaystyle CCNpNqCpq}$${\displaystyle (\neg p\rightarrow \neg q)\rightarrow (p\rightarrow q)}$

• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$

フレーゲのシステムと同様に、このシステムは置換規則を使用し、推論規則としてモーダスポネンスを使用します。^[107]まったく同じシステムが（明示的な置換規則とともに）アロンゾチャーチによって提示され、^{[110]彼はそれをP} ₂システム^{[110] [111]}と呼び、普及に貢献しました。^[111]

置換規則の使用を避けるには、公理を図式的に表し、それを使って無限の公理集合を生成するという方法がある。したがって、ギリシャ文字を使って図式（任意の整形式式を表すメタ論理変数）を表すと、公理は次のように表される。^{[33] [111]}

• ${\displaystyle \varphi \to (\psi \to \varphi )}$
• ${\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}$
• ${\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}$

_{P 2}の概略バージョンは、ジョン・フォン・ノイマン^[107]に帰属し、 Metamath の「set.mm」形式証明データベースで使用されています。 ^[111]また、ヒルベルト^[112]にも帰属し、この文脈で命名されました。 ^[112]${\displaystyle {\mathcal {H}}}$

例として、P ₂における の証明を以下に示します。まず、公理に名前を付けます。 ${\displaystyle A\to A}$

（A1）${\displaystyle (p\to (q\to p))}$

（A2）${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

（A3）${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

そしてその証明は次のようになります。

1. ${\displaystyle A\to ((B\to A)\to A)}$       （（A1）の例）
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       （（A2）の例）
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       （（１）と（２）から、モーダスポネンスによる）
4. ${\displaystyle A\to (B\to A)}$       （（A1）の例）
5. ${\displaystyle A\to A}$       （（4）と（3）から、モーダスポネンスによる）

命題論理と述語論理の顕著な違いの1つは、命題論理式の充足可能性が決定可能であることである。^[113]命題論理式の充足可能性の決定はNP完全問題である。しかし、多くの有用なケースで非常に高速な実用的な方法が存在する（例えば、DPLLアルゴリズム、1962年、Chaffアルゴリズム、2001年）。最近の研究では、 SATソルバーアルゴリズムを拡張して、算術式を含む命題で動作するようにした。これらはSMTソルバーである。

• 一階論理
• 第二階命題論理
• 二階論理
• 高階論理

• Brown, Frank Markham (2003)、『ブール推論：ブール方程式の論理』、第 1 版、Kluwer Academic Publishers、マサチューセッツ州ノーウェル。第 2 版、Dover Publications、ニューヨーク州ミネオラ。
• Chang, CCおよびKeisler, HJ (1973)、「モデル理論」、North-Holland、アムステルダム、オランダ。
• Kohavi, Zvi (1978)、「スイッチングおよび有限オートマトン理論」、第 1 版、McGraw–Hill、1970 年。第 2 版、McGraw–Hill、1978 年。
• Korfhage, Robert R. (1974)、「離散計算構造」、Academic Press、ニューヨーク、NY。
• Lambek, J.および Scott, PJ (1986)、「高階カテゴリー論理入門」、ケンブリッジ大学出版局、ケンブリッジ、英国。
• メンデルソン、エリオット（1964）「数学論理学入門」、D.ヴァン・ノストランド社。

• ホフスタッター、ダグラス(1979)。ゲーデル、エッシャー、バッハ:永遠の黄金の編み紐。ベーシックブックス。ISBN 978-0-465-02656-2。

• Klement, Kevin C. (2006)、「命題論理」、James Fieser および Bradley Dowden (編)、インターネット哲学百科事典、Eprint。
• 形式述語計算は、公理的証明を伴う体系的な形式的展開を含む。
• PD Magnus 著の「forall x: an introduction to formal logic 」では、文論理の形式意味論と証明理論について説明しています。
• 第 2 章 / Logic In Action からの命題論理
• Project Nayuki の命題シークエント計算証明器。(注: 含意は の形式で入力でき!X|Y、シークエントは と で始まり>、コンマのない単一の式になります)
• 命題論理 - 生成文法
• 簡単な表現を理解するのに役立つ命題計算機