お客様のなかにHauptsatzにお詳しい方は（ｒｙ

与式を示すのが普通だと思うのですが、この 2. を 2'. ∀y. [{∀x. ∀k＜y. φ(x, k)} ⇒ φ(0, y)] に代えた場合、数学的帰納法が成立するかどうかについて、御存知の方あれば教えて下さい！

2012-11-01 20:26:39

2 より広義なので、成り立つんではないでしょうか？でも、2'. を示すのは無駄があるので2を示せば十分ではないかと。 RT @Taroupho 与式を示すのが普通だと思うのですが、この 2. を 2'. ∀y. [{∀x. ∀k＜y. φ(x, k)} ⇒ φ(0, y)]

2012-11-01 20:43:21

@sakuranmocchi お返事ありがとうございます。より広義というのがピンと来ないのですが、∀k＜y. φ(0, k) より ∀x. ∀k＜y. φ(x, k) の方が強い帰納法の仮定ですよね。ということは、それだけ強く勝手に仮定してよい理由を説明する必要があるような……。

2012-11-01 20:50:53

ああー、頭が混乱してきたぞ。一般にQよりPが強いとき、すなわち P⇒Q のとき、Q⇒R から P⇒R が導ける、つまり (Q⇒R)⇒(P⇒R) となり、P⇒R より Q⇒R の方が強い。ええと、これは合ってる？　だから 2. の方が 2'. よりも強い主張で、うーん……。

2012-11-01 21:10:57

@YuishiYumeiji

@Taroupho 論理式をHeyting代数に持っていくと, a⇒bとはa∧c≦bを満たす最大のcと同じものです. また, a⇒bが真であることと, a≦bが真であることが同じことになります.

2012-11-01 21:15:50

@YuishiYumeiji

@Taroupho p≦q と仮定したとき max{c | p∧c≦r}, と max{c | q∧c≦r} のどちらが"小さいか"が, どちらが"強いか"と対応します. a∧b は直感的には min{a, b} と考えてもいいです.

2012-11-01 21:20:40

@YuishiYumeiji ハイティング代数キタコレ！　ありがたいのですが、頭がパンクしそうですｗ　ああでも、何となく分かりました、とりあえずぼくの書いていたこと自体は正しそうですね。

2012-11-01 21:37:34

@Taroupho 私が理解してないのかもしれませんが、、（あと記号がみつけられないのでわかりにくい説明ですみません）任意のxとして示せれば、x=0で成り立ちますよね？2が示せることになるので、普通の帰納法が示せるのではないでしょうか？

2012-11-01 21:19:47

@sakuranmocchi 一般に、φ(0)⇒ψ のとき {∀x. φ(x)}⇒ψ ですが、{∀x. φ(x)}⇒ψ だからといって φ(0)⇒ψ とは限らなくないでしょうか？　例えば φ(3)∧φ(5)⇒ψ であって φ(0)⇒ψ でない場合とか。

2012-11-01 21:30:59

失礼しました。私の勘違いでした。おっしゃるとおりですね。でも、帰納法は成り立たないと思いますがいかがでしょう。 1から2は展開できますが、任意のxとすると展開できないのではないかと。。 RT @Taroupho @sakuranmocchi 一般に、φ(0)⇒ψ のとき

2012-11-01 21:51:26

@sakuranmocchi そうなのです。ぼくもそう思うのですが、歴史的な論文にそんな間違いあるでなし、何か読み違えている箇所がある筈なのですが、どこか分からず困っている次第なのですね……。

2012-11-01 21:55:07

M.K @k_tumuji

横レス失礼します。自分も勘違いしていました。∀x.φ(x)⇒∃x.φ(x)とは違うということですね。失礼しました。 @Taroupho @sakuranmocchi

2012-11-01 22:11:44

@Taroupho 私が勘違いしたのですが、 (任意のA)→Bではなく、任意の（A→B) でしたらいえると思うのですが、かきぶりも違うと思うのでたぶんそんなミスではないですよね。なにも役にたてずにすみませんf^_^;)

2012-11-01 22:17:49

@sakuranmocchi 多分ちょっと違う感じなのですよねー。レスありがとうございました、お時間を取らせてしまいすみません。

2012-11-01 22:22:12

よし、その帰納法は成立しない！　直感通りそう考えるとして、論文の読み違えの方をさがそう。あー、お客様のなかにカット除去定理に（ｒｙ

2012-11-01 21:59:49

@Taroupho 横から失礼します。気になったのですが、2'∀yや、3∀xには、≠0という条件はありますか？無いのなら、3(x=0)で、k<0なるkは存在しないので、仮定は偽、よって∀yφ(0,y)が言える気がするのですが。

2012-11-01 22:03:22

@Taroupho 逆でした。「仮定は真」の言い間違えです。

2012-11-01 22:10:29

@zomi1202 えーっと、ちょっとすみません。頭が回ってないので御指摘の確認なのですが、それは 1∧2'∧3 から ∀x. ∀y. φ(x, y) が導ける、という意味なのでしょうか？　それとも、ぼくの書き方だと 1 を示す必要がなくなる、という意味ですか？

2012-11-01 22:18:06

@Taroupho それどころか、3だけから、∀x∀yφ(x,y)が言えてしまう様な気がします。多分、1,2が付いているところから察するに、≠0が付加（あるいは暗示？）されているのではと思いました。

2012-11-01 22:19:49

@zomi1202 ありがとうございます、了解しました。確かにぼくの書き方ではそうなっていますね。多分 ≠0 でよいのだとは思いますが、故意に抽象したので元の話に戻すのが……。だんだん疑心暗鬼になってきました。いずれにせよポカミスなのは間違いない筈なので！

2012-11-01 23:17:56

@Taroupho 仮に≠0ならば、多分φ(0,0)のみ成り立つ命題φ（例えばx^2+y^2=0とか）が反例になります。1の成立は自明として、「∀x. ∀k＜y. φ(x, k)」が偽なのでそれを仮定とした条件2'は成り立ちます。3も同様ですね。

2012-11-01 23:21:59

@zomi1202 ちょ、ちょっとすみません、おっしゃることは分かるような気がするのですが、その論法だと普通の数学的帰納法も成り立たないことになりません？　ごめんなさい、少々頭が回ってないので留保させて下さい……。

2012-11-01 23:57:28