自然演繹

論理学と証明理論において、自然演繹は、論理的推論が「自然な」推論方法に密接に関連した推論規則によって表現される一種の証明計算である。 ^{[1]これは、}演繹的推論の論理法則を表現するために可能な限り公理を使用するヒルベルトスタイルのシステムとは対照的である。

自然演繹は、ヒルベルト、フレーゲ、ラッセルの体系に共通する演繹的推論の公理化に対する不満という文脈から生まれた（例えば、ヒルベルト体系を参照）。このような公理化は、ラッセルとホワイトヘッドが数学論文『プリンキピア・マテマティカ』で使用したのが最も有名である。 1926年にポーランドで行われた、より自然な論理の扱い方を提唱したウカシェヴィチの一連のセミナーに刺激を受けたヤシュコフスキは、 1929年に図式的記法を用いてより自然な演繹を定義する最も初期の試みを行い、その後1934年と1935年に一連の論文で提案を更新した。^[2]彼の提案は、フィッチ式計算法（またはフィッチの図式）や、レモンが現在サッペス・レモン記法として知られる変種を与えたサッペス法などのさまざまな記法につながった。

現代的な形の自然演繹は、1933年にドイツの数学者ゲルハルト・ゲンツェンがゲッティンゲン大学数理科学部に提出した論文の中で独自に提唱した。^[3]自然演繹（あるいはドイツ語の同義語natürliches Schließen ）という用語はその論文の中で造られた。

ゲンツェンは数論の無矛盾性を確立したいという願望に突き動かされていた。無矛盾性の結果に必要な主要な結果であるカット消去定理（ハウプトザッツ）を自然演繹に対して直接証明することはできなかった。このため彼は代替システムであるシーケント計算を導入し、これによって古典論理と直観主義論理の両方に対してハウプトザッツを証明した。1961年と1962年の一連のセミナーでプラウィッツは自然演繹計算の包括的な概要を示し、ゲンツェンのシーケント計算に関する研究の多くを自然演繹の枠組みに移した。1965年の彼のモノグラフ「自然演繹：証明理論的研究」^[5]は自然演繹の参考書となり、様相論理と第二階述語論理への応用を含んでいた。

自然演繹では、推論規則を繰り返し適用することで、前提の集合から命題が演繹される。本稿で紹介するシステムは、ゲンツェンやプラウィッツの定式化を少し変えたものだ。しかし、マルティン＝レーフの論理的判断と接続詞の記述に、より忠実に従っている。^[6]

自然演繹には多種多様な表記法があり^[7] 、そのうちの 1 つに馴染みがなければ証明を認識するのが難しくなることがあります。この状況に対処するため、この記事には実際に使用するすべての表記法の読み方を説明する § 表記法 セクションがあります。このセクションでは表記法の歴史的進化についてのみ説明しますが、そのほとんどはパブリック著作権ライセンスの下で利用できる図がないため表示できません。読者は図については SEP と IEP を参照してください。

• ゲンツェンは、ツリー型の証明を使用した自然演繹を発明しました。詳細については、§ ゲンツェンのツリー表記法を参照してください。
• ヤシュコフスキはこれを様々なネストされたボックスを使用する表記法に変更した。^[7]
• フィッチはヤシュコフスキーのボックス描画法を変更し、フィッチ記法を作成した。^[7]
• 1940年:クワイン^[8]は教科書の中で、先行する依存関係を角括弧で囲んだ行番号で示し、1957年のサッペスの行番号表記法を予期した。
• 1950 年: 教科書の中で、クワインは (1982、pp. 241–255)、各証明行の左側に 1 つ以上のアスタリスクを使用して依存関係を示す方法を示しました。これは、クリーネの縦棒に相当します。(クワインのアスタリスク表記が 1950 年のオリジナル版に登場したのか、それとも後の版で追加されたのかは完全には明らかではありません。)
• 1957年: Suppes の教科書 (1999、pp. 25-150) に、実用論理の定理証明の入門が掲載されました。この教科書では、各行の左側に行番号を付けて依存関係 (つまり、先行命題) を示しました。
• 1963年: ストール(1979、pp. 183–190、215–219)は、自然演繹推論規則に基づいて、一連の論理的議論の行の先行依存関係を示すために行番号のセットを使用しています。
• 1965年: Lemmon (1965) による教科書全体は、現在Suppes–Lemmon 記法として知られているSuppesの方法に基づいた論理証明の入門書です。
• 1967年: クリーネは教科書の中で(2002、pp. 50–58, 128–130)、2種類の実用的な論理証明を簡単に示した。1つは各行の左側に先行命題を明示的に引用するシステムで、もう1つは依存関係を示すために左側に縦線を使用するシステムである。^[a]

以下は、論理接続詞の最も一般的な表記法のバリエーションを示す表です。

自然演繹を発明したゲンツェンは、議論のための独自の表記法を持っていました。これは、以下の簡単な議論で例証されます。命題論理における「雨が降っているなら曇りである。雨が降っている。したがって曇りである」などの簡単な議論の例があるとします。(これはmodus ponensです。) これを、一般的な命題のリストとして表すと、次のようになります。

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

${\displaystyle 2)~P}$

${\displaystyle \therefore ~Q}$

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

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

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

統語的帰結は意味的帰結^[16]と対比され、⊧で表されます。^{[15] [14]}この場合、自然演繹は推論規則をプリミティブとして想定する統語的証明システムであるため、結論は統語的に導かれます。

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

多くの教科書ではSuppes–Lemmon 記法^[7]が使用されているため、この記事でもその記法を扱います。ただし、現時点では命題論理についてのみ取り上げており、残りの説明は Gentzen スタイルでのみ行います。Suppes–Lemmon 記法スタイルに従って記述された証明は、文を含む行のシーケンスであり^[17] 、各文は仮定、またはシーケンス内の前の文に証明規則を適用した結果です。^[17]各証明行は、証明文、その注釈、仮定セット、および現在の行番号で構成されます。^[17]仮定セットには、特定の証明文が依存する仮定がリストされ、行番号で参照されます。^{[17]注釈には、現在の}文を生成するために、どの証明規則が以前のどの行に適用されたかが指定されます。^[17]証明の例を次に示します。

この証明は、推論規則とその適切な注釈が指定されるとより明確になります。§ 命題推論規則 (Suppes–Lemmon スタイル) を参照してください。

このセクションでは、命題論理言語の正式な構文を定義し、一般的な方法とゲンツェンスタイルの方法を対比します。

命題計算の形式言語は 通常、ボストックによる次のような再帰的定義によって定義される: ^[18]${\displaystyle {\mathcal {L}}}$

1. 各文文字は式です。
2. 「」と「」は数式です。${\displaystyle \top }$${\displaystyle \bot }$
3. が式であれば、 も式です。${\displaystyle \varphi }$${\displaystyle \neg \varphi }$
4. およびが公式である場合、、、、も同様です。${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle (\varphi \land \psi )}$${\displaystyle (\varphi \lor \psi )}$${\displaystyle (\varphi \to \psi )}$${\displaystyle (\varphi \leftrightarrow \psi )}$
5. それ以外は公式ではありません。

BNF文法 など他の方法もあります。^{[19] [20]}${\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\land ~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }$

§ゲンツェンのツリー記法を使って構文定義を与えることもできる。これは推論線の下に整形式の式を書き、その上にそれらの式で使用される図式変数を書くことによって行う。^[20]たとえば、上記のボストックの定義の規則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 )}}}$。

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

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

以下は、古典的な命題論理における自然演繹のための基本推論規則の完全なリストである: ^[20]

この表は、ギリシャ文字をスキーマとして使用する慣例に従っており、スキーマは原子命題だけでなく、任意の式に適用できます。規則の名前は、その式ツリーの右側に示されています。たとえば、最初の導入規則は という名前で、これは「接続詞導入」の略です。 ${\displaystyle \wedge _{i}}$

推論規則の使用例として、連言の可換性を考えてみましょう。A ∧ Bならば、B ∧ Aです。この導出は、より低い推論の前提が次に高い推論の結論と一致するように推論規則を構成することによって行うことができます。

2番目の例として、「 A ⊃ (B ⊃ (A ∧ B)) 」の導出を考えます。

この完全な導出には満たされていない前提はありませんが、サブ導出は仮説的です。たとえば、「B ⊃ (A ∧ B)」の導出は、前提「A」（uという名前）を持つ仮説的です。

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

§ Suppes–Lemmon 記法を紹介したときに、すでに例の証明が与えられていることを思い出してください。これは 2 番目の例です。

理論は、虚偽が（いかなる仮定からも）証明できない場合に無矛盾であり、すべての定理またはその否定が論理の推論規則を使用して証明できる場合に完全であると言われます。これらは論理全体についてのステートメントであり、通常、モデルの概念に結び付けられています。ただし、推論規則に対する純粋に構文上のチェックであり、モデルへの参照を必要としない、一貫性と完全性のローカルな概念があります。これらの最初のものは、ローカル一貫性、またはローカル還元性とも呼ばれるローカルな還元可能性であり、これは、接続詞の導入と直後のその除去を含む導出は、この迂回なしで同等の導出に変換できるというものです。これは、除去規則の強度のチェックです。除去規則は、前提にまだ含まれていない知識を含むほど強力であってはなりません。例として、接続詞を考えてみましょう。

${\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}u}$

双対的に、局所完全性とは、除去規則が接続詞をその導入規則に適した形式に分解するのに十分強力であることを意味します。接続詞の場合も同様です。

${\displaystyle {\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}}$

これらの概念は、カリー・ハワード同型性を使用したラムダ計算におけるβ-簡約 (ベータ簡約)とη-変換 (イータ変換)に正確に対応する。局所完全性により、すべての導出は、主結合子が導入された同等の導出に変換できることがわかる。実際、導出全体が、除去の後に導入が続くというこの順序に従っている場合、それは正規であると言われる。通常の導出では、すべての除去は導入より上で行われる。ほとんどの論理では、すべての導出には、正規形と呼ばれる同等の通常の導出がある。正規形の存在は、自然演繹のみを使用して証明することは一般に困難であるが、そのような説明は、1961 年のDag Prawitzによるものなど、文献には存在する。 ^[24]カットフリーのシーケント計算の表現によって間接的にこれを示す方がはるかに簡単である。

前のセクションの論理は、単一ソート論理、つまり、命題という単一の種類のオブジェクトを持つ論理の例です。この単純なフレームワークの拡張は数多く提案されていますが、このセクションでは、2 番目の種類の個体または項を使用して拡張します。より正確には、 で示される新しいカテゴリ「項」を追加します。可算な変数のセットと、別の可算な関数記号のセットを固定し、次の形成規則を使用して項を構築します。 ${\displaystyle {\mathcal {T}}}$${\displaystyle V}$${\displaystyle F}$

${\displaystyle {\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}}$

そして

${\displaystyle {\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}}$

命題については、述語の3番目の可算集合Pを考慮し、次の形成規則に従って 項上の原子述語を定義します。

${\displaystyle {\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}}$

最初の 2 つの形成規則は、項代数やモデル理論で定義されているものと実質的に同じ項の定義を提供しますが、これらの研究分野の焦点は自然演繹とはまったく異なります。3 番目の形成規則は、一階述語論理やモデル理論と同様に、原子式を実質的に定義します。

これらに加えて、量化命題の表記を定義する一対の形成規則が追加されます。1つは全称 (∀) 量化用、もう1つは存在量化 (∃) 用です。

${\displaystyle {\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}}$

全称量指定子には導入規則と除去規則があります。

${\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}}$

存在量指定子には導入規則と除去規則があります。

${\displaystyle {\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}}$

これらの規則では、表記法 [ t / x ] A は、 A内のxのすべての（目に見える）インスタンスをtに置き換えて、キャプチャを回避することを表します。^[c]前と同様に、名前の上付き文字は、解放されるコンポーネントを表します。つまり、項a は∀I の結論には出現できません（このような項は固有変数またはパラメータと呼ばれます）。また、∃E の仮説uおよびvは、仮説的導出の2番目の前提に局所化されます。前のセクションの命題論理は決定可能でしたが、量指定子を追加すると、論理は決定不可能になります。

これまでのところ、量化拡張は一階のものであり、命題を量化されるオブジェクトの種類と区別しています。高階論理は異なるアプローチを取り、命題の種類は 1 つだけです。量化子は、形成規則に反映されているように、量化のドメインとしてまったく同じ種類の命題を持ちます。

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}}$

高階論理の導入形式と除去形式については、この記事では取り上げません。1 階論理と高階論理の中間にあることは可能です。たとえば、2 階論理には2 種類の命題があり、1 つは項を量化するもので、もう 1 つは 1 種類の命題を量化するものです。

これまでの自然演繹の提示は、命題の性質に集中しており、証明の正式な定義は与えられていません。証明の概念を形式化するために、仮説的導出の提示を少し変更します。前提に証明変数（ある可算な変数の集合Vから）のラベルを付け、後続に実際の証明を添えます。前提または仮説は、回転木戸（⊢）によって後続から分離されます。この変更は、局所化された仮説と呼ばれることもあります。次の図は、変更をまとめたものです。

仮説の集合は、その正確な構成が重要でない場合は Γ と表記されます。証明を明確にするために、証明のない判断「A」から判断「πは (A) の証明である」に移ります。これは記号で「π : A 」と表記されます。標準的なアプローチに従って、証明は判断「π証明」の独自の形成ルールで指定されます。最も簡単な証明は、ラベル付けされた仮説を使用することです。この場合、証拠はラベルそのものです。

明示的な証明を伴う接続詞のいくつかを再検討してみましょう。連言については、導入規則 ∧I を見て、連言の証明の形式を見つけます。それらは、2 つの連言の証明のペアでなければなりません。つまり、

消去規則 ∧E ₁と ∧E _{2 は}左または右の連言のいずれかを選択します。したがって、証明は 1 つ目の射影 ( fst ) と 2 つ目の射影 ( snd ) のペアになります。

含意については、導入形式は λ を使用して記述された仮説を局所化または結合します。これは、発行されたラベルに対応します。規則では、「Γ、u : A 」は、追加の仮説uとともに、仮説 Γ の集合を表します。

証明が明示的に利用できると、証明を操作したり推論したりすることができます。証明に関する重要な操作は、ある証明で使用されている仮定を別の証明に置き換えることです。これは一般に置換定理として知られており、 2 番目の判断の深さ (または構造) に関する帰納法によって証明できます。

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

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

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

論理と同様に、型理論には、一階バージョンや高階バージョンなど、多くの拡張と変種があります。依存型理論と呼ばれる分野の 1 つは、多くのコンピューター支援証明システムで使用されています。依存型理論では、量指定子がプログラム自体の範囲をカバーできます。これらの量指定子付き型は、∀ や ∃ ではなく、Π や Σ と表記され、次の形成規則に従います。

これらの型は、導入規則と除去規則からもわかるように、それぞれ矢印型と積型の一般化です。

依存型理論は、完全に一般化されると非常に強力です。プログラムの考えられるほぼすべての特性を、プログラムの型で直接表現できます。この一般化には大きな代償が伴います。つまり、型チェックが決定不能 (外延型理論) であるか、外延的推論がより困難 (内包型理論) であるかのどちらかです。このため、一部の依存型理論では、任意のプログラムに対する量化を許可せず、整数、文字列、線形プログラムなど、特定の決定可能なインデックス ドメインのプログラムに制限します。

依存型理論では型がプログラムに依存することが許されているため、当然の疑問として、プログラムが型やその他の組み合わせに依存することは可能かどうかが挙げられます。このような疑問には多くの種類の答えがあります。型理論でよく使われるアプローチは、型に対してプログラムを量化できるようにすることです。これはパラメトリック多態性とも呼ばれます。これには主に 2 種類あります。型とプログラムを分けておくと、述語的多態性と呼ばれる、より行儀の良いシステムが得られます。プログラムと型の区別があいまいな場合は、非述語的多態性としても知られる、高階論理の型理論的類似物が得られます。文献では依存性と多態性のさまざまな組み合わせが検討されていますが、最も有名なのはHenk Barendregtのラムダ キューブです。

論理と型理論の交わりは、広大で活発な研究領域です。新しい論理は通常、論理フレームワークと呼ばれる一般的な型理論の設定で形式化されます。構成の計算やLFなどの人気のある現代の論理フレームワークは、決定可能性と表現力の点でさまざまなトレードオフを伴う高階依存型理論に基づいています。これらの論理フレームワーク自体は常に自然演繹システムとして指定されており、これは自然演繹アプローチの汎用性の証です。

簡潔にするために、これまで紹介した論理は直観主義的でした。古典論理は、直観主義論理に排中律という公理または原理を追加して拡張します。

任意の命題 p に対して、命題 p ∨ ¬p は真です。

この記述は明らかに導入でも除去でもありません。実際、2つの異なる接続詞が含まれています。ゲンツェンの排中律の元々の扱いは、ヒルベルトとハイティングの体系に類似の形ですでに存在していた次の3つの（同等の）定式化のうちの1つを規定していました。

(XM _{3 は}単にE で表現された XM _{2です。) 排中律のこの扱いは、純粋主義者の立場からすると好ましくないだけでなく、正規形の定義にさらなる複雑さをもたらします。}

導入規則と除去規則のみによる古典的な自然演繹の比較的満足のいく処理は、1992 年にパリゴによってλμと呼ばれる古典的なラムダ計算の形で初めて提案されました。彼のアプローチの重要な洞察は、真理中心の判断A を、シーケント計算を彷彿とさせるより古典的な概念で置き換えることでした。局所的な形式では、 Γ ⊢ Aの代わりにΓ ⊢ Δ を使用し、 Δ は Γ に似た命題のコレクションです。 Γ は連言として扱われ、 Δ は選言として扱われました。この構造は基本的に古典的なシーケント計算から直接取り入れられていますが、 λμ の革新は、 LISPとその子孫に見られるcallccまたは throw/catch メカニズムの観点から、古典的な自然演繹証明に計算上の意味を与えたことです。(ファーストクラス制御も参照してください。)

もう一つの重要な拡張は、基本的な真理の判断以上のものを必要とする様相論理やその他の論理に対する拡張であった。これらは、1965年にプラウィッツによって自然演繹スタイルで、アレティック様相論理S4とS5について初めて記述され、^[5]それ以来、関連する膨大な研究が蓄積されてきた。簡単な例を挙げると、様相論理S4は、真理に関して定言的な 「有効」という1つの新しい判断を必要とする。

「B」が真であるという仮定なしに「A」が真である場合、「A」は有効です。

この断定的な判断は、次のような導入および除去規則を持つ単項接続詞 ◻ A（「必然的に A」と読む）として内部化されます。

前提「A 有効」には定義ルールがないことに注意します。代わりに、妥当性のカテゴリ定義が使用されます。仮説が明示されている場合、このモードはローカライズされた形式でより明確になります。「Ω;Γ ⊢ A」と書きます。ここで、Γ には前述のように真の仮説が含まれ、Ω には有効な仮説が含まれます。右側には単一の判断「A 」があります。「Ω ⊢ A 有効」は定義上「Ω;⋅ ⊢ A 」と同じであるため、ここでは妥当性は必要ありません。導入形式と排除形式は次のようになります。

モーダル仮説には、仮説規則と置換定理の独自のバージョンがあります。

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

判断を別個の仮説の集合に分けるこの枠組みは、マルチゾーンまたはポリアディックコンテキストとしても知られ、非常に強力で拡張性があります。いくつかの例を挙げると、多くの異なる様相論理、また線形論理やその他の部分構造論理にも適用されています。ただし、様相論理のシステムは、自然演繹で直接形式化できるものが比較的少数です。これらのシステムの証明理論的特徴付けを行うには、ラベル付けや深い推論のシステムなどの拡張が必要です。

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

シーケント計算は、数理論理学の基礎として自然演繹に代わる主要なものである。自然演繹では、情報の流れは双方向である。すなわち、消去規則は分解によって情報を下向きに流し、導入規則は組み立てによって情報を上向きに流す。したがって、自然演繹の証明は、純粋なボトムアップまたはトップダウンの読み方を持たないため、証明検索の自動化には適さない。この事実に対処するため、ゲンツェンは1935年にシーケント計算を提案したが、当初は述語論理の一貫性を明らかにするための技術的手段を意図していた。クリーネは、1952年の画期的な著書「メタ数学入門」で、現代的なスタイルでシーケント計算を初めて定式化した。^[25]

シークエント計算では、すべての推論規則は純粋にボトムアップの読み方をします。推論規則は、ターンスタイルの両側の要素に適用できます。(自然演繹と区別するために、この記事では、シークエントに右矢印 ⊢ ではなく二重矢印 ⇒ を使用します。) 自然演繹の導入規則は、シークエント計算では右規則と見なされ、構造的に非常に似ています。一方、除去規則は、シークエント計算では左規則になります。例として、選言を考えてみましょう。右規則はおなじみです。

左に：

局所化された形式での自然演繹の∨E規則を思い出してください。

∨E の前提の後続である命題A ∨ Bは、左規則 ∨L の結論の仮説に変わります。したがって、左規則は、一種の反転した消去規則と見ることができます。この観察は次のように説明できます。

シークエント計算では、左ルールと右ルールは、自然演繹における除去ルールと導入ルールの接点に対応する初期シークエントに到達するまで、同期して実行されます。これらの初期ルールは、表面的には自然演繹の仮説ルールに似ていますが、シークエント計算では、左命題と右命題の転置または握手を記述します。

シーケント計算と自然演繹の間の対応は、健全性定理と完全性定理のペアであり、どちらも帰納的議論によって証明可能です。

⇒ ⊢ に対する健全性

Γ ⇒ AならばΓ ⊢ A。

⇒ ⊢ に対する完全性

Γ ⊢ AならばΓ ⇒ A。

これらの定理から、シーケント計算は真理の概念を変えないことが明らかである。なぜなら、同じ命題の集合は真のままだからである。したがって、シーケント計算の導出では、以前と同じ証明対象を使用できる。例として、接続詞を考えてみよう。右の規則は、導入規則と実質的に同一である。

ただし、左のルールでは、対応する除去ルールでは実行されない追加の置換がいくつか実行されます。

したがって、シークエント計算で生成される証明の種類は、自然演繹の証明とはかなり異なります。シークエント計算は、β-正規 η-長形式と呼ばれる形式で証明を生成します。これは、自然演繹証明の正規形式の標準表現に対応します。これらの証明を自然演繹自体を使用して記述しようとすると、インターカレーション計算(ジョン バーンズによって最初に記述) と呼ばれるものが得られ、これを使用して自然演繹の 正規形式の概念を正式に定義できます。

自然演繹の置換定理は、シーケント計算における カットとして知られる構造規則または構造定理の形をとります。

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

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

• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011). Language Proof and Logic (第 2 版). CSLI Publications. ISBN 978-1575866321。
• Gallier, Jean (2005). 「構成的論理。パート I: 証明システムと型付きλ計算に関するチュートリアル」 。2014年6 月 12 日閲覧。
• ゲンツェン、ゲルハルト・カール・エーリッヒ（1934年）。 「Untersuhungen über das logische Schließen. I」。数学的ツァイシュリフト。39 (2): 176–210。土井：10.1007/BF01201353。S2CID  121546341。 (英訳: ME サボ著『論理的演繹の調査』。ゲルハルト・ゲンツェン著作集。ノースホランド出版社、1969 年。)
• ゲンツェン、ゲルハルト・カール・エーリッヒ（1935年）。 「Untersuchungen über das logische Schließen. II」。数学的ツァイシュリフト。39 (3): 405–431。土井：10.1007/bf01201363。S2CID  186239837。
• ジャン=イヴ・ジラール(1990)。証明と型。ケンブリッジ理論計算機科学論文集。ケンブリッジ大学出版局、ケンブリッジ、イギリス。2016 年 7 月 4 日時点のオリジナルよりアーカイブ。2006年 4 月 20 日閲覧。翻訳および付録はポール・テイラーとイヴ・ラフォンが担当しました。
• ヤシュコフスキ、スタニスワフ（1934）。形式論理における仮定の規則について。Storrs McCall編『Polish logic 1920–39』に再録。
• クリーネ、スティーブン・コール（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。
• レモン、エドワード・ジョン（1965年）。『論理学入門』。トーマス・ネルソン。ISBN 978-0-17-712040-4。
• Martin-Löf, Per (1996). 「論理定数の意味と論理法則の正当性について」(PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11–60.1983年4月、シエナ大学での短期コースの講義ノート。
• Pfenning, Fr​​ank; Davies, Rowan (2001). 「様相論理の判断的再構築」(PDF) .コンピュータサイエンスにおける数学的構造. 11 (4): 511–540. CiteSeerX  10.1.1.43.1611 . doi :10.1017/S0960129501003322. S2CID  16467268.
• プラヴィッツ、ダグ(1965)。自然演繹: 証明理論的研究。 Acta Universitatis Stockholmiensis、ストックホルムの哲学研究 3. ストックホルム、ヨーテボリ、ウプサラ: アルムクヴィストとヴィクセル。
• プラウィッツ、ダグ（2006）[1965]。自然演繹：証明理論的研究。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-44655-4。
• クワイン、ウィラード・ヴァン・オーマン（1981）[1940]。数学論理（改訂版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-55451-1。
• クワイン、ウィラード・ヴァン・オーマン（1982）[1950]。論理の方法（第4版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-57176-1。
• シンプソン、アレックス (1993)。直観主義様相論理の証明理論と意味論(PDF)。エディンバラ大学。博士論文。
• ストール、ロバート・ロス（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。
• ヴァン・ダーレン、ダーク(2013) [1980]。ロジックと構造。ユニバーシティテキスト (第 5 版)。ロンドン、ハイデルベルク、ニューヨーク、ドルドレヒト: Springer。土井：10.1007/978-1-4471-4558-5。ISBN 978-1-4471-4558-5。

• ラボレオ、ダニエル・クレメンテ (2004 年 8 月)。 「自然控除入門」（PDF）。
• 「Domino On Acid」 。 2023年12月10日閲覧。ドミノゲームとして視覚化された自然推論
• ペルティエ、フランシス・ジェフリー。「自然演繹と初等論理学教科書の歴史」(PDF)。
• 「論理における自然演繹システム」の項目、フランシス・ジェフリー・ペルティエ、アレン・ヘイゼン著、スタンフォード哲学百科事典、2021年10月29日
• Levy, Michel. 「命題証明器」。