Path: sran265!katsu
From: katsu@sran14.sra.co.jp (Katsuhiro Watanabe)
Message-ID: <KATSU.92Feb24131733@sran14.sra.co.jp>
Date: 24 Feb 92 13:17:33
Organization: Software Research Associates, Inc.,Japan
In-reply-to: miyata@sra.co.jp's message of 9 Feb 92 09:01:46 GMT
Newsgroups: sra.comp.misc
Subject: Re: Formal Methods
Distribution: sra
References: <474@srasvf.sra.co.jp> <MIYATA.92Feb2170430@ext230.sra.co.jp>
	<SUGITA.92Feb5132024@sran159.sra.CO.JP>
	<MIYATA.92Feb7130126@ext230.sra.co.jp>
	<MIYATA.92Feb9180146@ext230.sra.co.jp>

　sra で恐らく一番 follow が遅い渡邊＠ソフト工研です。

　ツール S?P の正当性を、S?P 自身を用いて証明する件ですが、
記事 <MIYATA.92Feb9180146@ext230.sra.co.jp> で
miyata@sra.co.jp (Shigeaki Miyata) さんいはく

> 岩波書店の数学事典の661頁には次のように書いてあります。

> ［自然数の理論を含む形式的体系Sが有限の立場で与えられ
> しかもSが無矛盾であるならばSの中で形式化されるような
> 論法だけによってはSの無矛盾性を証明する事は不可能である］

　S?P は StP を連想させすぎでは？
　さて、

　『S?P はどうだかわからないが、StP は
(1)自然数の理論を含んでいない
(2)形式的体系でない
ので、上の不完全性定理の結果を応用することはできない』

って言ったら、これはくだんの形式主義者の言い種の一種なのでしょうか？ :-)

　実は私は StP は使ったことがなく、セミナーを１日受けただけなので、
間違っているかもしれません。どうして (1)(2) のように思うかというと、
(1') 例えば数学的帰納法が含まれていない。（ペアノの５公準だとか
　　いうようなやつのことを考えています。）
(2') StP の公理と推論規則が定まってない。がんばれば定まるとも見えるが、
　　でも定まるようなら結構な宣伝文句になるはずなのに定めていない。
からです。

　「無矛盾」っていう点でも案外安心できないかもしれません。解釈が
きちんと定まっているようならいいのですが、そうでないと矛盾無矛盾
さえも決定できませんよね？

--
----____----____
渡邊克宏＠ソフトウェア工学研究所（四谷）