推論規則と日本語による証明の対応関係

質問

以前、論理学の本を読み、コンピュータに軽く関わっている事もあり、数学基礎論に興味が発展しました。
推論規則などについて知る内に、高校で習った自然言語による証明との対応関係に疑問がわきました。
例えばゲッツェンの自然演繹などとどの様に対応しているのでしょうか？
論理記号で定義された、背理法や帰納法などの個々の規則は単独では納得していますが、数学の一般向けの本などに書かれている自然言語で記述された証明を見てもどうにも納得できない(論理構造を抜き出せない)事があります。
ぜひ、推論規則と日本語による証明の関係性を教えていただきたいのです。
何かいい本や、WEBサイト等ありましたら是非教えてください。

回答No.3

tgb · ベストアンサー

自然言語による証明との対応関係こうだと明快に説明できるわけではないですが、一般に認められるような推論のプロセスを経て結論に至るのはどちらも同じだと思います。
　異なる点としては、一般の(自然言語による)証明の場合は、曖昧さがあったり、接続の言葉が多かったり、論理の飛躍が紛れ込んだり、と言ったところでしょうか(厳密さが要求される場合にはそのようなことは少なくなるとは思いますが)。また、一般の証明の場合は証明の中に暗黙の前提となる定理のようなものをかなり多く含んでいると思います。
　基本的には自然言語の場合も論理学の場合も同じようなものなので、この「定理のようなもの」を論理学の証明において既に証明済みの論理式として導入する様な感覚で理解すれば、証明図(自然言語による証明を推論のプロセスをはっきりさせて論理学の証明図に近づけたもの)がスッキリしたように見えて来て全体が理解しやすくなると思います。
　質問者さんから自然言語による証明の例が提示されているので、これをを利用して「論理構造」が見えやすいような表現に変形して示してみたいと思います。
　ミスプリがあるように思われるので、こちらで適当に解釈します。
適当な解釈の内容は以下の通りです：
＃１：A~B==>A~B1　(ミスプリの修正)
＃２：証明内容を[C~D1,D1⊆DとなるD1が存在する]とする。
　　　(証明部分の内容から何を証明するかを推定してこのように変更)

先ず、文章を論理の筋立てがわかりやすくなるように少し変形しておきます。
　　※「証明のプロセス」(後出)との対応関係を見るためPF1～PF4に注意
●B~Dだから、BからDへの一対一の対応fがある。
==>B~Dである。B~DならばBからDへの一対一の対応fがある。(PF1)
●いま、B1の元fによる像全体のB1fをかんがえよう。
==>fによるB1の像が存在する。これをB1fとする。(PF2)
●しからば、当然B1f⊆DかつB1~B1f。
==>B1f⊆Dである。かつ、B1~B1fである。（PF3)
●いまB1f=D1とおく、さすれば、まずD1⊆Dで、しかもC~A~B1~B1f=D1よりC~D1。
ゆえに(定理a)が証明された。
==>C~AかつA~B1かつB1~B1fである。C~AかつA~B1かつB1~B1fならばC~B1fである。(PF4)
　　(B1f⊆Dであることは証明済みであり、)C~B1ｆであることから
　　B1fによりD1(の例として)の存在が示された。

次に各命題を取り出して記号で表現することにします。
(推論の道筋を主体にして見るにはこの方が都合がよい)

p1：|A|=|C|である
p2：|B|=|D|である
p3：あるB1が存在する
p4：A~B1である
p5：B1⊆Bである
p6：D1が存在する
p7：C~D1である
p8：D1⊆Dである
p9：C~Aである
p10：B~Dである
p11：BからDへの1:1対応fが存在する
p12：B1fが存在する
p13：B1f=f(B1)である
p14：B1~B1fである
p15：B1f⊆Dである
p16：B1f~Cである

証明すべき命題：
p1∧p2∧p3∧p4∧p5→p6∧p7∧p8

証明に使用する「定理」
(元の証明では無条件に成立するものとして使用しています。実際に通常の証明ではこれらを特に証明してから使用すると言うことはないと思います)

T1：p1→p9
T2：p2→p10
T3：p10→p11
T4：p11∧p3∧p5→p12∧p13
T5：p13→p14
T6：p13→p15
T7：p14∧p4∧p9→p16
T8：p12∧p15∧p16→p6∧p7∧p8

証明のプロセス：
　⇒の左辺は推論の仮定、右辺が結論です。
　左辺では以下の命題のみが使用されています。
　　・証明命題の「→」の左辺(証明の前提：p1～p5)
　　・その推論以前の推論で得られた結論(右辺に現れた命題：p9,p10,p11等)
　　・「定理」で列挙された命題(T1～T8)
　「定理」を使用するときはp1→p9[T1]のように[]を付加して番号を明記しておきます。

⇒p1∧p2∧p3∧p4∧p5　　(証明の前提：以下p1,p2等個別の命題として使用します)
(p1,p1→p9[T1])⇒p9
(p2,p2→p10[T2])⇒p10　　　・・・・・（PF1)
(p10,p10→p11[T3])⇒p11
(p11,p3,p5)⇒p11∧p3∧p5
(p11∧p3∧p5,p11∧p3∧p5→p12∧p13[T4])⇒p12∧p13　　　・・・・・（PF2)
(p13,p13→p14[T5])⇒p14
(p13,p13→p15[T6])⇒p15　　　・・・・・（PF3)
(p14,p4,p9)⇒p14∧p4∧p9
(p14∧p4∧p9,p14∧p4∧p9→p16[T7])⇒p16　　　・・・・・（PF4)
(p12,p15,p16)⇒p12∧p15∧p16
(p12∧p15∧p16,p12∧p15∧p16→p6∧p7∧p8[T8])⇒p6∧p7∧p8

　これを見ると、推論としては単純で、大略A,A→B,B→C,C→D,...,Y→Zから結論Zを導く形になっていることが分かると思います。ただ、証明のプロセスはほぼ忠実に再現出来ていると思いますので上記プロセスと元の証明のプロセスとを丁寧に見比べれば、対応関係が見えてくるのではないかと思います。

　上記の証明のプロセスで使用した手順を更に各「定理」の証明にも適用して詳細に記述すれば(記述して体裁を整えれば)論理学で質問者さんが証明図だと思うようなものに近づくでしょう。

※この証明は本来は述語論理を使って示すべきだったかも知れません。それをお茶を濁して命題論理で片づけてしまいましたので、多々あるツッコミどころには目をつぶって頂いて、自然言語による証明と論理学で示される証明との対応関係に焦点を当てることに注力して下さい。

回答No.2

trytobe

日本語でも英語でも、論理的に一意に論理構造が説明できれば良いだけで、

それを突き詰めていけば、最終的にはすべて数学記号という「言語」で記述すればよいが、

プログラミング言語と同じで人間に対する可読性が極端に落ちるので、自然言語で「解説してあげている」だけです。

お礼

お礼が遅れまして申し訳御座いません。
成る程、ターゲットはあくまでもその意味であり、言語間の対応関係はそれほど重要ではないということですね。。

回答No.1

f272

「数学の一般向けの本などに書かれている自然言語で記述された証明」というのがいい加減に書かれているだけかもしれません。具体例はありますか？

補足

回答ありがとうございます!
なぜか投稿が消えてしまします。。今回で消えてしまったら諦めます。
運営者様、著作権上の問題がありましたらお知らせ下さい。専門書ですので引用の範囲かと認識しておりますが。

そうですねぇこれっというのは無いのですが、例えば。。

ISBN:978-4480095886より引用(システムの都合上、多少の変更あり)
(数字は添え字、~は対等)
(定理a) |A|=|C|, |B|=|D|とし、A~B, B1⊆BなるB1がある。

B~Dだから、BからDへの一対一の対応fがある。
いま、B1の元fによる像全体のB1fをかんがえよう。
しからば、当然B1f⊆DかつB1~B1f。
いまB1f=D1とおく、さすれば、まずD1⊆Dで、しかもC~A~B1~B1f=D1よりC~D1。
ゆえに(定理a)が証明された。