論理的思考法/演繹的推論

提供: Internet Web School

UNIQ31f31bef162f62d9-MathJax-2-QINU2 による版
(差分) ←前の版 | 最新版 (差分) | 次の版→ (差分)

目次

[非表示]

演繹推論

演繹的推論は論理的思考の根幹である.


簡単な例を挙げる。

  • (1)人間の髪の毛の本数は100万本以下である.
  • (2)東京都民の人口は1200万人である.

これらの命題が正しければ

  • (3)東京都民のうち少なくとも2人は髪の毛の本数は同じである.


この命題の正しさを示すには背理法による.

命題(3)の否定が成り立つものとする。


命題(3)は厳密に書くと

　「東京都民A,Bがいて,A,Bは同一人物でなくかつA,Bの髪の毛の本数は同じ」

である．

このこの命題の否定は

  • (4)任意の東京都民A,Bについて,A,Bが同一人物でなければ　A,Bの髪の毛の本数は等しくない．

である.

ここでは(4)が正しいと仮定している．


東京都民一人一人にその人自身の髪の毛の本数によって背番号を振ることを考える. 例え ば毛の本数が0本の人には背番号0を，1000本の人には背番号1000を振る。


都民全員に付与した背番号は(4)の仮定により誰一人として同じものはなく, 一人一人に唯一の背番号が振られる.

「(1)人間の髪の毛の本数は100万本以下である.」が正しいとしているから 振られる番号は0番から100万まででの100万+1通りである.

都民全員に付与した背番号はそれぞれに唯一であるから 都民全員の数は100万人+１人である.

しかしこれは「(2)東京都民の人口は1200万人である.」に矛盾する.

この矛盾は 命題「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」

の否定が成り立つとしたことによっている.

従って「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」が正しい.


上記の　命題(1),(2)が正しければ命題(3)が正しいことを論証した過程は 論理の連鎖に依っている.命題(3)を否定した命題が正しいとして論理の連鎖を つくり,矛盾を導くことによって命題(3)の正しさを証明した.


演繹推論はこのように,正しいもとして与えられた命題から厳密な論理を 繰り返し適用することによって新たな命題を結論として導き出す.

この過程(証明)は,その論証の過程に出てくる命題やそれに施す論理的な推論を計算機によって処理できる形式化された記述で書けば,計算機によってその正しさを検証できる.それを形式化を行うかどうかは別として計算機による検証で正しさが認められるものでなければ完全な演繹推論とは言えない.


実際,以下は定理証明支援系のMizarによって上記の推論を記述したものである. Mizarのような定理証明支援系あるいは形式化証明検証システムでは,命題は全て記号列であり,三段論法その他の推論規則はそれらの複数の記号列を操作して 別の新たな記号列を構成する規則に過ぎない.証明は,前提となる命題(記号列)から出発して,目的の命題(記号列)に至る,推論規則により 生成された記号列の列にに過ぎない.


特に,A.I.　や　ICTの進歩など数学を含む科学技術の進歩の激流の中にある,科学工学の技術者はMizarのようなシステムの操作にも慣れ親しむことが必要になってくる.


UNIQde20ec43dadf287-pre-00000000-QINU

公理系と推論

論理式

「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.

ここでは，そのような扱いを「命題論理」によって説明する.

「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は 代数的な演算の変数とみなすことができる.　これを命題変数と呼ぶ.

命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.


その上で,一つの命題に,あるいは命題と命題をつなぐ「～でない」　「かつ」　「または」　「ならば」 などを命題を表す命題変数に作用する演算子とみなすことにする. それらをそれぞれUNIQde20ec43dadf287-MathJax-345-QINU および UNIQde20ec43dadf287-MathJax-346-QINU　UNIQde20ec43dadf287-MathJax-347-QINUで表す.

命題変数にこれらの演算子を作用させたものを論理式と呼ぶ.

論理式はこれを以下のように再帰的に定義する.


  • UNIQde20ec43dadf287-MathJax-348-QINU および UNIQde20ec43dadf287-MathJax-349-QINU は論理式である。
  • 個々の命題変数は論理式である。
  • UNIQde20ec43dadf287-MathJax-350-QINU が論理式ならば、UNIQde20ec43dadf287-MathJax-351-QINU も論理式である。
  • UNIQde20ec43dadf287-MathJax-352-QINU が論理式ならば、

UNIQde20ec43dadf287-MathJax-353-QINU は、いずれも論理式である。

  • 以上によって定まるものみが論理式である。


論理式の全体を UNIQde20ec43dadf287-MathJax-354-QINU と書くことにしよう。

UNIQde20ec43dadf287-MathJax-355-QINU の要素である論理式は、いずれもその論理式を表現としてもつ真理 関数と考えられる。任意の真理関数は、その独立変数がとり得る値のとり方 (UNIQde20ec43dadf287-MathJax-356-QINU 変数ならば UNIQde20ec43dadf287-MathJax-357-QINU 通り)の各々の場合について、有限回の操作でその 値(関数値)を決定できる。

UNIQde20ec43dadf287-MathJax-358-QINU の論理式の値(真理関数とみなした場合の関数値)が、(命題変数の 値のとり方のすべてに対して)つねに UNIQde20ec43dadf287-MathJax-359-QINU であるとき、そのような論理 式を{\gt 恒真論理式}(tautology)という。

公理系

公理系と呼ばれる UNIQde20ec43dadf287-MathJax-360-QINU の部分集合 UNIQde20ec43dadf287-MathJax-361-QINU と推論規則が適当に定めら れ、恒真論理式が UNIQde20ec43dadf287-MathJax-362-QINU から推論規則によって導けるような体系を、 命題論理の公理的体系、あるいは命題計算の体系という。

いろいろな公理的体系が知られているが、ここではヒルベルト(D. Hilbert) 流のものを挙げておこう。

以下、UNIQde20ec43dadf287-MathJax-363-QINU は任意の UNIQde20ec43dadf287-MathJax-364-QINU の要素とする。 公理系 A として、次の UNIQde20ec43dadf287-MathJax-365-QINU をとる。

  1. UNIQde20ec43dadf287-MathJax-366-QINU
  2. UNIQde20ec43dadf287-MathJax-367-QINU
  3. UNIQde20ec43dadf287-MathJax-368-QINU
  4. UNIQde20ec43dadf287-MathJax-369-QINU
  5. UNIQde20ec43dadf287-MathJax-370-QINU
  6. UNIQde20ec43dadf287-MathJax-371-QINU
  7. UNIQde20ec43dadf287-MathJax-372-QINU
  8. UNIQde20ec43dadf287-MathJax-373-QINU
  9. UNIQde20ec43dadf287-MathJax-374-QINU
  10. UNIQde20ec43dadf287-MathJax-375-QINU
  11. UNIQde20ec43dadf287-MathJax-376-QINU
  12. UNIQde20ec43dadf287-MathJax-377-QINU
  13. UNIQde20ec43dadf287-MathJax-378-QINU
  14. UNIQde20ec43dadf287-MathJax-379-QINU
  15. UNIQde20ec43dadf287-MathJax-380-QINU

推論規則は、次の三段論法(modus ponens)のみである。横線の上の論 理式から下の論理式が導かれることを表わす。

UNIQde20ec43dadf287-MathJax-381-QINU

証明可能性を定義する。すなわち、UNIQde20ec43dadf287-MathJax-382-QINU の要素である論理式のうち、 証明可能な論理式(provable formula)を次のように定める:

  • 公理系の各公理の形の論理式は証明可能である。
  • 論理式 UNIQde20ec43dadf287-MathJax-383-QINU と論理式 UNIQde20ec43dadf287-MathJax-384-QINU が証明可能ならば、(推論規則によって、)論理式 UNIQde20ec43dadf287-MathJax-385-QINU は証明可能である。
  • 以上によって定まるものだけが、証明可能な論理式である。

推論法則

証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば

UNIQde20ec43dadf287-MathJax-386-QINU が「証明」のとき各UNIQde20ec43dadf287-MathJax-387-QINUは

  • 公理系の各公理の形の論理式である。
  • 論理式UNIQde20ec43dadf287-MathJax-388-QINUの前に論理式UNIQde20ec43dadf287-MathJax-389-QINUとUNIQde20ec43dadf287-MathJax-390-QINUがありUNIQde20ec43dadf287-MathJax-391-QINUはUNIQde20ec43dadf287-MathJax-392-QINUの形をしている。


例えば、

UNIQde20ec43dadf287-MathJax-393-QINU

もっと具体的には

UNIQde20ec43dadf287-MathJax-394-QINU

は証明である。（証明可能な論理式を「定理」とか「命題」と呼ぶこともある。）

「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 と呼ぶ。（これ自身は公理系を定義するのに必須ではないが、それを操作する 上で便利な手続きをまとめたもの。）

推論法則

  • UNIQde20ec43dadf287-MathJax-395-QINU

UNIQde20ec43dadf287-MathJax-396-QINUが証明可能な論理式ならばUNIQde20ec43dadf287-MathJax-397-QINUも 証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)

  • UNIQde20ec43dadf287-MathJax-398-QINU

任意の論理式UNIQde20ec43dadf287-MathJax-399-QINUを用いて「添加」により

UNIQde20ec43dadf287-MathJax-400-QINU

が得られる。またUNIQde20ec43dadf287-MathJax-401-QINUであるから

UNIQde20ec43dadf287-MathJax-402-QINU

推論規則により、

UNIQde20ec43dadf287-MathJax-403-QINU

が得られる。ところでUNIQde20ec43dadf287-MathJax-404-QINUにより

UNIQde20ec43dadf287-MathJax-405-QINU

は公理（当然証明可能な論理式であるから） 結局

UNIQde20ec43dadf287-MathJax-406-QINU

は証明可能な論理式である。UNIQde20ec43dadf287-MathJax-407-QINU

またこれから直ちに


  • UNIQde20ec43dadf287-MathJax-408-QINU

が得られる。 同様に


  • UNIQde20ec43dadf287-MathJax-409-QINU

も得られる。さらに


  • UNIQde20ec43dadf287-MathJax-410-QINU

も得られる。


  • UNIQde20ec43dadf287-MathJax-411-QINU

これはUNIQde20ec43dadf287-MathJax-412-QINUより

UNIQde20ec43dadf287-MathJax-413-QINU

が得られ、これと

UNIQde20ec43dadf287-MathJax-414-QINU

から推論規則により、

UNIQde20ec43dadf287-MathJax-415-QINU

を得る。さらにこれと

UNIQde20ec43dadf287-MathJax-416-QINU

とから

UNIQde20ec43dadf287-MathJax-417-QINU

が得られることで示される。UNIQde20ec43dadf287-MathJax-418-QINU %% %% 同様に


  • UNIQde20ec43dadf287-MathJax-419-QINU

が得られる。これはまず、UNIQde20ec43dadf287-MathJax-420-QINUから


UNIQde20ec43dadf287-MathJax-421-QINU

これと

UNIQde20ec43dadf287-MathJax-422-QINU

から

UNIQde20ec43dadf287-MathJax-423-QINU

が得られ さらにUNIQde20ec43dadf287-MathJax-424-QINUの

UNIQde20ec43dadf287-MathJax-425-QINU

と前述の「推移」により

UNIQde20ec43dadf287-MathJax-426-QINU

が得られることで示される。UNIQde20ec43dadf287-MathJax-427-QINU

演繹定理

演繹定理

前述の公理系と推論規則のセットを UNIQde20ec43dadf287-MathJax-428-QINU と呼ぶことにしよう。（UNIQde20ec43dadf287-MathJax-429-QINU{\bf A}UNIQde20ec43dadf287-MathJax-430-QINU）

UNIQde20ec43dadf287-MathJax-431-QINUの論理式 UNIQde20ec43dadf287-MathJax-432-QINU が証明 可能であるとは、UNIQde20ec43dadf287-MathJax-433-QINU において、公理系 UNIQde20ec43dadf287-MathJax-434-QINU から UNIQde20ec43dadf287-MathJax-435-QINU が推論規 則によって導けることであるから、これを

UNIQde20ec43dadf287-MathJax-436-QINU

と書く。推論規則

UNIQde20ec43dadf287-MathJax-437-QINU

はこの表記法を用いると、

UNIQde20ec43dadf287-MathJax-438-QINU

と書くべきである。しかし、どの系で証明可能なのか明らかな場合は UNIQde20ec43dadf287-MathJax-439-QINUは省略することにする。


[演繹定理] 上の体系UNIQde20ec43dadf287-MathJax-440-QINUについてその公理系UNIQde20ec43dadf287-MathJax-441-QINUに論理式

UNIQde20ec43dadf287-MathJax-442-QINU

を追加してできる新たな系で 論理式UNIQde20ec43dadf287-MathJax-443-QINUが証明可能であるとき、このことを

UNIQde20ec43dadf287-MathJax-444-QINU

で表す。さらにこのとき：

UNIQde20ec43dadf287-MathJax-445-QINU

が成り立つ。

また、これを繰り返せば


UNIQde20ec43dadf287-MathJax-446-QINU



[演繹定理の証明]


体系UNIQde20ec43dadf287-MathJax-447-QINUについてその公理系UNIQde20ec43dadf287-MathJax-448-QINUに論理式

UNIQde20ec43dadf287-MathJax-449-QINU

を追加してできる新たな系をUNIQde20ec43dadf287-MathJax-450-QINUで表わす.


UNIQde20ec43dadf287-MathJax-451-QINU

ならば

UNIQde20ec43dadf287-MathJax-452-QINU

である.



体系UNIQde20ec43dadf287-MathJax-453-QINUについてその公理系UNIQde20ec43dadf287-MathJax-454-QINUに論理式

UNIQde20ec43dadf287-MathJax-455-QINU

を追加してできる系をUNIQde20ec43dadf287-MathJax-456-QINUで表す。


示すべきことは

UNIQde20ec43dadf287-MathJax-457-QINU

である。

UNIQde20ec43dadf287-MathJax-458-QINU

がUNIQde20ec43dadf287-MathJax-459-QINUでの「証明」とするとき、定義より 各UNIQde20ec43dadf287-MathJax-460-QINUは次のいずれかである。


  • UNIQde20ec43dadf287-MathJax-461-QINUはUNIQde20ec43dadf287-MathJax-462-QINUのうち１つで

ある。

  • UNIQde20ec43dadf287-MathJax-463-QINUは公理系UNIQde20ec43dadf287-MathJax-464-QINUの各公理の形の論理式である。
  • 論理式 UNIQde20ec43dadf287-MathJax-465-QINU の前に論理式 UNIQde20ec43dadf287-MathJax-466-QINUとUNIQde20ec43dadf287-MathJax-467-QINU

UNIQde20ec43dadf287-MathJax-468-QINUがあり、UNIQde20ec43dadf287-MathJax-469-QINUはUNIQde20ec43dadf287-MathJax-470-QINU の 形をしている。


そして、

UNIQde20ec43dadf287-MathJax-471-QINU

はUNIQde20ec43dadf287-MathJax-472-QINUでのUNIQde20ec43dadf287-MathJax-473-QINUを含む「証明」になる。



  • UNIQde20ec43dadf287-MathJax-474-QINUがUNIQde20ec43dadf287-MathJax-475-QINUのうち１つであれば、「添加」

UNIQde20ec43dadf287-MathJax-476-QINU

により、 UNIQde20ec43dadf287-MathJax-477-QINUはUNIQde20ec43dadf287-MathJax-478-QINUで証明可能な論理式になる。

UNIQde20ec43dadf287-MathJax-479-QINUがUNIQde20ec43dadf287-MathJax-480-QINU自身ならば、公理UNIQde20ec43dadf287-MathJax-481-QINU により、 UNIQde20ec43dadf287-MathJax-482-QINU はUNIQde20ec43dadf287-MathJax-483-QINUで証明可能な論理式である。

  • UNIQde20ec43dadf287-MathJax-484-QINUが公理系UNIQde20ec43dadf287-MathJax-485-QINUの各公理の形の論理式であるとき、

同様に「添加」により、 UNIQde20ec43dadf287-MathJax-486-QINUはUNIQde20ec43dadf287-MathJax-487-QINUで証明可能な論理式である。

  • 論理式 UNIQde20ec43dadf287-MathJax-488-QINU の前に論理式 UNIQde20ec43dadf287-MathJax-489-QINUとUNIQde20ec43dadf287-MathJax-490-QINU

UNIQde20ec43dadf287-MathJax-491-QINUがあり、UNIQde20ec43dadf287-MathJax-492-QINUはUNIQde20ec43dadf287-MathJax-493-QINU の 形をしているときは、 UNIQde20ec43dadf287-MathJax-494-QINUの前に、

UNIQde20ec43dadf287-MathJax-495-QINUとUNIQde20ec43dadf287-MathJax-496-QINUとがあることになる。

これに「複推移」

UNIQde20ec43dadf287-MathJax-497-QINU

を適用すると UNIQde20ec43dadf287-MathJax-498-QINUが得られる。UNIQde20ec43dadf287-MathJax-499-QINU

演繹定理の応用

  • UNIQde20ec43dadf287-MathJax-500-QINUのとき　UNIQde20ec43dadf287-MathJax-501-QINU


これは、まず

UNIQde20ec43dadf287-MathJax-502-QINU

から演繹定理により UNIQde20ec43dadf287-MathJax-503-QINU

これと公理(14)から

UNIQde20ec43dadf287-MathJax-504-QINU

となる。さらにUNIQde20ec43dadf287-MathJax-505-QINUにより、

UNIQde20ec43dadf287-MathJax-506-QINU

とUNIQde20ec43dadf287-MathJax-507-QINUから

UNIQde20ec43dadf287-MathJax-508-QINU

が得られる。また、UNIQde20ec43dadf287-MathJax-509-QINUにより

UNIQde20ec43dadf287-MathJax-510-QINU

が成り立っている。これらより結局

UNIQde20ec43dadf287-MathJax-511-QINU UNIQde20ec43dadf287-MathJax-512-QINU

上の結果を推論規則の形で表現すれば

UNIQde20ec43dadf287-MathJax-513-QINU


また論理式の形で表せば

UNIQde20ec43dadf287-MathJax-514-QINU

である。（いずれもUNIQde20ec43dadf287-MathJax-515-QINUが省略されていることに注意）


  • UNIQde20ec43dadf287-MathJax-516-QINU

まず、

UNIQde20ec43dadf287-MathJax-517-QINU

を仮定する。系UNIQde20ec43dadf287-MathJax-518-QINUにUNIQde20ec43dadf287-MathJax-519-QINUを追加して得られる系をUNIQde20ec43dadf287-MathJax-520-QINUとする。 さらにこれにUNIQde20ec43dadf287-MathJax-521-QINUの否定UNIQde20ec43dadf287-MathJax-522-QINUを追加した系をUNIQde20ec43dadf287-MathJax-523-QINUと すると、２重否定により、UNIQde20ec43dadf287-MathJax-524-QINUが、従って UNIQde20ec43dadf287-MathJax-525-QINUが得られる。このことから UNIQde20ec43dadf287-MathJax-526-QINUとなり、結局UNIQde20ec43dadf287-MathJax-527-QINUが得られる。UNIQde20ec43dadf287-MathJax-528-QINU

体系 UNIQde20ec43dadf287-MathJax-529-QINU については、次の事実が知られている:


  • 命題計算の体系についての完全性定理


UNIQde20ec43dadf287-MathJax-530-QINU が恒真論理式であることの必要十分条件は、UNIQde20ec43dadf287-MathJax-531-QINU が成立することである。UNIQde20ec43dadf287-MathJax-532-QINU

この定理は、命題計算の体系についての完全性定理(completeness theorem)と呼ばれるものである。

  • [証明]

まず、UNIQde20ec43dadf287-MathJax-533-QINUが成立すればUNIQde20ec43dadf287-MathJax-534-QINUが恒真論理式であることを示そう。

UNIQde20ec43dadf287-MathJax-535-QINUが成り立つとすると；

系UNIQde20ec43dadf287-MathJax-536-QINUの「証明」である論理式の列

UNIQde20ec43dadf287-MathJax-537-QINU

があって、UNIQde20ec43dadf287-MathJax-538-QINUは最後のUNIQde20ec43dadf287-MathJax-539-QINUと一致しているものとしてよい。 各UNIQde20ec43dadf287-MathJax-540-QINUは


  • 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3

であるからUNIQde20ec43dadf287-MathJax-541-QINUは恒真論理式である。

  • 論理式 UNIQde20ec43dadf287-MathJax-542-QINU の前に論理式 UNIQde20ec43dadf287-MathJax-543-QINUとUNIQde20ec43dadf287-MathJax-544-QINU

UNIQde20ec43dadf287-MathJax-545-QINUがあり、UNIQde20ec43dadf287-MathJax-546-QINUはUNIQde20ec43dadf287-MathJax-547-QINU の 形をしている。 UNIQde20ec43dadf287-MathJax-548-QINUより前の論理式は恒真論理式であると仮定すると、 UNIQde20ec43dadf287-MathJax-549-QINUとUNIQde20ec43dadf287-MathJax-550-QINUは真理値UNIQde20ec43dadf287-MathJax-551-QINUしかとらないから真理値表


UNIQde20ec43dadf287-MathJax-552-QINU UNIQde20ec43dadf287-MathJax-553-QINU UNIQde20ec43dadf287-MathJax-554-QINU
UNIQde20ec43dadf287-MathJax-555-QINU UNIQde20ec43dadf287-MathJax-556-QINU UNIQde20ec43dadf287-MathJax-557-QINU
UNIQde20ec43dadf287-MathJax-558-QINU UNIQde20ec43dadf287-MathJax-559-QINU UNIQde20ec43dadf287-MathJax-560-QINU
UNIQde20ec43dadf287-MathJax-561-QINU UNIQde20ec43dadf287-MathJax-562-QINU UNIQde20ec43dadf287-MathJax-563-QINU
UNIQde20ec43dadf287-MathJax-564-QINU UNIQde20ec43dadf287-MathJax-565-QINU UNIQde20ec43dadf287-MathJax-566-QINU


から明らかなようにUNIQde20ec43dadf287-MathJax-567-QINUの真理値はUNIQde20ec43dadf287-MathJax-568-QINUしか取り得ない。 すなわちUNIQde20ec43dadf287-MathJax-569-QINUは恒真論理式である。


逆にUNIQde20ec43dadf287-MathJax-570-QINUが恒真論理式であるときに、 UNIQde20ec43dadf287-MathJax-571-QINUが成立することをいうには次の補題１が必要になる。

  • [補題]

UNIQde20ec43dadf287-MathJax-572-QINUが命題変数UNIQde20ec43dadf287-MathJax-573-QINUから構成される論理式とする。 命題変数UNIQde20ec43dadf287-MathJax-574-QINUに真理値UNIQde20ec43dadf287-MathJax-575-QINUをふり当て、そのふり当てに対しUNIQde20ec43dadf287-MathJax-576-QINUの真理値がUNIQde20ec43dadf287-MathJax-577-QINUである場合

UNIQde20ec43dadf287-MathJax-578-QINU

UNIQde20ec43dadf287-MathJax-579-QINUの真理値がUNIQde20ec43dadf287-MathJax-580-QINUである場合

UNIQde20ec43dadf287-MathJax-581-QINU

である。ただし、UNIQde20ec43dadf287-MathJax-582-QINUはUNIQde20ec43dadf287-MathJax-583-QINUに対する真理値のふり当てがUNIQde20ec43dadf287-MathJax-584-QINUの場合UNIQde20ec43dadf287-MathJax-585-QINU、UNIQde20ec43dadf287-MathJax-586-QINUの場合はUNIQde20ec43dadf287-MathJax-587-QINUとする。UNIQde20ec43dadf287-MathJax-588-QINU

  • [定理の証明の続き]

恒真論理式UNIQde20ec43dadf287-MathJax-589-QINUが命題変数UNIQde20ec43dadf287-MathJax-590-QINUから構成されるものとする。 する。 命題変数UNIQde20ec43dadf287-MathJax-591-QINUに真理値UNIQde20ec43dadf287-MathJax-592-QINUどのようにふり当ても、 UNIQde20ec43dadf287-MathJax-593-QINUの真理値は常にUNIQde20ec43dadf287-MathJax-594-QINUである。

命題変数UNIQde20ec43dadf287-MathJax-595-QINUに真理値UNIQde20ec43dadf287-MathJax-596-QINUどのようにふり当てるしかたは UNIQde20ec43dadf287-MathJax-597-QINU通りある。これを辞書式順序で全て列挙し[補題１]を適用すると


UNIQde20ec43dadf287-MathJax-598-QINU


が得られる。最初の２式から演繹定理により

UNIQde20ec43dadf287-MathJax-599-QINU

これから

UNIQde20ec43dadf287-MathJax-600-QINU

が得られる。すなわちUNIQde20ec43dadf287-MathJax-601-QINUが消去された。同様にして順次に２式ずつ 同じ手順を繰り返せば、UNIQde20ec43dadf287-MathJax-602-QINUが消去されたUNIQde20ec43dadf287-MathJax-603-QINU個の式を得る。この UNIQde20ec43dadf287-MathJax-604-QINU個の式からUNIQde20ec43dadf287-MathJax-605-QINUを２式ずつをとり同じ手順を繰り返すとUNIQde20ec43dadf287-MathJax-606-QINUが 消去されたUNIQde20ec43dadf287-MathJax-607-QINU個の式を得る。 この手順を繰り返せば変数UNIQde20ec43dadf287-MathJax-608-QINUが全て消去され、結局

UNIQde20ec43dadf287-MathJax-609-QINU

を得る。UNIQde20ec43dadf287-MathJax-610-QINU

  • [補題の証明]
    • 論理式UNIQde20ec43dadf287-MathJax-611-QINUがただ１つの命題変数UNIQde20ec43dadf287-MathJax-612-QINUからなるとき

　　　　 UNIQde20ec43dadf287-MathJax-613-QINUに対するふり当てがUNIQde20ec43dadf287-MathJax-614-QINUのときUNIQde20ec43dadf287-MathJax-615-QINU　また　UNIQde20ec43dadf287-MathJax-616-QINUのとき UNIQde20ec43dadf287-MathJax-617-QINU これは公理のUNIQde20ec43dadf287-MathJax-618-QINUから容易に示される。

    • これ以外の場合は、UNIQde20ec43dadf287-MathJax-619-QINUはUNIQde20ec43dadf287-MathJax-620-QINUの形をしている。

そこで論理式の長さについての帰納法を使う.

UNIQde20ec43dadf287-MathJax-621-QINUより長さの短い部分式UNIQde20ec43dadf287-MathJax-622-QINUについてはこの補題が成り立つものとする。


      • UNIQde20ec43dadf287-MathJax-623-QINU がUNIQde20ec43dadf287-MathJax-624-QINUである場合


UNIQde20ec43dadf287-MathJax-625-QINUの値がUNIQde20ec43dadf287-MathJax-626-QINUのときUNIQde20ec43dadf287-MathJax-627-QINUの値はUNIQde20ec43dadf287-MathJax-628-QINUであるから

UNIQde20ec43dadf287-MathJax-629-QINU

UNIQde20ec43dadf287-MathJax-630-QINUの値がUNIQde20ec43dadf287-MathJax-631-QINUのときUNIQde20ec43dadf287-MathJax-632-QINUの値はUNIQde20ec43dadf287-MathJax-633-QINUであるから

UNIQde20ec43dadf287-MathJax-634-QINU

UNIQde20ec43dadf287-MathJax-635-QINUはそれぞれUNIQde20ec43dadf287-MathJax-636-QINU及びUNIQde20ec43dadf287-MathJax-637-QINUである。

      • UNIQde20ec43dadf287-MathJax-638-QINU がUNIQde20ec43dadf287-MathJax-639-QINUである場合

UNIQde20ec43dadf287-MathJax-640-QINUの値がUNIQde20ec43dadf287-MathJax-641-QINUのときUNIQde20ec43dadf287-MathJax-642-QINUの少なくともどちらか一方の値は UNIQde20ec43dadf287-MathJax-643-QINUであるから、UNIQde20ec43dadf287-MathJax-644-QINUの値がUNIQde20ec43dadf287-MathJax-645-QINUとしても一般性を失わない。このとき

UNIQde20ec43dadf287-MathJax-646-QINU

が成り立っている。これと公理のUNIQde20ec43dadf287-MathJax-647-QINU

UNIQde20ec43dadf287-MathJax-648-QINU

により UNIQde20ec43dadf287-MathJax-649-QINU

UNIQde20ec43dadf287-MathJax-650-QINUはUNIQde20ec43dadf287-MathJax-651-QINUに他ならない。

UNIQde20ec43dadf287-MathJax-652-QINUの値がUNIQde20ec43dadf287-MathJax-653-QINUのときUNIQde20ec43dadf287-MathJax-654-QINUの値はともにUNIQde20ec43dadf287-MathJax-655-QINUでなければならない。 このとき UNIQde20ec43dadf287-MathJax-656-QINU

UNIQde20ec43dadf287-MathJax-657-QINU

これに推論法則の「論理積」

UNIQde20ec43dadf287-MathJax-658-QINU

を用いて

UNIQde20ec43dadf287-MathJax-659-QINU を得る。

UNIQde20ec43dadf287-MathJax-660-QINUはUNIQde20ec43dadf287-MathJax-661-QINUに他ならない。


      • UNIQde20ec43dadf287-MathJax-662-QINU がUNIQde20ec43dadf287-MathJax-663-QINUである場合


UNIQde20ec43dadf287-MathJax-664-QINUの値がUNIQde20ec43dadf287-MathJax-665-QINUのときUNIQde20ec43dadf287-MathJax-666-QINUの値はともにUNIQde20ec43dadf287-MathJax-667-QINUでなければならない。 このとき

UNIQde20ec43dadf287-MathJax-668-QINU

UNIQde20ec43dadf287-MathJax-669-QINU

これに推論法則の「論理積」

UNIQde20ec43dadf287-MathJax-670-QINU

を用いて UNIQde20ec43dadf287-MathJax-671-QINU を得る。 UNIQde20ec43dadf287-MathJax-672-QINUはUNIQde20ec43dadf287-MathJax-673-QINUに他ならない。

UNIQde20ec43dadf287-MathJax-674-QINUの値がUNIQde20ec43dadf287-MathJax-675-QINUのときUNIQde20ec43dadf287-MathJax-676-QINUの少なくともどちらか一方の値は UNIQde20ec43dadf287-MathJax-677-QINUであるから、UNIQde20ec43dadf287-MathJax-678-QINUの値がUNIQde20ec43dadf287-MathJax-679-QINUとしても一般性を失わない。このとき

UNIQde20ec43dadf287-MathJax-680-QINU

が成り立っている。これと公理のUNIQde20ec43dadf287-MathJax-681-QINU

UNIQde20ec43dadf287-MathJax-682-QINU

により

UNIQde20ec43dadf287-MathJax-683-QINU

UNIQde20ec43dadf287-MathJax-684-QINUはUNIQde20ec43dadf287-MathJax-685-QINUに他ならない。 　UNIQde20ec43dadf287-MathJax-686-QINU

「http://ja.iwschool.org/wiki/%E8%AB%96%E7%90%86%E7%9A%84%E6%80%9D%E8%80%83%E6%B3%95/%E6%BC%94%E7%B9%B9%E7%9A%84%E6%8E%A8%E8%AB%96」より作成
個人用ツール