論理的思考法/演繹的推論
提供: Internet Web School
(→演繹定理の応用) |
|||
(間の88版分が非表示) | |||
1 行: | 1 行: | ||
+ | =演繹推論= | ||
+ | |||
+ | |||
[https://ja.wikipedia.org/wiki/%E6%BC%94%E7%B9%B9 演繹的推論]は論理的思考の根幹である. | [https://ja.wikipedia.org/wiki/%E6%BC%94%E7%B9%B9 演繹的推論]は論理的思考の根幹である. | ||
55 行: | 58 行: | ||
の否定が成り立つとしたことによっている. | の否定が成り立つとしたことによっている. | ||
- | + | 従って「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」が正しい. | |
61 行: | 64 行: | ||
上記の 命題(1),(2)が正しければ命題(3)が正しいことを論証した過程は | 上記の 命題(1),(2)が正しければ命題(3)が正しいことを論証した過程は | ||
論理の連鎖に依っている.命題(3)を否定した命題が正しいとして論理の連鎖を | 論理の連鎖に依っている.命題(3)を否定した命題が正しいとして論理の連鎖を | ||
- | つくり, | + | つくり,矛盾を導くことによって命題(3)の正しさを証明した. |
67 行: | 70 行: | ||
繰り返し適用することによって新たな命題を結論として導き出す. | 繰り返し適用することによって新たな命題を結論として導き出す. | ||
- | この過程(証明)は,その論証の過程に出てくる命題やそれに施す論理的な推論を計算機によって処理できる形式化された記述で書けば,計算機によってその正しさを検証できる. | + | この過程(証明)は,その論証の過程に出てくる命題やそれに施す論理的な推論を計算機によって処理できる形式化された記述で書けば,計算機によってその正しさを検証できる.それを形式化を行うかどうかは別として計算機による検証で正しさが認められるものでなければ完全な演繹推論とは言えない. |
79 行: | 82 行: | ||
- | < | + | <pre style="font-size:large"> |
+ | environ | ||
+ | vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3, | ||
+ | RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4, | ||
+ | TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0, | ||
+ | UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0; | ||
+ | notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS, | ||
+ | XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1, | ||
+ | FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1, | ||
+ | TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY; | ||
+ | constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1, | ||
+ | BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1; | ||
+ | registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, | ||
+ | XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1, | ||
+ | XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY, | ||
+ | XREAL_0, RVSUM_1; | ||
+ | requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE; | ||
+ | definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, | ||
+ | PRE_POLY,FINSET_1,CARD_1; | ||
+ | theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1, | ||
+ | INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1, | ||
+ | FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1, | ||
+ | FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2, | ||
+ | FINSET_1,PARTFUN1, PRE_POLY, CARD_1; | ||
+ | schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1; | ||
+ | |||
+ | begin | ||
now | now | ||
let | let | ||
- | Humankind be finite set, | + | Humankind be finite set, |
- | + | ||
Tokyoite be Subset of Humankind, | Tokyoite be Subset of Humankind, | ||
Numberofhair be Function of Tokyoite,NAT ; | Numberofhair be Function of Tokyoite,NAT ; | ||
205 行: | 233 行: | ||
end; | end; | ||
end; | end; | ||
- | |||
+ | </pre> | ||
+ | |||
+ | =公理系と推論= | ||
+ | ==論理式== | ||
+ | 「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる. | ||
+ | |||
+ | ここでは,そのような扱いを「命題論理」によって説明する. | ||
+ | |||
+ | 「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は | ||
+ | 代数的な演算の変数とみなすことができる. これを命題変数と呼ぶ. | ||
+ | |||
+ | 命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる. | ||
+ | |||
+ | |||
+ | その上で,一つの命題に,あるいは命題と命題をつなぐ「~でない」 「かつ」 「または」 「ならば」 | ||
+ | などを命題を表す命題変数に作用する演算子とみなすことにする. | ||
+ | それらをそれぞれ⊤ および ⊥ ¬,∧,∨,⇒で表す. | ||
+ | |||
+ | 命題変数にこれらの演算子を作用させたものを論理式と呼ぶ. | ||
+ | |||
+ | 論理式はこれを以下のように再帰的に定義する. | ||
+ | |||
+ | |||
+ | * ⊤ および ⊥ は論理式である。 | ||
+ | |||
+ | * 個々の命題変数は論理式である。 | ||
+ | |||
+ | * A が論理式ならば、¬A も論理式である。 | ||
+ | |||
+ | * A,B が論理式ならば、 | ||
+ | A∧B,A∨B,A⇒B | ||
+ | は、いずれも論理式である。 | ||
+ | |||
+ | *以上によって定まるものみが論理式である。 | ||
+ | |||
+ | |||
+ | 論理式の全体を L と書くことにしよう。 | ||
+ | |||
+ | L の要素である論理式は、いずれもその論理式を表現としてもつ真理 | ||
+ | 関数と考えられる。任意の真理関数は、その独立変数がとり得る値のとり方 | ||
+ | (n 変数ならば 2n 通り)の各々の場合について、有限回の操作でその | ||
+ | 値(関数値)を決定できる。 | ||
+ | |||
+ | L の論理式の値(真理関数とみなした場合の関数値)が、(命題変数の | ||
+ | 値のとり方のすべてに対して)つねに ⊤ であるとき、そのような論理 | ||
+ | 式を{\gt 恒真論理式}(tautology)という。 | ||
+ | |||
+ | ==公理系== | ||
+ | |||
+ | 公理系と呼ばれる L の部分集合 A と推論規則が適当に定めら | ||
+ | れ、恒真論理式が A から推論規則によって導けるような体系を、 | ||
+ | '''命題論理の公理的体系'''、あるいは'''命題計算の体系'''という。 | ||
+ | |||
+ | いろいろな公理的体系が知られているが、ここではヒルベルト(D. Hilbert) | ||
+ | 流のものを挙げておこう。 | ||
+ | |||
+ | 以下、A,B,C は任意の L の要素とする。 | ||
+ | '''公理系 A''' として、次の (1)∼(15) をとる。 | ||
+ | |||
+ | # A⇒A | ||
+ | # $\cal (A \Rightarrow B) | ||
+ | \Rightarrow [(B \Rightarrow C) \Rightarrow (A \Rightarrow C)]$ | ||
+ | # A⇒(A∨B) | ||
+ | # B⇒(A∨B) | ||
+ | # $\cal (A \Rightarrow C) | ||
+ | \Rightarrow \{ (B \Rightarrow C) | ||
+ | \Rightarrow [(A \lor B) \Rightarrow C]\}$ | ||
+ | # (A∧B)⇒A | ||
+ | # (A∧B)⇒B | ||
+ | # $\cal (C \Rightarrow A) | ||
+ | \Rightarrow \{ (C \Rightarrow B) | ||
+ | \Rightarrow [C \Rightarrow (A \land B)]\}$ | ||
+ | # [A∧(A⇒B)]⇒B | ||
+ | # $\cal [(A \land C) \Rightarrow B] | ||
+ | \Rightarrow [C \Rightarrow (A \Rightarrow B)]$ | ||
+ | # (A∧¬A)⇒⊥ | ||
+ | # $\cal [(A \land B) \Rightarrow \bot ] | ||
+ | \Rightarrow (B \Rightarrow \neg A)$ | ||
+ | # A⇒⊤ | ||
+ | # ⊥⇒A | ||
+ | # A∨¬A | ||
+ | |||
+ | '''推論規則'''は、次の三段論法(modus ponens)のみである。横線の上の論 | ||
+ | 理式から下の論理式が導かれることを表わす。 | ||
+ | |||
+ | $ | ||
+ | \frac{\cal A \quad A \Rightarrow B}{\cal B} | ||
+ | $ | ||
+ | |||
+ | 証明可能性を定義する。すなわち、L の要素である論理式のうち、 | ||
+ | '''証明可能な論理式'''(provable formula)を次のように定める: | ||
+ | |||
+ | * 公理系の各公理の形の論理式は証明可能である。 | ||
+ | * 論理式 A と論理式 A⇒B が証明可能ならば、(推論規則によって、)論理式 B は証明可能である。 | ||
+ | * 以上によって定まるものだけが、証明可能な論理式である。 | ||
+ | |||
+ | ==推論法則== | ||
+ | |||
+ | 証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n | ||
+ | $ | ||
+ | が「証明」のとき各Aiは | ||
+ | *公理系の各公理の形の論理式である。 | ||
+ | *論理式Aiの前に論理式AjとAk(j,k<i)がありAkはAj⇒Aiの形をしている。 | ||
+ | |||
+ | |||
+ | 例えば、 | ||
+ | |||
+ | $ | ||
+ | \cal B \land \cal A \Rightarrow A , | ||
+ | \quad (\cal B \land \cal A \Rightarrow \cal A) | ||
+ | \Rightarrow (\cal A \Rightarrow (\cal B \Rightarrow \cal A)), \quad \cal A \Rightarrow (\cal B \Rightarrow \cal A) | ||
+ | $ | ||
+ | |||
+ | もっと具体的には | ||
+ | |||
+ | $1=2 \land 2> 6 \Rightarrow 2>6 \\ | ||
+ | ( 1=2 \land 2>6 \Rightarrow 2>6) \Rightarrow (2>6 \Rightarrow (1=2 \Rightarrow 2>6)) \\ | ||
+ | 2>6 \Rightarrow ( 1=2 \Rightarrow 2>6) | ||
+ | $ | ||
+ | |||
+ | は証明である。(証明可能な論理式を「定理」とか「命題」と呼ぶこともある。) | ||
+ | |||
+ | 「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 | ||
+ | と呼ぶ。(これ自身は公理系を定義するのに必須ではないが、それを操作する | ||
+ | 上で便利な手続きをまとめたもの。) | ||
+ | |||
+ | '''推論法則''' | ||
+ | *$ | ||
+ | \frac{\cal A }{\cal B \Rightarrow A} | ||
+ | \qquad (推論法則:添加) | ||
+ | $ | ||
+ | |||
+ | Aが証明可能な論理式ならばB⇒Aも | ||
+ | 証明可能な論理式であることを表す。 (上の「証明」の例に現れている。) | ||
+ | |||
+ | *$ | ||
+ | \frac{\cal A,B }{\cal A \land B} | ||
+ | \qquad (推論法則:論理積) | ||
+ | $ | ||
+ | |||
+ | 任意の論理式Cを用いて「添加」により | ||
+ | |||
+ | $ | ||
+ | \cal (C \lor \lnot C ) \Rightarrow A,(C \lor \lnot C ) \Rightarrow B | ||
+ | $ | ||
+ | |||
+ | が得られる。また(8)であるから | ||
+ | |||
+ | $ | ||
+ | \cal \{ (C \lor \lnot C) \Rightarrow A \} | ||
+ | \Rightarrow | ||
+ | [ \{ (C \lor \lnot C) \Rightarrow B \} \Rightarrow | ||
+ | \{ (C \lor \lnot C) \Rightarrow (A \land B ) \} ] | ||
+ | $ | ||
+ | |||
+ | 推論規則により、 | ||
+ | |||
+ | $ | ||
+ | \cal (C \lor \lnot C) \Rightarrow (A \land B ) | ||
+ | $ | ||
+ | |||
+ | が得られる。ところで(15)により | ||
+ | |||
+ | $ | ||
+ | \cal C \lor \lnot C | ||
+ | $ | ||
+ | |||
+ | は公理(当然証明可能な論理式であるから) | ||
+ | 結局 | ||
+ | |||
+ | $ | ||
+ | \cal A \land B | ||
+ | $ | ||
+ | |||
+ | は証明可能な論理式である。◻ | ||
+ | |||
+ | またこれから直ちに | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \frac{\cal A \land B }{\cal B \land A} | ||
+ | \qquad (推論法則:交換) | ||
+ | $ | ||
+ | |||
+ | が得られる。 | ||
+ | 同様に | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \frac{\cal A \lor B }{\cal B \lor A} | ||
+ | \qquad (推論法則:交換) | ||
+ | $ | ||
+ | |||
+ | も得られる。さらに | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \cal A \Rightarrow \lnot \lnot A,\lnot \lnot A \Rightarrow A | ||
+ | (推論法則:2重否定) | ||
+ | $ | ||
+ | |||
+ | も得られる。 | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \frac{ \cal A \Rightarrow B ,B \Rightarrow C } | ||
+ | {\cal A \Rightarrow C}(推論法則:推移) | ||
+ | $ | ||
+ | |||
+ | これは(2)より | ||
+ | |||
+ | $ | ||
+ | \cal (A \Rightarrow B) \Rightarrow | ||
+ | [(B \Rightarrow C ) \Rightarrow (A \Rightarrow C) ] | ||
+ | $ | ||
+ | |||
+ | が得られ、これと | ||
+ | |||
+ | $ | ||
+ | \cal A \Rightarrow B | ||
+ | $ | ||
+ | |||
+ | から推論規則により、 | ||
+ | |||
+ | $ | ||
+ | \cal (B \Rightarrow C ) \Rightarrow (A \Rightarrow C) | ||
+ | $ | ||
+ | |||
+ | を得る。さらにこれと | ||
+ | |||
+ | $ | ||
+ | \cal B \Rightarrow C | ||
+ | $ | ||
+ | |||
+ | とから | ||
+ | |||
+ | $ | ||
+ | \cal A \Rightarrow C | ||
+ | $ | ||
+ | |||
+ | が得られることで示される。◻ | ||
+ | %% | ||
+ | %% | ||
+ | 同様に | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } | ||
+ | {\cal A \Rightarrow C} (推論法則:復推移) | ||
+ | $ | ||
+ | |||
+ | が得られる。これはまず、(8)から | ||
+ | |||
+ | |||
+ | $ | ||
+ | \cal (A \Rightarrow B) \Rightarrow [ \{ A \Rightarrow (B \Rightarrow C) \} | ||
+ | \Rightarrow \{A \Rightarrow B \land (B \Rightarrow C) \} ] | ||
+ | $ | ||
+ | |||
+ | これと | ||
+ | |||
+ | $ | ||
+ | {\cal A \Rightarrow (B \Rightarrow C) , A \Rightarrow B} | ||
+ | $ | ||
+ | |||
+ | から | ||
+ | |||
+ | $ | ||
+ | {\cal A \Rightarrow \{ B \land (B \Rightarrow C) \} } | ||
+ | $ | ||
+ | |||
+ | が得られ | ||
+ | さらに(9)の | ||
+ | |||
+ | $ | ||
+ | {\cal \{B \land (B \Rightarrow C)\} \Rightarrow C } | ||
+ | $ | ||
+ | |||
+ | と前述の「推移」により | ||
+ | |||
+ | $ | ||
+ | \cal A \Rightarrow C | ||
+ | $ | ||
+ | |||
+ | が得られることで示される。◻ | ||
+ | |||
+ | ==演繹定理== | ||
+ | |||
+ | |||
+ | |||
+ | ===演繹定理=== | ||
+ | 前述の公理系と推論規則のセットを H と呼ぶことにしよう。(H=公理系{\bf A}+「推論規則」) | ||
+ | |||
+ | Lの論理式 A が証明 | ||
+ | 可能であるとは、H において、公理系 A から A が推論規 | ||
+ | 則によって導けることであるから、これを | ||
+ | |||
+ | $ | ||
+ | \vdash_H \cal A | ||
+ | $ | ||
+ | |||
+ | と書く。推論規則 | ||
+ | |||
+ | $ | ||
+ | \frac{\cal A \quad A \Rightarrow B}{\cal B} | ||
+ | $ | ||
+ | |||
+ | はこの表記法を用いると、 | ||
+ | |||
+ | $ | ||
+ | \frac{\vdash_H \cal A \quad \vdash_H A \Rightarrow B}{\vdash_H \cal B} | ||
+ | $ | ||
+ | |||
+ | と書くべきである。しかし、どの系で証明可能なのか明らかな場合は | ||
+ | ⊢Hは省略することにする。 | ||
+ | |||
+ | |||
+ | '''[演繹定理]''' | ||
+ | 上の体系Hについてその公理系Aに論理式 | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n | ||
+ | $ | ||
+ | |||
+ | を追加してできる新たな系で | ||
+ | 論理式Bが証明可能であるとき、このことを | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B | ||
+ | $ | ||
+ | |||
+ | で表す。さらにこのとき: | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-1} \vdash_H {\cal A}_n \Rightarrow {\cal B} | ||
+ | $ | ||
+ | |||
+ | が成り立つ。 | ||
+ | |||
+ | また、これを繰り返せば | ||
+ | |||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A} _{n-2} | ||
+ | \vdash_H {\cal A} _{n-1} \Rightarrow ({\cal A}_n \Rightarrow {\cal B}) | ||
+ | $ | ||
+ | |||
+ | |||
+ | |||
+ | |||
+ | '''[演繹定理の証明]''' | ||
+ | |||
+ | |||
+ | 体系Hについてその公理系Aに論理式 | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n | ||
+ | $ | ||
+ | |||
+ | を追加してできる新たな系をH1で表わす. | ||
+ | |||
+ | |||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B | ||
+ | $ | ||
+ | |||
+ | ならば | ||
+ | |||
+ | $ | ||
+ | \vdash_{H^1} \cal B | ||
+ | $ | ||
+ | |||
+ | である. | ||
+ | |||
+ | |||
+ | |||
+ | |||
+ | |||
+ | 体系Hについてその公理系Aに論理式 | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2,\cdots,{\cal A}_{n-1} | ||
+ | $ | ||
+ | |||
+ | を追加してできる系をH2で表す。 | ||
+ | |||
+ | |||
+ | |||
+ | 示すべきことは | ||
+ | |||
+ | $ | ||
+ | \vdash_{H^2} {\cal A}_n \Rightarrow \cal B | ||
+ | $ | ||
+ | |||
+ | である。 | ||
+ | |||
+ | $ | ||
+ | {\cal B}_1,{\cal B}_2, \cdots,{\cal B}_{n-1},{\cal B}_n(={\cal B}) | ||
+ | $ | ||
+ | |||
+ | がH1での「証明」とするとき、定義より | ||
+ | 各Biは次のいずれかである。 | ||
+ | |||
+ | |||
+ | * BiはA1,A2,⋯,Anのうち1つで | ||
+ | ある。 | ||
+ | * Biは公理系Hの各公理の形の論理式である。 | ||
+ | * 論理式 Bi の前に論理式 BjとBk | ||
+ | (j,k<i)があり、BkはBj⇒Bi の | ||
+ | 形をしている。 | ||
+ | |||
+ | |||
+ | そして、 | ||
+ | |||
+ | $ | ||
+ | {\cal A}_n \Rightarrow {\cal B}_1,{\cal A}_n \Rightarrow {\cal B}_2, \cdots,{\cal A}_n \Rightarrow {\cal B}_{n-1},{\cal A}_n \Rightarrow {\cal B}_n | ||
+ | $ | ||
+ | |||
+ | はH2でのAn⇒Bを含む「証明」になる。 | ||
+ | |||
+ | |||
+ | |||
+ | |||
+ | * BiがA1,A2,⋯,An−1のうち1つであれば、「添加」 | ||
+ | |||
+ | $ | ||
+ | \frac{\cal A }{\cal B \Rightarrow A} | ||
+ | \qquad (添加) | ||
+ | $ | ||
+ | |||
+ | により、 | ||
+ | An⇒BiはH2で証明可能な論理式になる。 | ||
+ | |||
+ | BiがAn自身ならば、公理(1) | ||
+ | により、 | ||
+ | An⇒An | ||
+ | はH2で証明可能な論理式である。 | ||
+ | |||
+ | * Biが公理系Hの各公理の形の論理式であるとき、 | ||
+ | 同様に「添加」により、 | ||
+ | An⇒BiはH2で証明可能な論理式である。 | ||
+ | |||
+ | * 論理式 Bi の前に論理式 BjとBk | ||
+ | (j,k<i)があり、BkはBj⇒Bi の | ||
+ | 形をしているときは、 | ||
+ | An⇒Biの前に、 | ||
+ | |||
+ | An⇒Bjと${\cal A}_n \Rightarrow | ||
+ | ({\cal B}_j \Rightarrow {\cal B}_i)$とがあることになる。 | ||
+ | |||
+ | これに「複推移」 | ||
+ | |||
+ | $ | ||
+ | \frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } | ||
+ | {\cal A \Rightarrow C} (復推移) | ||
+ | $ | ||
+ | |||
+ | を適用すると | ||
+ | An⇒Biが得られる。◻ | ||
+ | |||
+ | ===演繹定理の応用=== | ||
+ | |||
+ | |||
+ | |||
+ | *¬A⊢H⊥のとき ⊢HA | ||
+ | |||
+ | |||
+ | これは、まず | ||
+ | |||
+ | $ | ||
+ | {\cal \lnot A}\vdash_H \bot | ||
+ | $ | ||
+ | |||
+ | から演繹定理により | ||
+ | $ | ||
+ | \vdash_H \cal \lnot A \Rightarrow \bot | ||
+ | $ | ||
+ | |||
+ | これと公理(14)から | ||
+ | |||
+ | $ | ||
+ | \vdash_H \cal \lnot A \Rightarrow A | ||
+ | $ | ||
+ | |||
+ | となる。さらに(1)により、 | ||
+ | |||
+ | $ | ||
+ | \cal A \Rightarrow A | ||
+ | $ | ||
+ | |||
+ | と(8)から | ||
+ | |||
+ | $ | ||
+ | \cal (\lnot A \Rightarrow A) \Rightarrow [(A \Rightarrow A) | ||
+ | \Rightarrow \{(A \lor \lnot A ) \Rightarrow A\} ] | ||
+ | $ | ||
+ | |||
+ | が得られる。また、(15)により | ||
+ | |||
+ | $ | ||
+ | \cal A \lor \lnot A | ||
+ | $ | ||
+ | |||
+ | が成り立っている。これらより結局 | ||
+ | |||
+ | $ | ||
+ | \vdash_H \cal A | ||
+ | $ | ||
+ | ◻ | ||
+ | |||
+ | 上の結果を推論規則の形で表現すれば | ||
+ | |||
+ | $ | ||
+ | \frac{\cal \lnot A \Rightarrow \bot }{\cal A} | ||
+ | $ | ||
+ | |||
+ | |||
+ | また論理式の形で表せば | ||
+ | |||
+ | $ | ||
+ | \cal (\lnot A \Rightarrow \bot) \Rightarrow A | ||
+ | $ | ||
+ | |||
+ | である。(いずれも⊢Hが省略されていることに注意) | ||
+ | |||
+ | |||
+ | *$ | ||
+ | \frac{\cal A \Rightarrow B}{\cal \lnot B \rightarrow \lnot A} | ||
+ | (「対偶」) | ||
+ | $ | ||
+ | |||
+ | まず、 | ||
+ | |||
+ | $ | ||
+ | \cal \vdash_H A \Rightarrow B | ||
+ | $ | ||
+ | |||
+ | を仮定する。系Hに¬Bを追加して得られる系をH1とする。 | ||
+ | さらにこれに¬Aの否定¬¬Aを追加した系をH2と | ||
+ | すると、2重否定により、⊢H2Aが、従って | ||
+ | ⊢H2Bが得られる。このことから | ||
+ | ⊢H2⊥となり、結局⊢H1¬B⇒¬Aが得られる。◻ | ||
+ | |||
+ | 体系 H については、次の事実が知られている: | ||
+ | |||
+ | |||
+ | *'''命題計算の体系についての完全性定理''' | ||
+ | |||
+ | |||
+ | A が恒真論理式であることの必要十分条件は、⊢HA | ||
+ | が成立することである。◻ | ||
+ | |||
+ | この定理は、'''命題計算の体系についての完全性定理'''(completeness | ||
+ | theorem)と呼ばれるものである。 | ||
+ | *[証明] | ||
+ | |||
+ | まず、⊢HAが成立すればAが恒真論理式であることを示そう。 | ||
+ | |||
+ | ⊢HAが成り立つとすると; | ||
+ | |||
+ | 系Hの「証明」である論理式の列 | ||
+ | |||
+ | $ | ||
+ | {\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n | ||
+ | $ | ||
+ | |||
+ | があって、Aは最後のAnと一致しているものとしてよい。 | ||
+ | 各Aiは | ||
+ | |||
+ | |||
+ | * 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3 | ||
+ | であるからAiは恒真論理式である。 | ||
+ | |||
+ | * 論理式 Ai の前に論理式 AjとAk | ||
+ | (j,k<i)があり、AkはAj⇒Ai の | ||
+ | 形をしている。 | ||
+ | iより前の論理式は恒真論理式であると仮定すると、 | ||
+ | AjとAj⇒Aiは真理値⊤しかとらないから真理値表 | ||
+ | |||
+ | |||
+ | |||
+ | {| border="3" class="wikitable" | ||
+ | ||Aj | ||
+ | |Ai | ||
+ | |Aj⇒Ai | ||
+ | |- | ||
+ | | ⊥ | ||
+ | | ⊥ | ||
+ | | ⊤ | ||
+ | |- | ||
+ | | ⊥ | ||
+ | | ⊤ | ||
+ | | ⊤ | ||
+ | |- | ||
+ | | ⊤ | ||
+ | | ⊥ | ||
+ | | ⊥ | ||
+ | |- | ||
+ | | ⊤ | ||
+ | | ⊤ | ||
+ | | ⊤ | ||
+ | |} | ||
+ | |||
+ | |||
+ | |||
+ | から明らかなようにAiの真理値は⊤しか取り得ない。 | ||
+ | すなわちAiは恒真論理式である。 | ||
+ | |||
+ | |||
+ | 逆にAが恒真論理式であるときに、 | ||
+ | ⊢HAが成立することをいうには次の補題1が必要になる。 | ||
+ | *[補題] | ||
+ | |||
+ | Aが命題変数X1,X2,⋯,Xnから構成される論理式とする。 | ||
+ | 命題変数X1,X2,⋯,Xnに真理値⊤,⊥をふり当て、そのふり当てに対しAの真理値が⊤である場合 | ||
+ | |||
+ | $ | ||
+ | \delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal A | ||
+ | $ | ||
+ | |||
+ | Aの真理値が⊥である場合 | ||
+ | |||
+ | $ | ||
+ | \delta X_1,\delta X_2,\cdots \delta X_n \vdash_H \cal \lnot A | ||
+ | $ | ||
+ | |||
+ | である。ただし、δXiはXiに対する真理値のふり当てが⊤の場合Xi、⊥の場合は¬Xiとする。◻ | ||
+ | |||
+ | *[定理の証明の続き] | ||
+ | |||
+ | 恒真論理式Aが命題変数X1,X2,⋯,Xnから構成されるものとする。 | ||
+ | する。 | ||
+ | 命題変数X1,X2,⋯,Xnに真理値⊤,⊥どのようにふり当ても、 | ||
+ | Aの真理値は常に⊤である。 | ||
+ | |||
+ | 命題変数X1,X2,⋯,Xnに真理値⊤,⊥どのようにふり当てるしかたは | ||
+ | 2n通りある。これを辞書式順序で全て列挙し[補題1]を適用すると | ||
+ | |||
+ | |||
+ | $X_1,X_2,\cdots , X_n \vdash_H \cal A \\ | ||
+ | X_1,X_2,\cdots , \lnot X_n \vdash_H \cal A \\ | ||
+ | X_1,X_2,\cdots , \lnot X_{n-1},X_n \vdash_H \cal A \\ | ||
+ | X_1,X_2,\cdots , \lnot X_{n-1},\lnot X_n \vdash_H \cal A \\ | ||
+ | \cdots \\ | ||
+ | \cdots \\ | ||
+ | \lnot X_1,\lnot X_2,\cdots , \lnot X_n \vdash_H \cal A \\ | ||
+ | $ | ||
+ | |||
+ | |||
+ | が得られる。最初の2式から演繹定理により | ||
+ | |||
+ | $X_1,X_2,\cdots , X_{n-1} \vdash X_n \Rightarrow \cal A \\ | ||
+ | X_1,X_2,\cdots , X_{n-1} \vdash \lnot X_n \Rightarrow \cal A \\ | ||
+ | $ | ||
+ | |||
+ | これから | ||
+ | |||
+ | $ | ||
+ | X_1,X_2,\cdots , X_{n-1} \vdash_H \cal A | ||
+ | $ | ||
+ | |||
+ | が得られる。すなわちXnが消去された。同様にして順次に2式ずつ | ||
+ | 同じ手順を繰り返せば、Xnが消去された2n−1個の式を得る。この | ||
+ | 2n−1個の式からXn−1を2式ずつをとり同じ手順を繰り返すとXn−1が | ||
+ | 消去された2n−2個の式を得る。 | ||
+ | この手順を繰り返せば変数X1,X2,⋯,Xnが全て消去され、結局 | ||
+ | |||
+ | $ | ||
+ | \vdash_H \cal A | ||
+ | $ | ||
+ | |||
+ | を得る。◻ | ||
+ | |||
+ | *[補題の証明] | ||
+ | |||
+ | **論理式Aがただ1つの命題変数Xからなるとき | ||
+ | |||
+ | Xに対するふり当てが⊤のときX⊢HX また ⊥のとき ¬X⊢H¬X | ||
+ | これは公理の(1)から容易に示される。 | ||
+ | |||
+ | **これ以外の場合は、Aは¬B,B∧C,B∨Cの形をしている。 | ||
+ | |||
+ | そこで論理式の長さについての帰納法を使う. | ||
+ | |||
+ | Aより長さの短い部分式B,Cについてはこの補題が成り立つものとする。 | ||
+ | |||
+ | |||
+ | ***A が¬Bである場合 | ||
+ | |||
+ | |||
+ | Aの値が⊤のときBの値は⊥であるから | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢H¬B | ||
+ | |||
+ | Aの値が⊥のときBの値は⊤であるから | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢HB | ||
+ | |||
+ | B,¬BはそれぞれA及び¬Aである。 | ||
+ | |||
+ | ***A がB∨Cである場合 | ||
+ | |||
+ | Aの値が⊤のときB,Cの少なくともどちらか一方の値は | ||
+ | ⊤であるから、Bの値が⊤としても一般性を失わない。このとき | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢HB | ||
+ | |||
+ | が成り立っている。これと公理の(3) | ||
+ | |||
+ | B⇒B∨C | ||
+ | |||
+ | により | ||
+ | δX1,δX2,⋯,δXn⊢HB∨C | ||
+ | |||
+ | B∨CはAに他ならない。 | ||
+ | |||
+ | Aの値が⊥のときB,Cの値はともに⊥でなければならない。 | ||
+ | このとき | ||
+ | δX1,δX2,⋯,δXn⊢H¬B | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢H¬C | ||
+ | |||
+ | これに推論法則の「論理積」 | ||
+ | |||
+ | $ | ||
+ | \frac{\cal P,Q}{\cal P \land Q} | ||
+ | $ | ||
+ | |||
+ | を用いて | ||
+ | |||
+ | $ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H | ||
+ | \cal \lnot B \land \lnot C$ | ||
+ | を得る。 | ||
+ | |||
+ | ¬B∧¬Cは¬A(=¬(B∨C))に他ならない。 | ||
+ | |||
+ | |||
+ | ***A がB∧Cである場合 | ||
+ | |||
+ | |||
+ | Aの値が⊤のときB,Cの値はともに⊤でなければならない。 | ||
+ | このとき | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢HB | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢HC | ||
+ | |||
+ | これに推論法則の「論理積」 | ||
+ | |||
+ | $ | ||
+ | \frac{\cal P,Q}{\cal P \land Q} | ||
+ | $ | ||
+ | |||
+ | を用いて | ||
+ | $ \delta X_1,\delta X_2,\cdots,\delta X_n \vdash_H | ||
+ | \cal B \land C$ | ||
+ | を得る。 | ||
+ | B∧CはAに他ならない。 | ||
+ | |||
+ | Aの値が⊥のときB,Cの少なくともどちらか一方の値は | ||
+ | ⊥であるから、Bの値が⊥としても一般性を失わない。このとき | ||
+ | |||
+ | δX1,δX2,⋯,δXn⊢H¬B | ||
+ | が成り立っている。これと公理の(3) | ||
+ | P⇒P∨Q | ||
- | + | により | |
+ | δX1,δX2,⋯,δXn⊢H¬B∨¬C | ||
- | + | ¬B∨¬Cは¬A=¬(B∧C)に他ならない。 | |
+ | ◻ |
2020年12月1日 (火) 01:33 時点における最新版
目次[非表示] |
演繹推論
演繹的推論は論理的思考の根幹である.
簡単な例を挙げる。
- (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万人+1人である.
しかしこれは「(2)東京都民の人口は1200万人である.」に矛盾する.
この矛盾は 命題「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」
の否定が成り立つとしたことによっている.
従って「東京都民のうち少なくとも2人は髪の毛の本数は同じである.」が正しい.
上記の 命題(1),(2)が正しければ命題(3)が正しいことを論証した過程は 論理の連鎖に依っている.命題(3)を否定した命題が正しいとして論理の連鎖を つくり,矛盾を導くことによって命題(3)の正しさを証明した.
演繹推論はこのように,正しいもとして与えられた命題から厳密な論理を
繰り返し適用することによって新たな命題を結論として導き出す.
この過程(証明)は,その論証の過程に出てくる命題やそれに施す論理的な推論を計算機によって処理できる形式化された記述で書けば,計算機によってその正しさを検証できる.それを形式化を行うかどうかは別として計算機による検証で正しさが認められるものでなければ完全な演繹推論とは言えない.
実際,以下は定理証明支援系のMizarによって上記の推論を記述したものである.
Mizarのような定理証明支援系あるいは形式化証明検証システムでは,命題は全て記号列であり,三段論法その他の推論規則はそれらの複数の記号列を操作して
別の新たな記号列を構成する規則に過ぎない.証明は,前提となる命題(記号列)から出発して,目的の命題(記号列)に至る,推論規則により
生成された記号列の列にに過ぎない.
特に,A.I. や ICTの進歩など数学を含む科学技術の進歩の激流の中にある,科学工学の技術者はMizarのようなシステムの操作にも慣れ親しむことが必要になってくる.
environ vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3, RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4, TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0, UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0; notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1, TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY; constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1, BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1, XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY, XREAL_0, RVSUM_1; requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE; definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, PRE_POLY,FINSET_1,CARD_1; theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1, INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1, FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1, FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2, FINSET_1,PARTFUN1, PRE_POLY, CARD_1; schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1; begin now let Humankind be finite set, Tokyoite be Subset of Humankind, Numberofhair be Function of Tokyoite,NAT ; assume LM1: card (Tokyoite) = 12*10|^6; assume LM2: for x be object st x in Tokyoite holds Numberofhair.x <= 10|^6; LM0: 10|^6 + 1 < 12*10|^6 proof 0 < 10|^6 by PREPOWER:6; then P2: 1*10|^6 < 11* 10|^6 by XREAL_1:68; P3: 1 < 10 & 2 <= 6; then 10 < 10 |^6 by PREPOWER:13; then 1 < 10 |^6 by XXREAL_0:2,P3; then 1 < 11*10|^6 by P2,XXREAL_0:2; then P4: 1*10|^6 + 1 < 1*10|^6 + 11*10|^6 by XREAL_1:8; 1*10|^6 + 11*10|^6 = (1+11)*10|^6 ; hence thesis by P4; end; LM3: card (rng Numberofhair) <= 10|^6+1 proof now let y be object ; assume y in rng Numberofhair; then consider x be object such that A1: x in Tokyoite & y=Numberofhair.x by FUNCT_2:11; Numberofhair.x <= 10|^6 by A1,LM2; then Numberofhair.x < 10|^6+1 by NAT_1:16,XXREAL_0:2; then Numberofhair.x in Segm (10|^6+1) by NAT_1:44,A1; hence y in Segm (10|^6+1) by A1; end; then A2: rng Numberofhair c= Segm (10|^6+1) by TARSKI:def 3; then card rng Numberofhair <= card Segm (10|^6+1) by NAT_1:43; then card rng Numberofhair <= card (10|^6+1) by ORDINAL1:def 17; hence card rng Numberofhair <= (10|^6+1) ; end; LM4: card (rng (Numberofhair)) < card (Tokyoite) proof reconsider N1= card (rng (Numberofhair)) as Element of NAT ; reconsider N2= card (Tokyoite) as Element of NAT ; A1: N1<=(10|^6+1) & N2=12*10|^6 by LM1,LM3; then N1 < N2 by A1,XXREAL_0:2,LM0; hence thesis ; end; EX: ex x,y be object st x in Tokyoite & y in Tokyoite & x <> y & Numberofhair.x = Numberofhair.y proof assume A1: not ( ex x,y be object st x in Tokyoite & y in Tokyoite & x <> y & Numberofhair.x = Numberofhair.y ) ; then A2: for x,y be object st x in Tokyoite & y in Tokyoite & x <> y holds Numberofhair.x <> Numberofhair.y ; A3: dom Numberofhair = Tokyoite by FUNCT_2:def 1; then for x,y be object st x in dom Numberofhair & y in dom Numberofhair & Numberofhair.x = Numberofhair.y holds x = y by A2; then Numberofhair is one-to-one by FUNCT_1:def 4; then card (dom Numberofhair) = card (rng Numberofhair) by CARD_1:70; then card (Tokyoite) = card (rng (Numberofhair)) by A3; hence contradiction by LM4; end; end;
公理系と推論
論理式
「真」とする複数の命題から論理的操作をして,「真」である命題を導き出す演繹推論は代数的演算のような扱いができる.
ここでは,そのような扱いを「命題論理」によって説明する.
「命題」をそれが何を主張しているかを意味を考えずに,それが「真」か「偽」であるかどうかだけを考えれば,命題は 代数的な演算の変数とみなすことができる. これを命題変数と呼ぶ.
命題の「真」,「偽」はその変数の値あるいは定数のように扱うことができる.
その上で,一つの命題に,あるいは命題と命題をつなぐ「~でない」 「かつ」 「または」 「ならば」
などを命題を表す命題変数に作用する演算子とみなすことにする.
それらをそれぞれ⊤ および ⊥ ¬,∧,∨,⇒で表す.
命題変数にこれらの演算子を作用させたものを論理式と呼ぶ.
論理式はこれを以下のように再帰的に定義する.
- ⊤ および ⊥ は論理式である。
- 個々の命題変数は論理式である。
- A が論理式ならば、¬A も論理式である。
- A,B が論理式ならば、
A∧B,A∨B,A⇒B は、いずれも論理式である。
- 以上によって定まるものみが論理式である。
論理式の全体を L と書くことにしよう。
L の要素である論理式は、いずれもその論理式を表現としてもつ真理 関数と考えられる。任意の真理関数は、その独立変数がとり得る値のとり方 (n 変数ならば 2n 通り)の各々の場合について、有限回の操作でその 値(関数値)を決定できる。
L の論理式の値(真理関数とみなした場合の関数値)が、(命題変数の 値のとり方のすべてに対して)つねに ⊤ であるとき、そのような論理 式を{\gt 恒真論理式}(tautology)という。
公理系
公理系と呼ばれる L の部分集合 A と推論規則が適当に定めら れ、恒真論理式が A から推論規則によって導けるような体系を、 命題論理の公理的体系、あるいは命題計算の体系という。
いろいろな公理的体系が知られているが、ここではヒルベルト(D. Hilbert) 流のものを挙げておこう。
以下、A,B,C は任意の L の要素とする。 公理系 A として、次の (1)∼(15) をとる。
- A⇒A
- (A⇒B)⇒[(B⇒C)⇒(A⇒C)]
- A⇒(A∨B)
- B⇒(A∨B)
- (A⇒C)⇒{(B⇒C)⇒[(A∨B)⇒C]}
- (A∧B)⇒A
- (A∧B)⇒B
- (C⇒A)⇒{(C⇒B)⇒[C⇒(A∧B)]}
- [A∧(A⇒B)]⇒B
- [(A∧C)⇒B]⇒[C⇒(A⇒B)]
- (A∧¬A)⇒⊥
- [(A∧B)⇒⊥]⇒(B⇒¬A)
- A⇒⊤
- ⊥⇒A
- A∨¬A
推論規則は、次の三段論法(modus ponens)のみである。横線の上の論 理式から下の論理式が導かれることを表わす。
AA⇒BB
証明可能性を定義する。すなわち、L の要素である論理式のうち、 証明可能な論理式(provable formula)を次のように定める:
- 公理系の各公理の形の論理式は証明可能である。
- 論理式 A と論理式 A⇒B が証明可能ならば、(推論規則によって、)論理式 B は証明可能である。
- 以上によって定まるものだけが、証明可能な論理式である。
推論法則
証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば
A1,A2,⋯,An が「証明」のとき各Aiは
- 公理系の各公理の形の論理式である。
- 論理式Aiの前に論理式AjとAk(j,k<i)がありAkはAj⇒Aiの形をしている。
例えば、
B∧A⇒A,(B∧A⇒A)⇒(A⇒(B⇒A)),A⇒(B⇒A)
もっと具体的には
1=2∧2>6⇒2>6(1=2∧2>6⇒2>6)⇒(2>6⇒(1=2⇒2>6))2>6⇒(1=2⇒2>6)
は証明である。(証明可能な論理式を「定理」とか「命題」と呼ぶこともある。)
「証明」の中で推論規則と公理を何回か適用する共通した手順を「推論法則」 と呼ぶ。(これ自身は公理系を定義するのに必須ではないが、それを操作する 上で便利な手続きをまとめたもの。)
推論法則
- AB⇒A(推論法則:添加)
Aが証明可能な論理式ならばB⇒Aも 証明可能な論理式であることを表す。 (上の「証明」の例に現れている。)
- A,BA∧B(推論法則:論理積)
任意の論理式Cを用いて「添加」により
(C∨¬C)⇒A,(C∨¬C)⇒B
が得られる。また(8)であるから
{(C∨¬C)⇒A}⇒[{(C∨¬C)⇒B}⇒{(C∨¬C)⇒(A∧B)}]
推論規則により、
(C∨¬C)⇒(A∧B)
が得られる。ところで(15)により
C∨¬C
は公理(当然証明可能な論理式であるから) 結局
A∧B
は証明可能な論理式である。◻
またこれから直ちに
- A∧BB∧A(推論法則:交換)
が得られる。 同様に
- A∨BB∨A(推論法則:交換)
も得られる。さらに
- A⇒¬¬A,¬¬A⇒A(推論法則:2重否定)
も得られる。
- A⇒B,B⇒CA⇒C(推論法則:推移)
これは(2)より
(A⇒B)⇒[(B⇒C)⇒(A⇒C)]
が得られ、これと
A⇒B
から推論規則により、
(B⇒C)⇒(A⇒C)
を得る。さらにこれと
B⇒C
とから
A⇒C
が得られることで示される。◻ %% %% 同様に
- A⇒(B⇒C),A⇒BA⇒C (推論法則:復推移)
が得られる。これはまず、(8)から
(A⇒B)⇒[{A⇒(B⇒C)}⇒{A⇒B∧(B⇒C)}]
これと
A⇒(B⇒C),A⇒B
から
A⇒{B∧(B⇒C)}
が得られ さらに(9)の
{B∧(B⇒C)}⇒C
と前述の「推移」により
A⇒C
が得られることで示される。◻
演繹定理
演繹定理
前述の公理系と推論規則のセットを H と呼ぶことにしよう。(H=公理系{\bf A}+「推論規則」)
Lの論理式 A が証明 可能であるとは、H において、公理系 A から A が推論規 則によって導けることであるから、これを
⊢HA
と書く。推論規則
AA⇒BB
はこの表記法を用いると、
⊢HA⊢HA⇒B⊢HB
と書くべきである。しかし、どの系で証明可能なのか明らかな場合は ⊢Hは省略することにする。
[演繹定理]
上の体系Hについてその公理系Aに論理式
A1,A2,⋯,An
を追加してできる新たな系で 論理式Bが証明可能であるとき、このことを
A1,A2,⋯,An⊢HB
で表す。さらにこのとき:
A1,A2,⋯,An−1⊢HAn⇒B
が成り立つ。
また、これを繰り返せば
A1,A2,⋯,An−2⊢HAn−1⇒(An⇒B)
[演繹定理の証明]
体系Hについてその公理系Aに論理式
A1,A2,⋯,An
を追加してできる新たな系をH1で表わす.
A1,A2,⋯,An⊢HB
ならば
⊢H1B
である.
体系Hについてその公理系Aに論理式
A1,A2,⋯,An−1
を追加してできる系をH2で表す。
示すべきことは
⊢H2An⇒B
である。
B1,B2,⋯,Bn−1,Bn(=B)
がH1での「証明」とするとき、定義より 各Biは次のいずれかである。
- BiはA1,A2,⋯,Anのうち1つで
ある。
- Biは公理系Hの各公理の形の論理式である。
- 論理式 Bi の前に論理式 BjとBk
(j,k<i)があり、BkはBj⇒Bi の 形をしている。
そして、
An⇒B1,An⇒B2,⋯,An⇒Bn−1,An⇒Bn
はH2でのAn⇒Bを含む「証明」になる。
- BiがA1,A2,⋯,An−1のうち1つであれば、「添加」
AB⇒A(添加)
により、 An⇒BiはH2で証明可能な論理式になる。
BiがAn自身ならば、公理(1) により、 An⇒An はH2で証明可能な論理式である。
- Biが公理系Hの各公理の形の論理式であるとき、
同様に「添加」により、 An⇒BiはH2で証明可能な論理式である。
- 論理式 Bi の前に論理式 BjとBk
(j,k<i)があり、BkはBj⇒Bi の 形をしているときは、 An⇒Biの前に、
An⇒BjとAn⇒(Bj⇒Bi)とがあることになる。
これに「複推移」
A⇒(B⇒C),A⇒BA⇒C (復推移)
を適用すると An⇒Biが得られる。◻
演繹定理の応用
- ¬A⊢H⊥のとき ⊢HA
これは、まず
¬A⊢H⊥
から演繹定理により ⊢H¬A⇒⊥
これと公理(14)から
⊢H¬A⇒A
となる。さらに(1)により、
A⇒A
と(8)から
(¬A⇒A)⇒[(A⇒A)⇒{(A∨¬A)⇒A}]
が得られる。また、(15)により
A∨¬A
が成り立っている。これらより結局
⊢HA ◻
上の結果を推論規則の形で表現すれば
¬A⇒⊥A
また論理式の形で表せば
(¬A⇒⊥)⇒A
である。(いずれも⊢Hが省略されていることに注意)
- A⇒B¬B→¬A(「対偶」)
まず、
⊢HA⇒B
を仮定する。系Hに¬Bを追加して得られる系をH1とする。 さらにこれに¬Aの否定¬¬Aを追加した系をH2と すると、2重否定により、⊢H2Aが、従って ⊢H2Bが得られる。このことから ⊢H2⊥となり、結局⊢H1¬B⇒¬Aが得られる。◻
体系 H については、次の事実が知られている:
- 命題計算の体系についての完全性定理
A が恒真論理式であることの必要十分条件は、⊢HA
が成立することである。◻
この定理は、命題計算の体系についての完全性定理(completeness theorem)と呼ばれるものである。
- [証明]
まず、⊢HAが成立すればAが恒真論理式であることを示そう。
⊢HAが成り立つとすると;
系Hの「証明」である論理式の列
A1,A2,⋯,An
があって、Aは最後のAnと一致しているものとしてよい。 各Aiは
- 公理系の各公理の形の論理式である。この場合、各公理は恒真論理式3
であるからAiは恒真論理式である。
- 論理式 Ai の前に論理式 AjとAk
(j,k<i)があり、AkはAj⇒Ai の 形をしている。 iより前の論理式は恒真論理式であると仮定すると、 AjとAj⇒Aiは真理値⊤しかとらないから真理値表
Aj | Ai | Aj⇒Ai |
⊥ | ⊥ | ⊤ |
⊥ | ⊤ | ⊤ |
⊤ | ⊥ | ⊥ |
⊤ | ⊤ | ⊤ |
から明らかなようにAiの真理値は⊤しか取り得ない。 すなわちAiは恒真論理式である。
逆にAが恒真論理式であるときに、
⊢HAが成立することをいうには次の補題1が必要になる。
- [補題]
Aが命題変数X1,X2,⋯,Xnから構成される論理式とする。 命題変数X1,X2,⋯,Xnに真理値⊤,⊥をふり当て、そのふり当てに対しAの真理値が⊤である場合
δX1,δX2,⋯δXn⊢HA
Aの真理値が⊥である場合
δX1,δX2,⋯δXn⊢H¬A
である。ただし、δXiはXiに対する真理値のふり当てが⊤の場合Xi、⊥の場合は¬Xiとする。◻
- [定理の証明の続き]
恒真論理式Aが命題変数X1,X2,⋯,Xnから構成されるものとする。 する。 命題変数X1,X2,⋯,Xnに真理値⊤,⊥どのようにふり当ても、 Aの真理値は常に⊤である。
命題変数X1,X2,⋯,Xnに真理値⊤,⊥どのようにふり当てるしかたは 2n通りある。これを辞書式順序で全て列挙し[補題1]を適用すると
X1,X2,⋯,Xn⊢HAX1,X2,⋯,¬Xn⊢HAX1,X2,⋯,¬Xn−1,Xn⊢HAX1,X2,⋯,¬Xn−1,¬Xn⊢HA⋯⋯¬X1,¬X2,⋯,¬Xn⊢HA
が得られる。最初の2式から演繹定理により
X1,X2,⋯,Xn−1⊢Xn⇒AX1,X2,⋯,Xn−1⊢¬Xn⇒A
これから
X1,X2,⋯,Xn−1⊢HA
が得られる。すなわちXnが消去された。同様にして順次に2式ずつ 同じ手順を繰り返せば、Xnが消去された2n−1個の式を得る。この 2n−1個の式からXn−1を2式ずつをとり同じ手順を繰り返すとXn−1が 消去された2n−2個の式を得る。 この手順を繰り返せば変数X1,X2,⋯,Xnが全て消去され、結局
⊢HA
を得る。◻
- [補題の証明]
- 論理式Aがただ1つの命題変数Xからなるとき
Xに対するふり当てが⊤のときX⊢HX また ⊥のとき ¬X⊢H¬X これは公理の(1)から容易に示される。
- これ以外の場合は、Aは¬B,B∧C,B∨Cの形をしている。
そこで論理式の長さについての帰納法を使う.
Aより長さの短い部分式B,Cについてはこの補題が成り立つものとする。
- A が¬Bである場合
Aの値が⊤のときBの値は⊥であるから
δX1,δX2,⋯,δXn⊢H¬B
Aの値が⊥のときBの値は⊤であるから
δX1,δX2,⋯,δXn⊢HB
B,¬BはそれぞれA及び¬Aである。
- A がB∨Cである場合
Aの値が⊤のときB,Cの少なくともどちらか一方の値は ⊤であるから、Bの値が⊤としても一般性を失わない。このとき
δX1,δX2,⋯,δXn⊢HB
が成り立っている。これと公理の(3)
B⇒B∨C
により δX1,δX2,⋯,δXn⊢HB∨C
B∨CはAに他ならない。
Aの値が⊥のときB,Cの値はともに⊥でなければならない。 このとき δX1,δX2,⋯,δXn⊢H¬B
δX1,δX2,⋯,δXn⊢H¬C
これに推論法則の「論理積」
P,QP∧Q
を用いて
δX1,δX2,⋯,δXn⊢H¬B ∧¬C を得る。
¬B∧¬Cは¬A(=¬(B∨C))に他ならない。
- A がB∧Cである場合
Aの値が⊤のときB,Cの値はともに⊤でなければならない。
このとき
δX1,δX2,⋯,δXn⊢HB
δX1,δX2,⋯,δXn⊢HC
これに推論法則の「論理積」
P,QP∧Q
を用いて δX1,δX2,⋯,δXn⊢HB ∧C を得る。 B∧CはAに他ならない。
Aの値が⊥のときB,Cの少なくともどちらか一方の値は ⊥であるから、Bの値が⊥としても一般性を失わない。このとき
δX1,δX2,⋯,δXn⊢H¬B
が成り立っている。これと公理の(3)
P⇒P∨Q
により
δX1,δX2,⋯,δXn⊢H¬B∨¬C
¬B∨¬Cは¬A=¬(B∧C)に他ならない。 ◻