Path: sran265!katsu From: katsu@sran14.sra.co.jp (Katsuhiro Watanabe) Message-ID: Date: 3 Mar 92 18:24:05 Organization: Software Research Associates, Inc.,Japan In-reply-to: sugita@sra.CO.JP's message of 24 Feb 92 06:45:46 GMT Newsgroups: sra.comp.misc Subject: Re: Formal Methods Distribution: sra References: <474@srasvf.sra.co.jp> 　ううむ、formal method は難しくないとか、高度な数学的知識は必要ない とかいうのが議論の端緒の一つだったのが、「自然数の理論」だの 「形式的体系」だの「不完全性定理」だの、深遠な方へ向いちゃいましたね。 （私にはこれらは高度で難しい数学的知識に思えて、近づくのが恐いのです） 記事 で sugita@sra.CO.JP (Kenji Sugita) さんいはく > 現在の計 > 算機には自然数の理論は含まれていないのではないかと。含まれているのですか？ 　計算機自身が含む?かどうかわかりません。ある形式的体系と、それの （例えば）導出システムのようなもの（を計算機上に実装したもの）とは、 私は区別して考えています。 　（自然数の理論を含むような）形式的体系について、計算機上で (a)（自然数についての）勝手な定理の導出をやらせることができる (b)（自然数についての）定理のある導出と称するものがあった時に、 それが確かに正しい導出で最後に出たものが定理であるかを判定できる (c)ある命題があった時に、これがその理論での定理か否かを有限時間内で 判定するのは無理 ですよね。岩波の数学事典での > ［自然数の理論を含む形式的体系Sが有限の立場で与えられ > しかもSが無矛盾であるならばSの中で形式化されるような > 論法だけによってはSの無矛盾性を証明する事は不可能である］ 含むっていうのは、S の上で自然数の理論に関する表現ができるという ことでしょう。（表現できるというのはここでは、正しいとわかる 表明は定理で、正しくないとわかる表明は定理でないということ） 例えば(c)なんかとは無関係というのはいいですよね。 　「有限の立場」っていうのが、S での導出の規則が十分制限されていること （例えば計算機でも簡単にできるということ）を要請しているのではないかしら？ （詳しくは知りません） 　困った。またもや「導出」だの「有限の立場」だの妙な言葉が………。 まあ、この辺は枝葉の話かもしれないということで、大目に見て下さい。 -- ----____----____ 渡邊克宏＠ソフトウェア工学研究所（四谷）