今日の収穫

「すべてのAはXXXである」という命題を証明するときに、より証明しやすくするために、より制約の強い「すべてのBはYYYである」という等価な命題に帰着して「すべてのBはYYYである」を証明するという方法がある。
特に、クラスAがクラスBを包含していて、「すべてのBはXXXである」を示せば十分という場合がよくある。
「すべてのBはXXXである」を帰納法で証明仕様とした場合に、帰納法の仮定をある部分Sに適用しようとしたときに、SがBに含まれる事を示す必要がある。
このSがAに含まれる事は自明だけどBに含まれる事は非自明だとめんどくさい。
今回のケースでは、「すべてのAはXXXである」から「すべてのBはXXXである」に帰着したのだが、「すべてのAはXXXである」を満たさない反例を考えたときに、その反例は必ずBに含まれることも示せる。
すると、「すべてのAはXXXである」を考えるときに、ある最小の反例Cを仮定すると、CはBに含まれ、その部分Sは最小性より「SはXXXである」ことが言え、帰納法の証明と同様にCが反例でないことを示して、矛盾を導くことができる。

どこか間違えているのかもしれないけど、"「すべてのAはXXXである」を満たさない反例を考えたときに、その反例は必ずBに含まれる" と "SがBに含まれる"が同じ働きをしているように見える。

ほかの人のできあがった証明では、こういったことが見えてくることは(あまり)ないので、非常に勉強になった。