11. 命題論理の定石
ウカシェビッチの公理からは色々な証明のテクニックが見えてくる。ウカシェビッチの公理を再掲すると次のようになる。 P1. A -> (B -> A) P2. (A -> (B -> C)) -> ((A -> B) -> (A -> C)) P3. (¬B -> ¬A) -> (A -> B) 1. 定石その1 P1 は B に任意の命題を当てはめることができるため、証明に任意の命題を導入できる。しかし、前件 A が定理ならば B -> A は定理なので、A が定理の場合、後件を A にすれば任意の命題を前件にしたものは定理になる。すなわち、 B -> A が定理となる。 2. 定石その2 P2 は複雑な形をしているが、活用する時は、基本的には前件が定理の場合が多い。つまり、前件の A -> (B -> C) という形はすでにある定理の命題を利用する場合が多いということだ。この場合、P2 の後件も定理になる。そう考えると、P2 は上の定理を次のような定理に変形させることができることを意味している。 (A -> B) -> (A -> C) 3. 定石その3 P3 を利用する目的は証明に否定演算子を導入することだが、P3 それ自身が定理(公理)だから、 (¬B -> ¬A) -> (A -> B) は定理である。これに、D が定理の時、任意の命題 C について C -> D も定理となる定石その1を利用すると、上の P3 を後件にして任意の命題 C を証明に導入できる。 C -> ((¬B -> ¬A) -> (A -> B)) これが定石その3だ。 さらに、C に ¬A を当てはめると、 ¬A -> ((¬B -> ¬A) -> (A -> B)) これを P2 による定石その2を使うと次の定理が得られる。 (¬A -> (¬B -> ¬A)) -> (¬A -> (A -> B)) この定理の前件は公理 P1 による定理だから、後件も定理になる。 ¬A -> (A -> B) つまり A の否定を前件にすると、後件に A -> B のような A を前件とし任意の命題 B を後件とする命題を導入できる。これは定石その4と呼べるだろう。 他にも定石と言えるテクニックは色々あると思うが『数学基礎論講義』にはあまり触れられていない。命題論理の完全性定理から定理は全てトートロジーであることが証明されているからだろう。トートロジーなら直接的な計算で判断できるからだ。 4. 定石の応用 上に述べた定石の応用として、『数学基礎論講義』の次の例題を解いてみる。問題は、 ¬¬A -> A を証明することだ。トートロジーの計算なら簡単に確かめることができるが、公理から演繹するためには証明しないといけない。 まず、この命題には否定演算子が登場するので公理 P2 を利用する必要がある。つまり、 (¬A -> ¬¬¬A) -> (¬¬A -> A) この時も証明したい命題を後件にするのがコツだ。これに定石その1を使って命題を導入した後、定石その2を使って前件を消去することを考える。普通に考えると ¬¬¬A を導入して次のようにすることになる。 ¬¬¬A -> ((¬A -> ¬¬¬A) -> (¬¬A -> A)) さらに P2 を適用して、前件のパターンが公理 P1 になるようにする。 (¬¬¬A -> (¬A -> ¬¬¬A)) -> (¬¬¬A -> (¬¬A -> A)) しかし、これだと得られる定理が次のようになって先が続かない。 ¬¬¬A -> (¬¬A -> A) そこで作戦を変えて、前件の消去に定石その4の ¬A -> (A -> B) を活用することにして、¬¬A を導入する。 ¬¬A -> ((¬A -> ¬¬¬A) -> (¬¬A -> A)) これだと P2 と定石 ¬A -> (A -> B) を適用して次の定理が得られる。 ¬¬A -> (¬¬A -> A) これは P2 で次のように変形できる (¬¬A -> ¬¬A) -> (¬¬A -> A) この記事では述べなかったが前回までの記事で何回か言及した定理 A -> A によって前件が定理だから、結局次の定理が得られることになる。 ¬¬A -> A このように命題論理の証明を考えるときは、上に述べたような定石を利用するのが便利だ。しかし、すべての定理をこの方法で導き出すことが目的ではなく、定理とトートロジーの同値関係を証明する(命題論理の完全性定理)のがもっと大切だ。このために活躍するのが、演繹定理と、証明への矛盾の導入だが、その際の議論にも上で述べた推論のテクニックは役に立つ。
by tnomura9
| 2016-08-07 05:07
| 考えるということ
|
Comments(0)
|
カテゴリ
新型コロナウイルス 主インデックス Haskell 記事リスト 圏論記事リスト 考えるということのリスト 考えるということ ラッセルのパラドックス Haskell Prelude Ocaml ボーカロイド 圏論 jQuery デモ HTML Python ツールボックス XAMPP Ruby ubuntu WordPress 脳の話 話のネタ リンク 幸福論 キリスト教 心の話 メモ 電子カルテ Dojo JavaScript C# NetWalker ed と sed HTML Raspberry Pi C 言語 命題論理 以前の記事
最新のトラックバック
最新のコメント
ファン
記事ランキング
ブログジャンル
画像一覧
|
ファン申請 |
||