自然演繹法

自然演繹にはさまざまな記法スタイルがあり、^{[ 7 ]}それらのどれかに慣れていない読者にとっては証明を認識するのが難しい場合があります。この状況を改善するために、この記事では実際に使用するすべての記法の読み方を説明する§ 記法セクションがあります。このセクションでは記法スタイルの歴史的な進化のみを説明しますが、そのほとんどはパブリック著作権ライセンスの下で利用できる図がないため表示できません。読者は図についてはSEPとIEPを参照してください。

• ゲンツェンは、樹形証明を用いた自然演繹法を発明した。詳細は「 ゲンツェンの樹形記法」を参照のこと。
• ヤシュコフスキはこれを、さまざまな入れ子になったボックスを使用する記法に変更した。^{[ 7 ]}
• フィッチはヤシュコフスキーの箱の描き方を変え、フィッチ記法を作り出した。^{[ 7 ]}
• 1940年：クワイン^{[ 8 ]}は教科書の中で、角括弧で囲んだ行番号によって先行関係を示し、1957年のサップスの行番号表記を先取りした。
• 1950年：クワインは教科書（1982年、241～255ページ）の中で、証明の各行の左側に1つ以上の星印を用いて依存関係を示す方法を示した。これはクリーネの縦棒に相当する。（クワインの星印表記が1950年の初版に最初からあったのか、後の版で追加されたのかは完全には明らかではない。） 
• 1957年： Suppes著の教科書（1999年、25～150ページ）に掲載された実践論理定理証明入門。これは、各行の左側にある行番号によって依存関係（つまり、先行命題）を示していた。 
• 1963年：ストール（1979年、183～190ページ、215～219ページ）は、自然演繹推論規則に基づく連続論理的議論の行の先行依存関係を示すために行番号のセットを使用しています。 
• 1965年：レモン（1978）による教科書全体は、サップスの方法に基づいた方法を用いた論理証明の入門書であり、現在ではサップス・レモン記法として知られている。
• 1967年：クリーネ（2002年、50～58ページ、128～130ページ）は教科書の中で、2種類の実用的な論理証明を簡単に示しました。1つは各行の左側に前件命題を明示的に引用するシステムで、もう1つは左側に縦線を使用して依存関係を示すシステムです。^{[ 9 ]} 

自然演繹法を発明したゲンツェンは、独自の論証記法を持っていた。以下に示す簡単な論証でその例を見てみよう。命題論理における簡単な論証の例として、「雨が降っているならば曇りである。雨が降っている。したがって曇りである」というものがある。（これはモーダス・ポネンスである。）これを一般的な命題のリストとして表すと、次のようになる。

${\displaystyle 1)~P\to Q}$

${\displaystyle 2)~P}$

${\displaystyle \therefore ~Q}$

ゲンツェンの記法では、^{[ 7 ]}これは次のように書かれる。

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

前提は推論線と呼ばれる線の上に示され、^{[ 12 ] [ 13 ]}前提の組み合わせを示すコンマで区切られています。 ^{[ 14 ]}結論は推論線の下に書かれています。^{[ 12 ]}推論線は構文的帰結を表し、^{[ 12 ]}演繹的帰結とも呼ばれ、^{[ 15 ] [ 16 ]}また⊢で記号化されます。^{[ 16 ]}したがって、上記は1行で次のように書くこともできます。${\displaystyle P\to Q,P\vdash Q}$（構文的帰結を表すターンスタイルは、前提の組み合わせを表すコンマよりも優先順位が低く、さらにそれは実質含意に使用される矢印よりも優先順位が低い。したがって、この式を解釈するために括弧は必要ない。）^{[ 14 ]}

構文的帰結は意味的帰結と対比され、^{[ 17 ]} ⊧ で記号化される。^{[ 18 ] [ 16 ]}この場合、自然演繹は推論規則を基本要素とする構文的証明システムであるため、結論は構文的に導かれる。

この記事の大部分では、ゲンツェンのスタイルが用いられます。仮説的判断を内面化するためにゲンツェンが用いる注釈は、証明を「Aが真である」という判断のツリーではなく、シーケントのツリーΓ  ⊢ Aとして表現することで回避できます。 

Many textbooks use Suppes–Lemmon notation,^[7] so this article will also give that – although as of now, this is only included for propositional logic, and the rest of the coverage is given only in Gentzen style. A proof, laid out in accordance with the Suppes–Lemmon notation style, is a sequence of lines containing sentences,^[19] where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.^[19] Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number.^[19] The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.^[19] The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.^[19] Here's an example proof:

This proof will become clearer when the inference rules and their appropriate annotations are specified – see § Propositional inference rules (Suppes–Lemmon style).

In classicalpropositional calculus the formal language$\displaystyle {\mathcal {L}}}$ is usually defined (here: by recursion) as follows:^[20]

1. Each propositional variable is a formula.
2. "${\displaystyle \bot }$" is a formula.
3. If ${\displaystyle \varphi }$ and ${\displaystyle \psi }$ are formulae, so are ${\displaystyle (\varphi \land \psi )}$, ${\displaystyle (\varphi \lor \psi )}$, ${\displaystyle (\varphi \to \psi )}$, ${\displaystyle (\varphi \leftrightarrow \psi )}$.
4. Nothing else is a formula.

Negation (${\displaystyle \neg }$) is defined as implication to falsity

${\displaystyle \neg \phi \;{\overset {\text{def}}{=}}\;\phi \to \bot }$,

where ${\displaystyle \bot }$ (falsum) represents a contradiction or absolute falsehood.^{[21][22][23][24][25]}

古い出版物や、最小論理体系、直観主義論理体系、ヒルベルト論理体系などの論理体系に焦点を当てていない出版物では、否定を原始的な論理結合子とみなしており、つまり、否定は基本的な演算として想定され、他の結合子によって定義されていない。^{[ 26 ] [ 27 ]}ボストックなどの一部の著者は、${\displaystyle \bot }$そして${\displaystyle \top }$また定義する${\displaystyle \neg }$プリミティブとして。^{[ 28 ] [ 29 ]}

構文定義は、 § ゲンツェンのツリー記法を用いて、推論行の下に整形式の式を、その上にそれらの式で使用される図式変数を記述することによっても与えることができる。^{[ 26 ]}例えば、上記のボストックの定義の規則3と4に相当するものは、次のように記述される。

${\displaystyle {\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}}$。

別の表記法では、この言語の構文は「式」という単一のカテゴリを持つカテゴリ文法とみなされ、それは記号で表されます。${\displaystyle {\mathcal {F}}}$。したがって、構文の要素はすべてカテゴリ化によって導入され、その表記法は次のようになります。${\displaystyle \varphi$ :{\mathcal {F}}} 、意味は「${\displaystyle \varphi }$はカテゴリ内のオブジェクトを表す式です${\displaystyle {\mathcal {F}}}$^{[ 30 ]}文文字は、次のような分類によって導入されます。${\displaystyle P:{\mathcal {F}}}$、 ${\displaystyle Q:{\mathcal {F}}}$、 ${\displaystyle R:{\mathcal {F}}}$など。^{[ 30 ]}接続詞は、上記と同様の記述によって定義されますが、以下に示すように分類表記法を使用します。

この記事の残りの部分では、${\displaystyle \varphi$ :{\mathcal {F}}} 分類表記は、言語の文法を定義する Gentzen 表記法のステートメントに使用されます。Gentzen 表記法のその他のステートメントは推論であり、式が整形式であることを示すのではなく、シーケントが続くことを主張します。

命題言語${\displaystyle {\mathcal {L}}}$帰納的に定義される${\displaystyle \Phi$ ::=p_{1},p_{2},\dots \mid \bot \mid (\Phi \to \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )} 。

否定を次のように定義する${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,(\Phi \to \bot )}$。

以下は命題論理における自然演繹のための基本的な推論規則のリストです。^{[ 31 ] [ 26 ]}

この表ではギリシャ文字${\displaystyle \varphi ,\psi ,\chi }$これらは、原子命題だけでなく式全体にわたるスキーマです。ルールの名前は、その式ツリーの右側に付けられます。たとえば、最初の導入ルールは次のように名付けられます。${\displaystyle \land _{I}}$これは「接続詞導入」の略です。

• 最小限の論理：自然演繹規則は${\displaystyle ND_{MPC}=\{\land _{I},\land _{E},\lor _{I},\lor _{E},\to _{I},\to _{E}\}}$。

ルールなしで${\displaystyle \bot _{E}}$そして${\displaystyle \neg \neg _{E}}$このシステムは最小限の論理を定義している（ヨハンソンが論じたように）。^{[ 33 ]}

• 直観主義論理：自然演繹規則は${\displaystyle ND_{IPC}=ND_{MPC}\cup \{\bot _{E}\}}$。

ルールが${\displaystyle \bot _{E}}$（爆発原理）が最小論理の規則に追加され、システムは直観主義論理を定義します。

声明${\displaystyle P\to \neg \neg P}$は有効である（最小論理では既に有効である。以下の例 1 を参照）。一方、逆の含意は排中律を招くことになる。

• 古典論理：自然演繹規則は${\displaystyle ND_{CPC}=ND_{IPC}\cup \{\neg \neg _{E}\}}$[ ^{32 ]​}

リストされたすべての自然演繹規則が認められると、システムは古典論理を定義する。^{[ 34 ] [ 35 ] [ 36 ]}

例 1 : ^{[ 24 ]}最小限の論理による証明${\displaystyle P\to \neg \neg P}$。

ゴール：${\displaystyle P\to ((P\to \bot )\to \bot )}$ 証拠：

${\displaystyle {\cfrac {{\cfrac {[P]^{v}\qquad [P\to \bot ]^{u}}{\bot }}\to _{E}}{{\cfrac {((P\to \bot )\to \bot )}{P\to ((P\to \bot )\to \bot )}}\to _{I^{v}}}}\to _{I^{u}}}$

例2：最小限の論理による証明${\displaystyle A\to \left(B\to \left(A\land B\right)\right)}$:

${\displaystyle {\cfrac {{\cfrac {[A]^{u}\quad [B]^{w}}{A\land B}}\ \land _{I}}{{\cfrac {B\to \left(A\land B\right)}{A\to \left(B\to \left(A\land B\right)\right)}}\ \to _{I^{u}}}}\ \to _{I^{w}}}$

フィッチ式およびサップス＝レモン式の証明で用いられる、行番号と垂直方向の配置／仮定セットを用いた直線的な表現は、部分証明を明確に視覚化します。フィッチは（控えめに、かつ慎重に）導出規則を用いました。サップス＝レモンはさらに進んで、自然演繹規則のツールボックスに導出規則を追加しました。

サップスはゲンツェン式の規則を用いて自然演繹法を導入した。^{[ 37 ]}

• 彼は否定を矛盾という観点から定義した。${\displaystyle \neg P\equiv (P\to \bot )}$。
• He discussed derived rules explicitly, though not always distinguishing them clearly from primitive ones in layout.
• His system is close to minimal, but allows derived steps for brevity.

Lemmon formalized more derived rules.^[38] He as well defined negation as implication to falsity: ${\displaystyle \neg P\equiv P\to \bot }$. This is not stated as a formal definition in Beginning Logic, but it is implicitly assumed throughout the system, as evidenced by the following:

• Use of RAA (Reductio ad Absurdum): Lemmon regularly used RAA in the form: Assume ${\displaystyle P}$, derive ${\displaystyle \bot }$, then conclude ${\displaystyle \neg P}$.
  • This only works if ${\displaystyle \neg P}$ is understood as ${\displaystyle P\to \bot }$.
• Proofs involving contradiction: Lemmon used the fact that from ${\displaystyle \neg P\land P}$ one can derive ${\displaystyle \bot }$.
  • This requires treating ${\displaystyle \neg P}$ as ${\displaystyle P\to \bot }$, so that modus ponens yields contradiction.
• Absence of a primitive “¬” rule: Lemmon did not include a standalone rule for introducing or eliminating ¬. Instead, he derived negation using implication and contradiction.

In the table below, based on Lemmon (1978)^[39] and Allen & Hand (2022),^[19] Lemmon's derived rules are highlighted. They can be derived from the (non-highlighted) Gentzen rules.

There are nine primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rules of double negation and reductio ad absurdum, of which only one is needed.^[32][19]Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,^[19] and MTT is a commonly given rule,^[39] although it is not primitive.^[19]

§ サップス・レモン記法を導入した際に、すでに証明例を示したことを思い出してください。これは2番目の例です。

Γ ⊢ π ₁  : AおよびΓ、u : A ⊢ π ₂  : Bの場合、Γ ⊢ [π ₁ / u ] π ₂ : Bとなります。 

 これまで、「Γ ⊢ π : A 」という判断は、純粋に論理的な解釈をしてきました。型理論では、論理的な見方は、より計算的な対象観に置き換えられます。論理的解釈における命題は、型として、証明はラムダ計算 におけるプログラムとして見なされます。したがって、「π : A 」の解釈は、「プログラムπ は型Aを持つ」となります。論理結合子も異なる解釈が与えられます。論理積は積(×) として、含意は関数矢印(→) として見なされます。ただし、これらの違いは表面的なものにすぎません。型理論は、形成、導入、除去規則の観点から自然な演繹表現を持ちます。実際、読者は前のセクションから、いわゆる単純型理論を容易に再構築できます。

論理と型理論の主な違いは、焦点が型（命題）からプログラム（証明）に移っている点にある。型理論は主にプログラムの変換可能性または還元可能性に関心がある。すべての型には、還元不可能なその型の標準プログラムが存在する。これらは標準形式または標準値と呼ばれる。すべてのプログラムが標準形式に還元できる場合、その型理論は正規化（または弱正規化）であると言われる。標準形式が一意である場合、その理論は強正規化であると言われる。正規化可能性は、ほとんどの非自明な型理論ではまれな特徴であり、論理の世界とは大きく異なる。（ほとんどすべての論理導出には同等の正規導出があることを思い出してほしい。）その理由を概説すると、再帰的定義を許容する型理論では、値に還元されないプログラムを記述することが可能であり、そのようなループプログラムには一般に任意の型を与えることができる。特に、ループプログラムの型は⊥であるが、「⊥」の論理的証明は存在しない。このため、命題を型、証明をプログラムとするパラダイムは、もし機能するとしても一方向のみでしか機能しない。つまり、型理論を論理として解釈すると、一般的に矛盾した論理が得られる。

論理学と同様に、型理論にも多くの拡張や変種があり、一階述語論理や高階述語論理などが含まれます。依存型理論と呼ばれる分野は、多くのコンピュータ支援証明システムで使用されています。依存型理論では、量化子がプログラム自体を対象とすることができます。これらの量化型は、∀ や ∃ の代わりに Π や Σ と表記され、以下の構成規則に従います。

これらのタイプは、導入規則と消去規則からわかるように、それぞれ矢印タイプと積タイプの一般化である。

依存型理論は、その一般性においては非常に強力です。プログラムの型の中に、考えられるほぼすべての特性を直接表現できるからです。しかし、この一般性には大きな代償が伴います。型チェックが決定不能になる（外延型理論）か、外延推論がより困難になる（内包型理論）かのどちらかです。そのため、依存型理論の中には、任意のプログラムに対する量化を許容せず、整数、文字列、線形計画法など、特定の決定可能なインデックス領域のプログラムに限定するものもあります。

依存型理論では型がプログラムに依存することが許されているため、プログラムが型やその他の組み合わせに依存することが可能かどうかという疑問が生じるのは自然なことです。このような疑問にはさまざまな答えがあります。型理論でよく用いられるアプローチは、プログラムを型上で量化することを可能にすることであり、これはパラメトリック多相性とも呼ばれます。これには主に2種類あります。型とプログラムを分離すると、述語的多相性と呼ばれる、やや扱いやすいシステムが得られます。プログラムと型の区別が曖昧になると、高階論理の型理論版である非述語的多相性が得られます。文献では、依存性と多相性のさまざまな組み合わせが検討されており、最も有名なのはヘンク・バレンデレヒトのラムダキューブです。

論理学と型理論の交わりは、広大かつ活発な研究分野である。新しい論理体系は通常、論理フレームワークと呼ばれる一般的な型理論の枠組みの中で形式化される。構成計算やLFといった現代の代表的な論理フレームワークは、高階依存型理論に基づいており、決定可能性と表現力に関して様々なトレードオフが存在する。これらの論理フレームワーク自体も常に自然演繹システムとして規定されており、これは自然演繹アプローチの汎用性の高さを証明している。

Ω;⋅ ⊢ π ₁  : AおよびΩの場合、u : ( A valid )  ; Γ ⊢ π ₂  : C、次にΩ;Γ ⊢ [π ₁ / u ] π ₂  : C。

判断を異なる仮説の集合に分割するこの枠組みは、多領域コンテキストまたは多項コンテキストとも呼ばれ、非常に強力で拡張性があります。これは、さまざまな様相論理、線形論理、その他の部分構造論理など、いくつかの例を挙げると、多くの異なる様相論理に適用されています。しかし、自然演繹で直接形式化できる様相論理のシステムは比較的少数です。これらのシステムの証明論的特徴付けを与えるために、ラベル付けや深層推論システムなどの拡張が用いられます。

数式にラベルを追加することで、規則が適用される条件をより細かく制御できるようになり、ラベル付き演繹の場合のように、分析タブローのより柔軟な手法を適用できるようになります。ラベルは、クリプキ意味論で世界に名前を付けることも可能にします。Simpson (1994) は、クリプキ意味論の様相論理のフレーム条件をハイブリッド論理の自然演繹形式化における推論規則に変換する影響力のある手法を提示しています。Stouppa (2004) は、 Avron と Pottinger のハイパーシーケントや Belnap の表示論理など、多くの証明理論をS5 や B などの様相論理に適用した事例を概観しています。

Γ ⇒ π ₁  : AおよびΓ、u : A ⇒ π ₂  : Cの場合、Γ ⇒ [π ₁ /u] π ₂ : Cとなります。 

ほとんどの適切な論理体系では、カットは推論規則としては不要ですが、メタ定理としては証明可能です。カット規則の冗長性は、通常、カット除去と呼ばれる計算プロセスとして提示されます。これは自然演繹に興味深い応用があります。通常、自然演繹では、無数のケースがあるため、特定の性質を直接証明するのは非常に面倒です。たとえば、与えられた命題が自然演繹では証明できないことを示すことを考えてみましょう。単純な帰納的議論は、任意の命題を導入できる∨EやEのような規則のために失敗します。しかし、シーケント計算は自然演繹に関して完全であることがわかっているので、シーケント計算でこの証明不可能性を示すだけで十分です。さて、カットが推論規則として利用できない場合、すべてのシーケント規則は右または左に結合子を導入するため、シーケント導出の深さは最終結論の結合子によって完全に制限されます。したがって、証明不可能性を示すことははるかに容易です。なぜなら、考慮すべきケースの数は有限であり、各ケースは結論のサブ命題のみで構成されているからです。その簡単な例が、大域的整合性定理です。「⋅ ⊢ ⊥」は証明できません。シーケント計算版では、これは明らかに真です。なぜなら、「⋅ ⇒ ⊥」を結論とする規則は存在しないからです。証明論者は、このような性質から、カットフリーシーケント計算の定式化に取り組むことを好む場合が多いのです。

• アレン、コリン；ハンド、マイケル（2022）。論理学入門（第3 版）。マサチューセッツ州ケンブリッジ：MIT出版。ISBN 978-0-262-54364-4。
• アーサー、リチャード TW (2017).論理学入門：自然演繹、実例論証、ちょっとした歴史、そしてユーモア（第2 版）. ピーターバラ、オンタリオ州：ブロードビュー・プレス. ISBN 978-1-55481-332-2OCLC 962129086​​ 
• マウリシオ州アヤラ・リンコン。デ・モウラ、フラヴィオ LC (2017)。コンピュータ科学者のための応用論理。コンピューターサイエンスの学部トピック。スプリンガー。土井: 10.1007/978-3-319-51653-0。ISBN 978-3-319-51651-6。
• バーカー＝プラマー、デイブ；バーワイズ、ジョン；エチェメンディ、ジョン（2011）。言語証明と論理（第2 版）。CSLI出版。ISBN 978-1575866321。
• ボストック、デイヴィッド（1997）。中級論理学。オックスフォード；ニューヨーク：クラレンドン・プレス；オックスフォード大学出版局。ISBN 978-0-19-875141-0。
• Gallier, Jean (2005). "構成的論理学。パート I: 証明システムと型付き λ 計算に関するチュートリアル" . 2017 年 7 月 5 日のオリジナルからアーカイブ済み。2014年6 月 12 日取得。
• ゲンツェン、ゲルハルト・カール・エーリッヒ（1935a）。「Untersuchungen über das logische Schließen. I」。数学的ツァイシュリフト。39 (2): 176–210 .土井: 10.1007/bf01201353。S2CID 121546341。2015年12月24日のオリジナルからアーカイブ。 

— (1964) [1935]. 「論理演繹の研究」.アメリカ哲学季刊誌. 1 (4): 249–287 .

• ゲンツェン、ゲルハルト・カール・エーリッヒ（1935b）。「Untersuchungen über das logische Schließen. II」。数学的ツァイシュリフト。39 (3): 405–431 .土井: 10.1007/bf01201363。S2CID 186239837。 {{cite journal}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク)

— (1965) [1935]. 「論理演繹の研究」.アメリカ哲学季刊誌. 2 (3): 204–218 .

• ジラール、ジャン＝イヴ（1990）。証明と型。ケンブリッジ理論計算機科学論文集。ケンブリッジ大学出版局、ケンブリッジ、イングランド。2016年7月4日のオリジナルからアーカイブ。 2006年4月20日取得。ポール・テイラーとイヴ・ラフォンによる翻訳および付録。
• ハンソン、スヴェン・オーヴェ；ヘンドリックス、ヴィンセント・F. (2018).形式哲学入門. Springer Undergraduate Texts in Philosophy. Cham: Springer. ISBN 978-3-030-08454-7。
• ヤシュコフスキ、スタニスワフ（1934）。形式論理における仮定の規則について。ストーズ・マッコール編『ポーランド論理学 1920-39』に再録。
• ヨハンソン、インゲブリクト(1937)。「Der Minimalkalkül、ein reduzierter intuitionistischer Formalismus」。Compositio Mathematica (ドイツ語)。4：119～ 136。
• クリーネ、スティーブン・コール（1980）[1952]。メタ数学入門（第11 版）。ノースホランド。ISBN 978-0-7204-2103-3。
• クリーネ、スティーブン・コール（2009）[1952]。メタ数学入門。イシ・プレス・インターナショナル。ISBN 978-0-923891-57-2。
• クリーネ、スティーブン・コール（2002）[1967]。数理論理学。ニューヨーク州ミネオラ：ドーバー出版。ISBN 978-0-486-42533-7。
• レモン、エドワード・ジョン（ 1978）[1965]。『初級論理学』（第5版、1985年 版）。フロリダ州ボカラトン：ハケット出版。ISBN 0915144-50-6。
• Magnus, PD; Button, Tim; Trueman, Robert; Zach, Richard (2023). forall x: An Introduction to Formal Logic (Fall 2023  ed.). Open Logic Project . 2025年5月4日取得。
• Martin-Löf, Per (1996). 「論理定数の意味と論理法則の正当化について」(PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11– 60. 2023年12月8日にオリジナル(PDF)からアーカイブ済み。 2010年7月2日に取得。1983年4月、シエナ大学での短期コースの講義ノート。
• Paseau, AC; Leek, Robert. 「コンパクト性定理」 . インターネット哲学百科事典. 2024年3月22日取得.
• パソー、アレクサンダー；プレゲル、ファビアン（2023）「数学哲学における演繹主義」、ザルタ、エドワード・N；ノーデルマン、ウリ（編）『スタンフォード哲学百科事典』（2023年秋 版）、スタンフォード大学形而上学研究室、 2024年3月22日取得
• ペルティエ、フランシス・ジェフリー、ヘイゼン、アレン（2024）、「論理における自然演繹システム」、ザルタ、エドワード・N、ノーデルマン、ウリ（編）、『スタンフォード哲学百科事典』 （2024年春 版）、スタンフォード大学形而上学研究所、2024年3月22日取得
• Pfenning, Fr​​ank; Davies, Rowan (2001). "A judgmental reconstruction of modal logic" (PDF) . Mathematical Structures in Computer Science . 11 (4): 511– 540. CiteSeerX 10.1.1.43.1611 . doi : 10.1017/S0960129501003322 . S2CID 16467268 .  
• プラヴィッツ、ダグ(1965)。自然演繹: 証明理論的研究。ストックホルミエンシス大学;ストックホルム哲学研究、3。ストックホルム、ヨーテボリ、ウプサラ：アルムクヴィストとヴィクセル。OCLC 912927896。 
• プラウィッツ、ダグ（2006）。自然演繹：証明論的研究。ニューヨーク州ミネオラ：ドーバー出版。ISBN 9780486446554OCLC 61296001​​ 
• クワイン、ウィラード・ヴァン・オーマン（1981）[1940]。数理論理学（改訂 版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-55451-1。
• クワイン、ウィラード・ヴァン・オーマン（1982）[1950]。『論理の方法』（第4 版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-57176-1。
• レスタル、グレッグ（2018）、「部分構造論理」、ザルタ、エドワード・N（編）、『スタンフォード哲学百科事典』（2018年春版 ）、スタンフォード大学形而上学研究室、 2024年3月22日取得
• Simpson, Alex K. (1994).直観主義様相論理の証明論と意味論(PDF) (学位論文).エジンバラ研究アーカイブ (ERA) . hdl : 1842/407 .
• ストール、ロバート・ロス（1979）[1963]。集合論と論理学。ニューヨーク州ミネオラ：ドーバー出版。ISBN 978-0-486-63829-4。
• Stouppa, Phiniki (2004).様相証明理論の設計：S5 の場合。ドレスデン大学。CiteSeerX 10.1.1.140.1858。 修士論文。
• サップス、パトリック・コロネル(1999) [1957]。『論理学入門』。ニューヨーク州ミネオラ：ドーバー出版。ISBN 978-0-486-40687-9。
• サトクリフ、ジェフ。「命題論理」。www.cs.miami.edu 。マイアミ大学。 2025年5月4日取得。
• テナント、ニール（1990）[1978]。『自然論理学』（初版、訂正版 ）。エジンバラ大学出版局。ISBN 0852245793。
• ヴァン・ダーレン、ダーク(2013) [1980]。ロジックと構造。ユニバーシティテキスト (第 5 版)。ロンドン、ハイデルベルク、ニューヨーク、ドルドレヒト: Springer。土井：10.1007/978-1-4471-4558-5。ISBN 978-1-4471-4558-5。
• フォン・プラトー、ヤン（2013）。論理的推論の要素（初版 ）。ケンブリッジ：ケンブリッジ大学出版局。ISBN 978-1-107-03659-8。
• Weisstein, Eric W. 「Connective」 . mathworld.wolfram.com . 2024年3月22日取得。