演繹定理

数理論理学において、演繹定理は、仮説を明示的に公理化しないシステムにおいて、仮説からの条件付き証明を行うことを正当化するメタ定理である。つまり、含意A  →  B を証明するには、 A を仮説として仮定し、次にB を導出すれば十分である。演繹定理は、命題論理と一階述語論理の両方に存在する。^{[1]演繹定理は}ヒルベルトスタイルの演繹システムにおいて重要なツールである。演繹定理によって、それを使用しない場合よりもわかりやすく、通常ははるかに短い証明を書くことができるからである。他の特定の形式的証明システムでは、明示的な推論規則によって同様の利便性が提供される。たとえば、自然演繹ではこれを含意導入と呼ぶ。

より詳しくは、命題論理の演繹定理は、式が一連の仮定から演繹可能な場合、その含意は から演繹可能であることを述べています。記号で、はを意味します。 が空集合である特殊なケースでは、演繹定理の主張は、 とより簡潔に記述できます。を意味します。述語論理の演繹定理は似ていますが、いくつかの追加の制約があります (たとえば、が閉じた式である場合に満たされる)。一般に、演繹定理では、検討中の理論のすべての論理的詳細を考慮する必要があるため、各論理システムには技術的に独自の演繹定理が必要ですが、違いは通常はわずかです。 ${\displaystyle B}$${\displaystyle \デルタ \cup \{A\}}$${\displaystyle A\to B}$${\displaystyle \Delta }$${\displaystyle \Delta \cup \{A\}\vdash B}$${\displaystyle \Delta \vdash A\to B}$${\displaystyle \Delta }$${\displaystyle A\vdash B}$${\displaystyle \vdash A\to B}$${\displaystyle A}$

演繹定理は、通常の^{[2]一階論理の} 演繹システムを持つすべての一階理論に対して成り立ちます。^[3]しかし、演繹定理が成り立たない新しい推論規則が追加された一階システムもあります。^{[4]最も顕著なのは、演繹定理が}バーコフ-フォン・ノイマン 量子論理では成り立たないことです。これは、ヒルベルト空間の線型部分空間が非分配格子を形成するためです。

1. 公理1を「証明する」: P →( Q → P ) ^[a]

   • P 1.仮説
     • Q 2. 仮説
     • P 3. 1の繰り返し
   • Q → P 4. 2から3への減算

   • P →( Q → P ) 5. 1から4までの演繹 QED
2. 公理2を「証明」する:

   • P →( Q → R ) 1.仮説
     • P → Q 2.仮説
       • P 3. 仮説
       • Q 4. モーダスポネンス 3,2
       • Q → R 5. モーダスポネンス 3,1
       • R 6. モーダスポネンス 4,5
     • P → R 7. 3から6までの減点
   • ( P → Q )→( P → R ) 8. 2から7までの演繹

   • ( P →( Q → R ))→(( P → Q )→( P → R )) 9. 1から8までの演繹 QED
3. 公理1を使って(( P →( Q → P ))→ R )→ Rを示します。

   • ( P →( Q → P ))→ R 1. 仮説
   • P →( Q → P ) 2. 公理1
   • R 3. モーダスポネンス 2,1

   • (( P →( Q → P ))→ R )→ R 4. 1から3までの演繹 QED

例から、通常の公理論理学に 3 つの仮想 (または追加的かつ一時的な) 推論規則を追加したことがわかります。これらは、「仮説」、「繰り返し」、および「演繹」です。通常の推論規則 (つまり、「モーダスポネンス」およびさまざまな公理) は引き続き使用できます。

1.仮説とは、既存の前提に新たな前提を加えるステップです。つまり、前のステップSが次のように推論された場合:

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash S,}$

すると、別の前提Hが追加され、次のようになります。

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n},H\vdash H.}$

これは、インデントのn番目のレベルからn +1番目のレベルに移動し、^[b]と言うことで表されます。

• S前のステップ
  • H仮説

2.繰り返しは、前のステップを再利用するステップです。実際には、これは、最新の仮説ではない仮説を、演繹ステップの前の最終ステップとして使用する場合にのみ必要です。

3.演繹とは、最新の仮説（まだ利用可能なもの）を削除し、それを前のステップの前に置くステップです。これは、次のように 1 レベルインデントを解除することで示されます。^[b]

• H仮説
• .........（その他の手順）
• C ( Hから導き出された結論)

• H → C控除

命題論理の公理バージョンでは、通常、公理スキーマのいずれかが使用されます（P、Q、およびR は任意の命題に置き換えられます）。

• 公理1は、P →( Q → P )である。
• 公理2は、( P →( Q → R ))→(( P → Q )→( P → R ))である。
• 手法は次のとおりです: PおよびP → QからQ を推測します

これらの公理スキーマは、演繹定理を簡単に導出できるようにするために選択されています。そのため、論点先取のように見えるかもしれません。ただし、真理値表を使用してトートロジーであることと、モーダスポネンスが真理値を保持することを確認することで、正当化できます。

これらの公理スキーマから、以下で使用される 定理スキーマP → P (含意の反射性) をすぐに推測できます。

1. ( P →(( Q → P )→ P ))→(( P →( Q → P ))→( P → P )) 公理スキーマ2より、 P、( Q → P )、P
2. P →(( Q → P )→ P ) 公理スキーム1より、 P、( Q → P )
3. ( P →( Q → P ))→( P → P ) はステップ2とステップ1に適用されたモーダスポネンスから
4. P →( Q → P ) 公理図1より、P、Q
5. P → P はステップ4とステップ3に適用されたモーダスポネンスから

Γ とH を合わせるとC が証明されるとし、 Γ がH → C を証明することを示したいとします。 Γ の前提 (繰り返しステップ) または公理である演繹の各ステップSに対して、公理 1 のS →( H → S )にモーダスポネンスを適用してH → Sを得ることができます。 ステップがH自体 (仮説ステップ) である場合は、定理スキーマを適用してH → Hを取得します。 ステップがAおよびA → Sにモーダスポネンスを適用した結果である場合は、まずこれらがH → AおよびH →( A → S )に変換されていることを確認し、次に公理 2 の ( H →( A → S ))→(( H → A )→( H → S )) を取り、モーダスポネンスを適用して ( H → A )→( H → S ) を取得し、次に再度H → Sを取得します。証明の最後には、要求どおりH → Cが得られますが、今度はHではなく Γ のみに依存します。したがって、演繹ステップはなくなり、 Hから導かれた結論であった前のステップに統合されます。

結果として得られる証明の複雑さを最小限に抑えるために、変換前に何らかの前処理を行う必要があります。H に実際に依存しないステップ (結論以外) は、仮説ステップの前に移動して 1 レベルインデントを解除する必要があります。また、結論ではない繰り返しなど、その他の不要なステップ (結論を得るために使用されない、またはバイパスできるステップ) は削除する必要があります。

変換中は、演繹の始め（H → Hステップの直後）に、公理 1 への modus ponens の適用をすべて行うと便利な場合があります。

モーダスポネンスを変換する際、A がHのスコープ外にある場合、公理 1、A →( H → A )、およびモーダスポネンスを適用してH → Aを取得する必要があります。同様に、A → S がHのスコープ外にある場合、公理 1、 ( A → S )→( H →( A → S ))、およびモーダスポネンスを適用してH →( A → S ) を取得します。モーダスポネンスのステップが結論でない限り、これら両方を実行する必要はありません。なぜなら、両方がスコープ外にある場合、モーダスポネンスはH の前に移動されているはずであり、したがってこれもスコープ外にあるはずであるからです。

カリー・ハワード対応の下では、演繹メタ定理の上記の変換プロセスは、ラムダ計算の用語から組合せ論理の用語への変換プロセスに類似しており、公理 1 は K コンビネータに対応し、公理 2 は S コンビネータに対応します。I コンビネータは定理スキーマP → Pに対応することに注意してください。

演繹定理を使った複雑な証明を演繹定理を使わない直線的な証明に変換しようとする場合、最初にこれらの定理を一度証明しておき、その後で変換に役立てるとおそらく役に立つでしょう。

${\displaystyle A\to A}$

仮説ステップの変換に役立ちます。

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

大前提が仮説に依存していない場合に、仮定法を変換するのに役立ち、公理 1 の使用を避けながら公理 2 を置き換えます。

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

小前提が仮説に依存していない場合に、仮定法を変換するのに役立ち、公理 1 の使用を避けながら公理 2 を置き換えます。

これら 2 つの定理は公理 2 の代わりに併用できますが、変換後の証明はより複雑になります。

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

${\displaystyle (A\to (A\to C))\to (A\to C)}$

パースの法則は演繹定理の結果ではありませんが、演繹定理と併用することで、他の方法では証明できない事柄を証明することができます。

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

これは、公理 2 の代わりに使用できる 2 つの定理のうちの 2 番目を取得するためにも使用できます。

ヒルベルト型の演繹的命題計算システムにおける演繹定理を証明する。^[7]

が、 となる式の集合、および となる式の集合であるとします。 を証明します。 ${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle B}$${\displaystyle \Delta \cup \{A\}\vdash B}$${\displaystyle \Delta \vdash A\to B}$

なので、からの証明が存在します。 この定理は、証明の長さnについて帰納法により証明します。 つまり、帰納法の仮定は、長さnまでのからの証明が存在する任意の、およびに対して、が成立するというものです。 ${\displaystyle \Delta \cup \{A\}\vdash B}$${\displaystyle B}$${\displaystyle \デルタ \cup \{A\}}$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle B}$${\displaystyle B}$${\displaystyle \デルタ \cup \{A\}}$${\displaystyle \Delta \vdash A\to B}$

n = 1の場合、 は公式の集合 のメンバーです。したがって、 の場合、単に となり、これはp → pから代入して導出でき、これは公理から導出でき、したがって も導出できます。または の場合、 となり、この場合は、代入により公理p → ( q → p ) から となり、したがって法則により となります。 ${\displaystyle B}$${\displaystyle \デルタ \cup \{A\}}$${\displaystyle B=A}$${\displaystyle A\to B}$${\displaystyle A\to A}$${\displaystyle \Delta \vdash A\to B}$${\displaystyle B}$${\displaystyle \Delta }$${\displaystyle \Delta \vdash B}$${\displaystyle \Delta \vdash B\to (A\to B)}$${\displaystyle \Delta \vdash A\to B}$

ここで、長さnまでの証明に対する帰納法の仮説を仮定し、長さn +1の証明でから証明可能な式があるとします。この場合、2 つの可能性があります。 ${\displaystyle B}$${\displaystyle \デルタ \cup \{A\}}$

1. ${\displaystyle B}$は式集合の要素です。この場合、n =1 の場合と同じように進めます。${\displaystyle \デルタ \cup \{A\}}$
2. ${\displaystyle B}$は、モーダスポネンスを使用して到達します。次に、およびを証明できるような公式Cがあり、次にモーダスポネンスを使用して を証明します。およびの証明は最大でnステップで、帰納法の仮定により、および が得られます。公理 ( p → ( q → r )) → (( p → q ) → ( p → r )) を代入すると、 となり 、モーダスポネンスを 2 回使用すると が得られます。${\displaystyle \デルタ \cup \{A\}}$${\displaystyle C}$${\displaystyle C\to B}$${\displaystyle B}$${\displaystyle C}$${\displaystyle C\to B}$${\displaystyle \Delta \vdash A\to C}$${\displaystyle \Delta \vdash A\to (C\to B)}$${\displaystyle \Delta \vdash (A\to (C\to B))\to ((A\to C)\to (A\to B))}$${\displaystyle \Delta \vdash A\to B}$

したがって、すべての場合において定理はn +1 にも当てはまり、帰納法によって演繹定理が証明されます。

演繹定理は、次の形式で 第一階論理でも有効です。

• T が理論であり、 F 、 GがFが 閉じた式、およびである場合、 となります。${\displaystyle T\cup \{F\}\vdash G}$${\displaystyle T\vdash F\rightarrow G}$

ここで、記号は「 の構文上の帰結である」という意味です。この演繹定理の証明が命題計算における演繹定理の証明とどのように異なるかを以下で示します。 ${\displaystyle \vdash }$

形式的証明の概念の最も一般的なバージョンには、命題計算の公理スキーム（または命題計算のすべてのトートロジーはそれ自体が公理スキームとして解釈されるべきであるという理解）に加えて、量指定子公理があり、また、可能性の法則に加えて、一般化規則として知られる推論のもう 1 つの規則、「 Kから、 ∀ vKを推論する」があります。

T ∪{ F }からのGの証明をTからのF → Gの証明に変換するには、命題論理の証明と同じように、公理であるか、または可能性の適用から生じるGの証明のステップを扱います。一般化の規則の適用から生じるステップは、次の量指定子公理によって扱われます (式Hで変数 vが自由でない場合は常に有効です)。

• (∀ v ( H → K ))→( H →∀ vK )。

この場合、F は閉じていると仮定されているので、H をFとすることができます。この公理により、 F → Kと一般化からF →∀ vK を演繹することができます。これは、 Gの証明で一般化の規則が何らかのKに適用されるときはいつでも必要なことです。

一階述語論理では、F が閉じた論理式であるという制約は、G を から演繹する際に F の自由変数が変化していないことを条件として緩和される。演繹において F の自由変数 v が変化した場合は、（回転式の添え字は v が変化したことを示す）と書き、演繹定理の対応する形式は となる。^[8]${\displaystyle T\cup \{F\}}$${\displaystyle T\cup \{F\}\vdash ^{v}G}$${\displaystyle T\vdash (\forall vF)\rightarrow G}$

自然演繹を公理形式の証明に変換する方法を説明するために、これをトートロジーQ →(( Q → R )→ Rに適用します。実際には、これが可能であることを知っていれば十分です。通常、より長い公理的証明の代わりに自然演繹形式を使用します。

まず、自然演繹のような方法を使用して証明を書きます。

• Q 1. 仮説
  • Q → R 2.仮説
  • R 3. モーダスポネンス 1,2
• ( Q → R )→ R 4. 2から3への演繹

• Q →(( Q → R )→ R ) 5. 1から4までの演繹 QED

次に、内部演繹を公理的な証明に変換します。

• ( Q → R )→( Q → R ) 1. 定理の図式 ( A → A )
• (( Q → R )→( Q → R ))→((( Q → R )→ Q )→(( Q → R )→ R )) 2. 公理 2
• (( Q → R )→ Q )→(( Q → R )→ R ) 3. 法則 1,2
• Q →(( Q → R )→ Q ) 4. 公理 1
  • Q 5. 仮説
  • ( Q → R )→ Q 6. 法則 5,4
  • ( Q → R )→ R 7. 法則 6,3
• Q →(( Q → R )→ R ) 8. 5から7への演繹 QED

3番目に、外部演繹を公理的な証明に変換します。

• ( Q → R )→( Q → R ) 1. 定理の図式 ( A → A )
• (( Q → R )→( Q → R ))→((( Q → R )→ Q )→(( Q → R )→ R )) 2. 公理 2
• (( Q → R )→ Q )→(( Q → R )→ R ) 3. 法則 1,2
• Q →(( Q → R )→ Q ) 4. 公理 1
• [(( Q → R )→ Q )→(( Q → R )→ R )]→[ Q →((( Q → R )→ Q )→(( Q → R )→ R ))] 5. 公理 1
• Q →((( Q → R )→ Q )→(( Q → R )→ R )) 6. 法則 3,5
• [ Q →((( Q → R )→ Q )→(( Q → R )→ R ))]→([ Q →(( Q → R )→ Q )]→[ Q →(( Q → R )→ R ))]) 7. 公理 2
• [ Q →(( Q → R )→ Q )]→[ Q →(( Q → R )→ R ))] 8. 法則 6,7
• Q →(( Q → R )→ R )) 9. 法則 4,8 QED

これら 3 つのステップは、 Curry-Howard 対応を使用して簡潔に述べることができます。

• まず、ラムダ計算では、関数f = λa. λb. baはq → ( q → r ) → rの型を持つ。
• 次に、 b 上のラムダ消去により、f = λa. si (ka)
• 3番目に、aのラムダ消去により、f = s (k (si)) k

• カット除去定理
• 条件付き証明
• カレー作り
• 命題計算
• ピアースの法則

• Carl Hewitt (2008)、「スケーラブルで堅牢、プライバシーに配慮したクライアントクラウドコンピューティングのためのORG」、IEEEインターネットコンピューティング、12 (5): 96–99、doi :10.1109/MIC.2008.107、S2CID  27828219。2008年9月/10月
• コーレンバッハ、ウルリッヒ（2008）、応用証明理論：証明の解釈と数学におけるその利用、Springer Monographs in Mathematics、ベルリン、ニューヨーク：Springer-Verlag、ISBN 978-3-540-77532-4、MR  2445721
• クリーネ、スティーブン・コール（2002）[1967]、数学論理学、ニューヨーク：ドーバー出版、ISBN 978-0-486-42533-7、MR  1950307
• ラウテンバーグ、ヴォルフガング（2010）、数学論理学の簡潔な入門（第3版）、ニューヨーク：シュプリンガーサイエンス+ビジネスメディア、doi：10.1007 / 978-1-4419-1221-3、ISBN 978-1-4419-1220-6。
• ショーンフィールド、ジョセフ・R. (2001) [1967]、数学論理学（第2版）、AKピーターズ、ISBN 978-1-56881-135-2

• Vilnis Detlovs と Karlis Podnieks による「Introduction to Mathematical Logic」は包括的なチュートリアルです。セクション 1.5 を参照してください。
• 「演繹定理」