「x,y,zを自然数とする。このとき、x=3ならばy=5になる。あるいは、y=5ならばz=8になる」をめぐって

新井紀子/ Noriko Arai @noricoco

正しいのになぜかみんなが「変だ！」という問題：　x,y,zを自然数とする。このとき、x=3ならばy=5になる。あるいは、y=5ならばz=8になる。

新井紀子/ Noriko Arai @noricoco

@hyuki どういう？でしょう？

結城浩 / Hiroshi Yuki @hyuki

@noricoco あ、わざわざすみません。歩きながら読んでいて意味がよくわからなかったのですが、いま落ち着いて考えてみると、確かにこれは正しいですね。おもしろい問題です！ありがとうございました。

結城浩 / Hiroshi Yuki @hyuki

これは良問！さすが @noricoco 先生 > RT

新井紀子/ Noriko Arai @noricoco

@hyuki 気に入ってもらえて嬉しいです(^^)

ただまご = 永島孝 @tadamago

@noricoco (x=3→y=5)∨(y=5→z=8) が恒真との趣旨でしょうけれど，そのようには読みにくい．「y=5になる。あるいは、」と記してるので，文がそこで切れてると思ってしばし考えてしまいました．句読点の難しさですね．

新井紀子/ Noriko Arai @noricoco

@tadamago いろいろなバリエーションで誤読がないように書いて試したのですが、どの場合でもおおむね「変だ！」と言われます。たぶん、レレバンスの問題だと思います。

hiratara @hiratara

正しいのになぜかみんなが「変だ！」という問題をPerlで答えてみた http://t.co/t30mvd1A

結城浩 / Hiroshi Yuki @hyuki

. @noricoco 先生による良問に @hyuki が蛇足の説明を付けました⇒「x,y,zを自然数とする。このとき、x=3ならばy=5になる。あるいは、y=5ならばz=8になる」この命題は常に成り立つのですが、そのことを納得 and/or 証明できますか。

k @mathink

証明しろと言われたらー #Coq でやるがー 王道よお http://t.co/QFgJmQtQ

結城浩 / Hiroshi Yuki @hyuki

（自然数と言わなくてもいいような気がしてきた）

ヽ|・∀・|ノ @i_am_a_youkan

@hiratara Coqだと、forall (x y z:nat),(x=3 -> y=5) \/ (y=5->z=8)は証明できるけども、forall (p q r:Prop),(p->q)\/(q->r)は証明できないので、これはダメです！

Hiroyasu Kamo @kamo_hiroyasu

@hyuki ちなみに、(A→B)∨(B→C) が胆で、それを根拠づけるのに A→B ⇔ ￢A∨B を持ち出すのは牛刀です。出題者は当然ご承知でしょう。

新井紀子/ Noriko Arai @noricoco

そのことを納得 and/or 証明できますか。 @hyuki ほんの少しバリエーションを加えたら自分もきっと気づかないです。

結城浩 / Hiroshi Yuki @hyuki

@kamo_hiroyasu そ、そうなんですか…（しばらく考える）… Bは真か偽のいずれか。Bが真ならA→Bが真。Bが偽ならB→Cが真。よって(A→B)∨(B→C) は恒に真。…これで済む。ということでしょうか？

結城浩 / Hiroshi Yuki @hyuki

@noricoco そうですか…（こういうことが可能かどうかわかりませんが）もしも法律上の文言に悪用されたら嫌ですね^^;

k @mathink

ちなみにさっき #Coq でやった証明では排中律入れてわかりやすくしましたけど,"自然数"って括りがあるので実は必要ありません.

Takashi Miyamoto @tmiya_

Coqで証明。eq_nat_dec使用。 http://t.co/eyjr6KMo QT @hyuki 「x,y,zを自然数とする。このとき、=3ならばy=5になる。あるいは、y=5ならばz=8になる」この命題は常に成り立つのですが、そのことを納得 and/or 証明できますか。

結城浩 / Hiroshi Yuki @hyuki

@tmiya_ へ、へえ…こんなふうになるんですか。Coqについてはまったくしらないんですが、eq_nat_decというので y が 5に等しい場合と等しくない場合の場合分けをしているのかなあ…と想像しました。

Hiroyasu Kamo @kamo_hiroyasu

@y_bonten はい。NJ + (A→B)∨(B→C) は面白い体系です。鹿島先生の教科書の11.4節に出てきます。http://t.co/LrsVftDQ

Takashi Miyamoto @tmiya_

@halcat0x15a あー、specialize (...); intro; destruct H. しなくても直接 destruct (...) の方が簡潔で良い証明だと思います...こっそり直そうかな。

k @mathink

直観主義論理では証明できない,という言明はメタなものですわね. Coqよりもメタ.

片山 功士 @katayama_k

@tmiya_ @hyuki eq_nat_decは、型を自然数に限定するなら、任意のm nについて、m=n ¥/m<>nが直観主義の立場からも認められることを意味している、ということでしょうか？

片山 功士 @katayama_k

@tmiya_ @hyuki よく考えたら、二つの自然数が=か<>かというのと排中律とはまた別の話ですね。

Takashi Miyamoto @tmiya_

@katayama_k @hyuki 端的に言うとm=n ¥/m<>nの判定は構成的に判定できるので排中律の助けを借りなくてOKです。nat (=Peanoの自然数)は帰納的に定義され、帰納的に定義されている型の値は場合分け可能なのでその手の判定が出来る、ということだと思います。