論理的思考法/演繹的推論
提供: Internet Web School
目次[非表示] |
演繹推論
演繹的推論は論理的思考の根幹である.
簡単な例を挙げる。
- (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のようなシステムの操作にも慣れ親しむことが必要になってくる.
公理系と推論
論理式
「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.
ここでは，そのような扱いを「命題論理」によって説明する.
「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は 代数的な演算の変数とみなすことができる. これを命題変数と呼ぶ.
命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.
その上で,一つの命題に,あるいは命題と命題をつなぐ「～でない」 「かつ」 「または」 「ならば」
などを命題を表す命題変数に作用する演算子とみなすことにする.
それらをそれぞれUNIQ6f94c5d86da6e4a5-MathJax-345-QINU および UNIQ6f94c5d86da6e4a5-MathJax-346-QINU UNIQ6f94c5d86da6e4a5-MathJax-347-QINUで表す.
命題変数にこれらの演算子を作用させたものを論理式と呼ぶ.
論理式はこれを以下のように再帰的に定義する.
- UNIQ6f94c5d86da6e4a5-MathJax-348-QINU および UNIQ6f94c5d86da6e4a5-MathJax-349-QINU は論理式である。
- 個々の命題変数は論理式である。
- UNIQ6f94c5d86da6e4a5-MathJax-350-QINU が論理式ならば、UNIQ6f94c5d86da6e4a5-MathJax-351-QINU も論理式である。
- UNIQ6f94c5d86da6e4a5-MathJax-352-QINU が論理式ならば、
UNIQ6f94c5d86da6e4a5-MathJax-353-QINU は、いずれも論理式である。
- 以上によって定まるものみが論理式である。
論理式の全体を UNIQ6f94c5d86da6e4a5-MathJax-354-QINU と書くことにしよう。
UNIQ6f94c5d86da6e4a5-MathJax-355-QINU の要素である論理式は、いずれもその論理式を表現としてもつ真理 関数と考えられる。任意の真理関数は、その独立変数がとり得る値のとり方 (UNIQ6f94c5d86da6e4a5-MathJax-356-QINU 変数ならば UNIQ6f94c5d86da6e4a5-MathJax-357-QINU 通り)の各々の場合について、有限回の操作でその 値(関数値)を決定できる。
UNIQ6f94c5d86da6e4a5-MathJax-358-QINU の論理式の値(真理関数とみなした場合の関数値)が、(命題変数の 値のとり方のすべてに対して)つねに UNIQ6f94c5d86da6e4a5-MathJax-359-QINU であるとき、そのような論理 式を{\gt 恒真論理式}(tautology)という。
公理系
公理系と呼ばれる UNIQ6f94c5d86da6e4a5-MathJax-360-QINU の部分集合 UNIQ6f94c5d86da6e4a5-MathJax-361-QINU と推論規則が適当に定めら れ、恒真論理式が UNIQ6f94c5d86da6e4a5-MathJax-362-QINU から推論規則によって導けるような体系を、 命題論理の公理的体系、あるいは命題計算の体系という。
いろいろな公理的体系が知られているが、ここではヒルベルト(D. Hilbert) 流のものを挙げておこう。
以下、UNIQ6f94c5d86da6e4a5-MathJax-363-QINU は任意の UNIQ6f94c5d86da6e4a5-MathJax-364-QINU の要素とする。 公理系 A として、次の UNIQ6f94c5d86da6e4a5-MathJax-365-QINU をとる。
- UNIQ6f94c5d86da6e4a5-MathJax-366-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-367-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-368-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-369-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-370-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-371-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-372-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-373-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-374-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-375-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-376-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-377-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-378-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-379-QINU
- UNIQ6f94c5d86da6e4a5-MathJax-380-QINU
推論規則は、次の三段論法(modus ponens)のみである。横線の上の論 理式から下の論理式が導かれることを表わす。
UNIQ6f94c5d86da6e4a5-MathJax-381-QINU
証明可能性を定義する。すなわち、UNIQ6f94c5d86da6e4a5-MathJax-382-QINU の要素である論理式のうち、 証明可能な論理式(provable formula)を次のように定める:
- 公理系の各公理の形の論理式は証明可能である。
- 論理式 UNIQ6f94c5d86da6e4a5-MathJax-383-QINU と論理式 UNIQ6f94c5d86da6e4a5-MathJax-384-QINU が証明可能ならば、(推論規則によって、)論理式 UNIQ6f94c5d86da6e4a5-MathJax-385-QINU は証明可能である。
- 以上によって定まるものだけが、証明可能な論理式である。
推論法則
証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば
UNIQ6f94c5d86da6e4a5-MathJax-386-QINU が「証明」のとき各UNIQ6f94c5d86da6e4a5-MathJax-387-QINUは
- 公理系の各公理の形の論理式である。
- 論理式UNIQ6f94c5d86da6e4a5-MathJax-388-QINUの前に論理式UNIQ6f94c5d86da6e4a5-MathJax-389-QINUとUNIQ6f94c5d86da6e4a5-MathJax-390-QINUがありUNIQ6f94c5d86da6e4a5-MathJax-391-QINUはUNIQ6f94c5d86da6e4a5-MathJax-392-QINUの形をしている。
例えば、
UNIQ6f94c5d86da6e4a5-MathJax-393-QINU
もっと具体的には
UNIQ6f94c5d86da6e4a5-MathJax-394-QINU
は証明である。（証明可能な論理式を「定理」とか「命題」と呼ぶこともある。）
「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 と呼ぶ。（これ自身は公理系を定義するのに必須ではないが、それを操作する 上で便利な手続きをまとめたもの。）
推論法則
- UNIQ6f94c5d86da6e4a5-MathJax-395-QINU
UNIQ6f94c5d86da6e4a5-MathJax-396-QINUが証明可能な論理式ならばUNIQ6f94c5d86da6e4a5-MathJax-397-QINUも 証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)
- UNIQ6f94c5d86da6e4a5-MathJax-398-QINU
任意の論理式UNIQ6f94c5d86da6e4a5-MathJax-399-QINUを用いて「添加」により
UNIQ6f94c5d86da6e4a5-MathJax-400-QINU
が得られる。またUNIQ6f94c5d86da6e4a5-MathJax-401-QINUであるから
UNIQ6f94c5d86da6e4a5-MathJax-402-QINU
推論規則により、
UNIQ6f94c5d86da6e4a5-MathJax-403-QINU
が得られる。ところでUNIQ6f94c5d86da6e4a5-MathJax-404-QINUにより
UNIQ6f94c5d86da6e4a5-MathJax-405-QINU
は公理（当然証明可能な論理式であるから） 結局
UNIQ6f94c5d86da6e4a5-MathJax-406-QINU
は証明可能な論理式である。UNIQ6f94c5d86da6e4a5-MathJax-407-QINU
またこれから直ちに
- UNIQ6f94c5d86da6e4a5-MathJax-408-QINU
が得られる。 同様に
- UNIQ6f94c5d86da6e4a5-MathJax-409-QINU
も得られる。さらに
- UNIQ6f94c5d86da6e4a5-MathJax-410-QINU
も得られる。
- UNIQ6f94c5d86da6e4a5-MathJax-411-QINU
これはUNIQ6f94c5d86da6e4a5-MathJax-412-QINUより
UNIQ6f94c5d86da6e4a5-MathJax-413-QINU
が得られ、これと
UNIQ6f94c5d86da6e4a5-MathJax-414-QINU
から推論規則により、
UNIQ6f94c5d86da6e4a5-MathJax-415-QINU
を得る。さらにこれと
UNIQ6f94c5d86da6e4a5-MathJax-416-QINU
とから
UNIQ6f94c5d86da6e4a5-MathJax-417-QINU
が得られることで示される。UNIQ6f94c5d86da6e4a5-MathJax-418-QINU %% %% 同様に
- UNIQ6f94c5d86da6e4a5-MathJax-419-QINU
が得られる。これはまず、UNIQ6f94c5d86da6e4a5-MathJax-420-QINUから
UNIQ6f94c5d86da6e4a5-MathJax-421-QINU
これと
UNIQ6f94c5d86da6e4a5-MathJax-422-QINU
から
UNIQ6f94c5d86da6e4a5-MathJax-423-QINU
が得られ さらにUNIQ6f94c5d86da6e4a5-MathJax-424-QINUの
UNIQ6f94c5d86da6e4a5-MathJax-425-QINU
と前述の「推移」により
UNIQ6f94c5d86da6e4a5-MathJax-426-QINU
が得られることで示される。UNIQ6f94c5d86da6e4a5-MathJax-427-QINU
演繹定理
演繹定理
前述の公理系と推論規則のセットを UNIQ6f94c5d86da6e4a5-MathJax-428-QINU と呼ぶことにしよう。（UNIQ6f94c5d86da6e4a5-MathJax-429-QINU{\bf A}UNIQ6f94c5d86da6e4a5-MathJax-430-QINU）
UNIQ6f94c5d86da6e4a5-MathJax-431-QINUの論理式 UNIQ6f94c5d86da6e4a5-MathJax-432-QINU が証明 可能であるとは、UNIQ6f94c5d86da6e4a5-MathJax-433-QINU において、公理系 UNIQ6f94c5d86da6e4a5-MathJax-434-QINU から UNIQ6f94c5d86da6e4a5-MathJax-435-QINU が推論規 則によって導けることであるから、これを
UNIQ6f94c5d86da6e4a5-MathJax-436-QINU
と書く。推論規則
UNIQ6f94c5d86da6e4a5-MathJax-437-QINU
はこの表記法を用いると、
UNIQ6f94c5d86da6e4a5-MathJax-438-QINU
と書くべきである。しかし、どの系で証明可能なのか明らかな場合は UNIQ6f94c5d86da6e4a5-MathJax-439-QINUは省略することにする。
[演繹定理]
上の体系UNIQ6f94c5d86da6e4a5-MathJax-440-QINUについてその公理系UNIQ6f94c5d86da6e4a5-MathJax-441-QINUに論理式
UNIQ6f94c5d86da6e4a5-MathJax-442-QINU
を追加してできる新たな系で 論理式UNIQ6f94c5d86da6e4a5-MathJax-443-QINUが証明可能であるとき、このことを
UNIQ6f94c5d86da6e4a5-MathJax-444-QINU
で表す。さらにこのとき：
UNIQ6f94c5d86da6e4a5-MathJax-445-QINU
が成り立つ。
また、これを繰り返せば
UNIQ6f94c5d86da6e4a5-MathJax-446-QINU
[演繹定理の証明]
体系UNIQ6f94c5d86da6e4a5-MathJax-447-QINUについてその公理系UNIQ6f94c5d86da6e4a5-MathJax-448-QINUに論理式
UNIQ6f94c5d86da6e4a5-MathJax-449-QINU
を追加してできる新たな系をUNIQ6f94c5d86da6e4a5-MathJax-450-QINUで表わす.
UNIQ6f94c5d86da6e4a5-MathJax-451-QINU
ならば
UNIQ6f94c5d86da6e4a5-MathJax-452-QINU
である.
体系UNIQ6f94c5d86da6e4a5-MathJax-453-QINUについてその公理系UNIQ6f94c5d86da6e4a5-MathJax-454-QINUに論理式
UNIQ6f94c5d86da6e4a5-MathJax-455-QINU
を追加してできる系をUNIQ6f94c5d86da6e4a5-MathJax-456-QINUで表す。
示すべきことは
UNIQ6f94c5d86da6e4a5-MathJax-457-QINU
である。
UNIQ6f94c5d86da6e4a5-MathJax-458-QINU
がUNIQ6f94c5d86da6e4a5-MathJax-459-QINUでの「証明」とするとき、定義より 各UNIQ6f94c5d86da6e4a5-MathJax-460-QINUは次のいずれかである。
- UNIQ6f94c5d86da6e4a5-MathJax-461-QINUはUNIQ6f94c5d86da6e4a5-MathJax-462-QINUのうち１つで
ある。
- UNIQ6f94c5d86da6e4a5-MathJax-463-QINUは公理系UNIQ6f94c5d86da6e4a5-MathJax-464-QINUの各公理の形の論理式である。
- 論理式 UNIQ6f94c5d86da6e4a5-MathJax-465-QINU の前に論理式 UNIQ6f94c5d86da6e4a5-MathJax-466-QINUとUNIQ6f94c5d86da6e4a5-MathJax-467-QINU
UNIQ6f94c5d86da6e4a5-MathJax-468-QINUがあり、UNIQ6f94c5d86da6e4a5-MathJax-469-QINUはUNIQ6f94c5d86da6e4a5-MathJax-470-QINU の 形をしている。
そして、
UNIQ6f94c5d86da6e4a5-MathJax-471-QINU
はUNIQ6f94c5d86da6e4a5-MathJax-472-QINUでのUNIQ6f94c5d86da6e4a5-MathJax-473-QINUを含む「証明」になる。
- UNIQ6f94c5d86da6e4a5-MathJax-474-QINUがUNIQ6f94c5d86da6e4a5-MathJax-475-QINUのうち１つであれば、「添加」
UNIQ6f94c5d86da6e4a5-MathJax-476-QINU
により、 UNIQ6f94c5d86da6e4a5-MathJax-477-QINUはUNIQ6f94c5d86da6e4a5-MathJax-478-QINUで証明可能な論理式になる。
UNIQ6f94c5d86da6e4a5-MathJax-479-QINUがUNIQ6f94c5d86da6e4a5-MathJax-480-QINU自身ならば、公理UNIQ6f94c5d86da6e4a5-MathJax-481-QINU により、 UNIQ6f94c5d86da6e4a5-MathJax-482-QINU はUNIQ6f94c5d86da6e4a5-MathJax-483-QINUで証明可能な論理式である。
- UNIQ6f94c5d86da6e4a5-MathJax-484-QINUが公理系UNIQ6f94c5d86da6e4a5-MathJax-485-QINUの各公理の形の論理式であるとき、
同様に「添加」により、 UNIQ6f94c5d86da6e4a5-MathJax-486-QINUはUNIQ6f94c5d86da6e4a5-MathJax-487-QINUで証明可能な論理式である。
- 論理式 UNIQ6f94c5d86da6e4a5-MathJax-488-QINU の前に論理式 UNIQ6f94c5d86da6e4a5-MathJax-489-QINUとUNIQ6f94c5d86da6e4a5-MathJax-490-QINU
UNIQ6f94c5d86da6e4a5-MathJax-491-QINUがあり、UNIQ6f94c5d86da6e4a5-MathJax-492-QINUはUNIQ6f94c5d86da6e4a5-MathJax-493-QINU の 形をしているときは、 UNIQ6f94c5d86da6e4a5-MathJax-494-QINUの前に、
UNIQ6f94c5d86da6e4a5-MathJax-495-QINUとUNIQ6f94c5d86da6e4a5-MathJax-496-QINUとがあることになる。
これに「複推移」
UNIQ6f94c5d86da6e4a5-MathJax-497-QINU
を適用すると UNIQ6f94c5d86da6e4a5-MathJax-498-QINUが得られる。UNIQ6f94c5d86da6e4a5-MathJax-499-QINU
演繹定理の応用
- UNIQ6f94c5d86da6e4a5-MathJax-500-QINUのとき UNIQ6f94c5d86da6e4a5-MathJax-501-QINU
これは、まず
UNIQ6f94c5d86da6e4a5-MathJax-502-QINU
から演繹定理により UNIQ6f94c5d86da6e4a5-MathJax-503-QINU
これと公理(14)から
UNIQ6f94c5d86da6e4a5-MathJax-504-QINU
となる。さらにUNIQ6f94c5d86da6e4a5-MathJax-505-QINUにより、
UNIQ6f94c5d86da6e4a5-MathJax-506-QINU
とUNIQ6f94c5d86da6e4a5-MathJax-507-QINUから
UNIQ6f94c5d86da6e4a5-MathJax-508-QINU
が得られる。また、UNIQ6f94c5d86da6e4a5-MathJax-509-QINUにより
UNIQ6f94c5d86da6e4a5-MathJax-510-QINU
が成り立っている。これらより結局
UNIQ6f94c5d86da6e4a5-MathJax-511-QINU UNIQ6f94c5d86da6e4a5-MathJax-512-QINU
上の結果を推論規則の形で表現すれば
UNIQ6f94c5d86da6e4a5-MathJax-513-QINU
また論理式の形で表せば
UNIQ6f94c5d86da6e4a5-MathJax-514-QINU
である。（いずれもUNIQ6f94c5d86da6e4a5-MathJax-515-QINUが省略されていることに注意）
- UNIQ6f94c5d86da6e4a5-MathJax-516-QINU
まず、
UNIQ6f94c5d86da6e4a5-MathJax-517-QINU
を仮定する。系UNIQ6f94c5d86da6e4a5-MathJax-518-QINUにUNIQ6f94c5d86da6e4a5-MathJax-519-QINUを追加して得られる系をUNIQ6f94c5d86da6e4a5-MathJax-520-QINUとする。 さらにこれにUNIQ6f94c5d86da6e4a5-MathJax-521-QINUの否定UNIQ6f94c5d86da6e4a5-MathJax-522-QINUを追加した系をUNIQ6f94c5d86da6e4a5-MathJax-523-QINUと すると、２重否定により、UNIQ6f94c5d86da6e4a5-MathJax-524-QINUが、従って UNIQ6f94c5d86da6e4a5-MathJax-525-QINUが得られる。このことから UNIQ6f94c5d86da6e4a5-MathJax-526-QINUとなり、結局UNIQ6f94c5d86da6e4a5-MathJax-527-QINUが得られる。UNIQ6f94c5d86da6e4a5-MathJax-528-QINU
体系 UNIQ6f94c5d86da6e4a5-MathJax-529-QINU については、次の事実が知られている:
- 命題計算の体系についての完全性定理
UNIQ6f94c5d86da6e4a5-MathJax-530-QINU が恒真論理式であることの必要十分条件は、UNIQ6f94c5d86da6e4a5-MathJax-531-QINU
が成立することである。UNIQ6f94c5d86da6e4a5-MathJax-532-QINU
この定理は、命題計算の体系についての完全性定理(completeness theorem)と呼ばれるものである。
- [証明]
まず、UNIQ6f94c5d86da6e4a5-MathJax-533-QINUが成立すればUNIQ6f94c5d86da6e4a5-MathJax-534-QINUが恒真論理式であることを示そう。
UNIQ6f94c5d86da6e4a5-MathJax-535-QINUが成り立つとすると；
系UNIQ6f94c5d86da6e4a5-MathJax-536-QINUの「証明」である論理式の列
UNIQ6f94c5d86da6e4a5-MathJax-537-QINU
があって、UNIQ6f94c5d86da6e4a5-MathJax-538-QINUは最後のUNIQ6f94c5d86da6e4a5-MathJax-539-QINUと一致しているものとしてよい。 各UNIQ6f94c5d86da6e4a5-MathJax-540-QINUは
- 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3
であるからUNIQ6f94c5d86da6e4a5-MathJax-541-QINUは恒真論理式である。
- 論理式 UNIQ6f94c5d86da6e4a5-MathJax-542-QINU の前に論理式 UNIQ6f94c5d86da6e4a5-MathJax-543-QINUとUNIQ6f94c5d86da6e4a5-MathJax-544-QINU
UNIQ6f94c5d86da6e4a5-MathJax-545-QINUがあり、UNIQ6f94c5d86da6e4a5-MathJax-546-QINUはUNIQ6f94c5d86da6e4a5-MathJax-547-QINU の 形をしている。 UNIQ6f94c5d86da6e4a5-MathJax-548-QINUより前の論理式は恒真論理式であると仮定すると、 UNIQ6f94c5d86da6e4a5-MathJax-549-QINUとUNIQ6f94c5d86da6e4a5-MathJax-550-QINUは真理値UNIQ6f94c5d86da6e4a5-MathJax-551-QINUしかとらないから真理値表
| UNIQ6f94c5d86da6e4a5-MathJax-552-QINU | UNIQ6f94c5d86da6e4a5-MathJax-553-QINU | UNIQ6f94c5d86da6e4a5-MathJax-554-QINU |
| UNIQ6f94c5d86da6e4a5-MathJax-555-QINU | UNIQ6f94c5d86da6e4a5-MathJax-556-QINU | UNIQ6f94c5d86da6e4a5-MathJax-557-QINU |
| UNIQ6f94c5d86da6e4a5-MathJax-558-QINU | UNIQ6f94c5d86da6e4a5-MathJax-559-QINU | UNIQ6f94c5d86da6e4a5-MathJax-560-QINU |
| UNIQ6f94c5d86da6e4a5-MathJax-561-QINU | UNIQ6f94c5d86da6e4a5-MathJax-562-QINU | UNIQ6f94c5d86da6e4a5-MathJax-563-QINU |
| UNIQ6f94c5d86da6e4a5-MathJax-564-QINU | UNIQ6f94c5d86da6e4a5-MathJax-565-QINU | UNIQ6f94c5d86da6e4a5-MathJax-566-QINU |
から明らかなようにUNIQ6f94c5d86da6e4a5-MathJax-567-QINUの真理値はUNIQ6f94c5d86da6e4a5-MathJax-568-QINUしか取り得ない。 すなわちUNIQ6f94c5d86da6e4a5-MathJax-569-QINUは恒真論理式である。
逆にUNIQ6f94c5d86da6e4a5-MathJax-570-QINUが恒真論理式であるときに、
UNIQ6f94c5d86da6e4a5-MathJax-571-QINUが成立することをいうには次の補題１が必要になる。
- [補題]
UNIQ6f94c5d86da6e4a5-MathJax-572-QINUが命題変数UNIQ6f94c5d86da6e4a5-MathJax-573-QINUから構成される論理式とする。 命題変数UNIQ6f94c5d86da6e4a5-MathJax-574-QINUに真理値UNIQ6f94c5d86da6e4a5-MathJax-575-QINUをふり当て、そのふり当てに対しUNIQ6f94c5d86da6e4a5-MathJax-576-QINUの真理値がUNIQ6f94c5d86da6e4a5-MathJax-577-QINUである場合
UNIQ6f94c5d86da6e4a5-MathJax-578-QINU
UNIQ6f94c5d86da6e4a5-MathJax-579-QINUの真理値がUNIQ6f94c5d86da6e4a5-MathJax-580-QINUである場合
UNIQ6f94c5d86da6e4a5-MathJax-581-QINU
である。ただし、UNIQ6f94c5d86da6e4a5-MathJax-582-QINUはUNIQ6f94c5d86da6e4a5-MathJax-583-QINUに対する真理値のふり当てがUNIQ6f94c5d86da6e4a5-MathJax-584-QINUの場合UNIQ6f94c5d86da6e4a5-MathJax-585-QINU、UNIQ6f94c5d86da6e4a5-MathJax-586-QINUの場合はUNIQ6f94c5d86da6e4a5-MathJax-587-QINUとする。UNIQ6f94c5d86da6e4a5-MathJax-588-QINU
- [定理の証明の続き]
恒真論理式UNIQ6f94c5d86da6e4a5-MathJax-589-QINUが命題変数UNIQ6f94c5d86da6e4a5-MathJax-590-QINUから構成されるものとする。 する。 命題変数UNIQ6f94c5d86da6e4a5-MathJax-591-QINUに真理値UNIQ6f94c5d86da6e4a5-MathJax-592-QINUどのようにふり当ても、 UNIQ6f94c5d86da6e4a5-MathJax-593-QINUの真理値は常にUNIQ6f94c5d86da6e4a5-MathJax-594-QINUである。
命題変数UNIQ6f94c5d86da6e4a5-MathJax-595-QINUに真理値UNIQ6f94c5d86da6e4a5-MathJax-596-QINUどのようにふり当てるしかたは UNIQ6f94c5d86da6e4a5-MathJax-597-QINU通りある。これを辞書式順序で全て列挙し[補題１]を適用すると
UNIQ6f94c5d86da6e4a5-MathJax-598-QINU
が得られる。最初の２式から演繹定理により
UNIQ6f94c5d86da6e4a5-MathJax-599-QINU
これから
UNIQ6f94c5d86da6e4a5-MathJax-600-QINU
が得られる。すなわちUNIQ6f94c5d86da6e4a5-MathJax-601-QINUが消去された。同様にして順次に２式ずつ 同じ手順を繰り返せば、UNIQ6f94c5d86da6e4a5-MathJax-602-QINUが消去されたUNIQ6f94c5d86da6e4a5-MathJax-603-QINU個の式を得る。この UNIQ6f94c5d86da6e4a5-MathJax-604-QINU個の式からUNIQ6f94c5d86da6e4a5-MathJax-605-QINUを２式ずつをとり同じ手順を繰り返すとUNIQ6f94c5d86da6e4a5-MathJax-606-QINUが 消去されたUNIQ6f94c5d86da6e4a5-MathJax-607-QINU個の式を得る。 この手順を繰り返せば変数UNIQ6f94c5d86da6e4a5-MathJax-608-QINUが全て消去され、結局
UNIQ6f94c5d86da6e4a5-MathJax-609-QINU
を得る。UNIQ6f94c5d86da6e4a5-MathJax-610-QINU
- [補題の証明]
- 論理式UNIQ6f94c5d86da6e4a5-MathJax-611-QINUがただ１つの命題変数UNIQ6f94c5d86da6e4a5-MathJax-612-QINUからなるとき
UNIQ6f94c5d86da6e4a5-MathJax-613-QINUに対するふり当てがUNIQ6f94c5d86da6e4a5-MathJax-614-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-615-QINU また UNIQ6f94c5d86da6e4a5-MathJax-616-QINUのとき UNIQ6f94c5d86da6e4a5-MathJax-617-QINU これは公理のUNIQ6f94c5d86da6e4a5-MathJax-618-QINUから容易に示される。
- これ以外の場合は、UNIQ6f94c5d86da6e4a5-MathJax-619-QINUはUNIQ6f94c5d86da6e4a5-MathJax-620-QINUの形をしている。
そこで論理式の長さについての帰納法を使う.
UNIQ6f94c5d86da6e4a5-MathJax-621-QINUより長さの短い部分式UNIQ6f94c5d86da6e4a5-MathJax-622-QINUについてはこの補題が成り立つものとする。
- UNIQ6f94c5d86da6e4a5-MathJax-623-QINU がUNIQ6f94c5d86da6e4a5-MathJax-624-QINUである場合
UNIQ6f94c5d86da6e4a5-MathJax-625-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-626-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-627-QINUの値はUNIQ6f94c5d86da6e4a5-MathJax-628-QINUであるから
UNIQ6f94c5d86da6e4a5-MathJax-629-QINU
UNIQ6f94c5d86da6e4a5-MathJax-630-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-631-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-632-QINUの値はUNIQ6f94c5d86da6e4a5-MathJax-633-QINUであるから
UNIQ6f94c5d86da6e4a5-MathJax-634-QINU
UNIQ6f94c5d86da6e4a5-MathJax-635-QINUはそれぞれUNIQ6f94c5d86da6e4a5-MathJax-636-QINU及びUNIQ6f94c5d86da6e4a5-MathJax-637-QINUである。
- UNIQ6f94c5d86da6e4a5-MathJax-638-QINU がUNIQ6f94c5d86da6e4a5-MathJax-639-QINUである場合
UNIQ6f94c5d86da6e4a5-MathJax-640-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-641-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-642-QINUの少なくともどちらか一方の値は UNIQ6f94c5d86da6e4a5-MathJax-643-QINUであるから、UNIQ6f94c5d86da6e4a5-MathJax-644-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-645-QINUとしても一般性を失わない。このとき
UNIQ6f94c5d86da6e4a5-MathJax-646-QINU
が成り立っている。これと公理のUNIQ6f94c5d86da6e4a5-MathJax-647-QINU
UNIQ6f94c5d86da6e4a5-MathJax-648-QINU
により UNIQ6f94c5d86da6e4a5-MathJax-649-QINU
UNIQ6f94c5d86da6e4a5-MathJax-650-QINUはUNIQ6f94c5d86da6e4a5-MathJax-651-QINUに他ならない。
UNIQ6f94c5d86da6e4a5-MathJax-652-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-653-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-654-QINUの値はともにUNIQ6f94c5d86da6e4a5-MathJax-655-QINUでなければならない。 このとき UNIQ6f94c5d86da6e4a5-MathJax-656-QINU
UNIQ6f94c5d86da6e4a5-MathJax-657-QINU
これに推論法則の「論理積」
UNIQ6f94c5d86da6e4a5-MathJax-658-QINU
を用いて
UNIQ6f94c5d86da6e4a5-MathJax-659-QINU を得る。
UNIQ6f94c5d86da6e4a5-MathJax-660-QINUはUNIQ6f94c5d86da6e4a5-MathJax-661-QINUに他ならない。
- UNIQ6f94c5d86da6e4a5-MathJax-662-QINU がUNIQ6f94c5d86da6e4a5-MathJax-663-QINUである場合
UNIQ6f94c5d86da6e4a5-MathJax-664-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-665-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-666-QINUの値はともにUNIQ6f94c5d86da6e4a5-MathJax-667-QINUでなければならない。
このとき
UNIQ6f94c5d86da6e4a5-MathJax-668-QINU
UNIQ6f94c5d86da6e4a5-MathJax-669-QINU
これに推論法則の「論理積」
UNIQ6f94c5d86da6e4a5-MathJax-670-QINU
を用いて UNIQ6f94c5d86da6e4a5-MathJax-671-QINU を得る。 UNIQ6f94c5d86da6e4a5-MathJax-672-QINUはUNIQ6f94c5d86da6e4a5-MathJax-673-QINUに他ならない。
UNIQ6f94c5d86da6e4a5-MathJax-674-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-675-QINUのときUNIQ6f94c5d86da6e4a5-MathJax-676-QINUの少なくともどちらか一方の値は UNIQ6f94c5d86da6e4a5-MathJax-677-QINUであるから、UNIQ6f94c5d86da6e4a5-MathJax-678-QINUの値がUNIQ6f94c5d86da6e4a5-MathJax-679-QINUとしても一般性を失わない。このとき
UNIQ6f94c5d86da6e4a5-MathJax-680-QINU
が成り立っている。これと公理のUNIQ6f94c5d86da6e4a5-MathJax-681-QINU
UNIQ6f94c5d86da6e4a5-MathJax-682-QINU
により
UNIQ6f94c5d86da6e4a5-MathJax-683-QINU
UNIQ6f94c5d86da6e4a5-MathJax-684-QINUはUNIQ6f94c5d86da6e4a5-MathJax-685-QINUに他ならない。 UNIQ6f94c5d86da6e4a5-MathJax-686-QINU
