余帰納法についての質問と回答

cutsea110 @cutsea110

@esumii @ksknac あ、そうですね。混乱してます。。 何か余帰納的なもの同士が同値であることを求める、という直感的には終わらないはずの命題がどうやって証明できてしまえるか？という流れが分かると少し納得できるようになるかな。 mandel59.hateblo.jp/entry/2013/02/… これとかが具体例だと思うのですが。

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

@cutsea110 @ksknac 帰納法は自然数のように帰納的に定義された集合に対し「すべての自然数は…を満たす」つまり「N⊆…」のような命題を証明するのに対して、余帰納法は先のSのように余帰納的に定義された集合に対し「…⊆S」のような命題（…に属するプログラムが非停止性なり等価性なりを満たすこと）を示すと思えば。

cutsea110 @cutsea110

@esumii @ksknac Pが停止しないことを証明するために、Pが余帰納的なものSの要素であることを証明する。という証明法ってことでいいですかね…

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

@cutsea110 @ksknac はい、そう思います。

cutsea110 @cutsea110

@esumii @ksknac しつこい質問に丁寧に答えていただき本当にありがとうございました。 まだ「余帰納法、完全に理解した！」とはなりませんが、大きな枠組みとしては分かってきました。 頑張って勉強続けます。

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

@cutsea110 @ksknac 追伸ですみません。「停止しないプログラム（状態）」の例だと「Pが停止しないならば、P→QなるQが存在して停止しない」でも良いと思います。別の例に引きづられて回りくどい定義を書いてしまいましたm(_ _)m

S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) @esumii

@cutsea110 @ksknac 何度もすみません。回りくどいというか私の書いた条件が間違っていますね（汗）。正しくは∀P.P∈S⇒∃Q.P→Q∧Q∈Sなので、要するにcutsea110さんの条件と同じですね。慌ててよく確かめずどうも失礼しました…