正しいのになぜかみんなが「変だ！」という問題にPerlで答えてみた

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

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

Perlで解答するとこうだろうなあ。 perl -e 'for my $x(0, 1) { for my $y (0, 1) { for my $z (0, 1) { ($x && $y || !$x) || ($y && $z || !$y) or die } } }'
@hiratara

追記

まずこの問題はどういう意味かというと、任意の自然数について「x=3ならばy=5になる。あるいは、y=5ならばz=8になる。」は成り立つということ。例えば x = 10, y = 20, z = 30 としてもこの命題は成り立っている。

"自然数"とか"3"とか"5"とか"8"は「変だ！」って感じを出すためのダミーであって、この問題の本質は「P → Q ∨ Q → R」が恒真式になるかってこと。なので、P, Q, RのそれぞれについてTRUE, FALSEを当てはめた8通りを試せばよい。

P → Q は ¬P ∨ Q であることに気をつければ*1、以下のコードでチェックできる。

for my $x(0, 1) {
    for my $y (0, 1) {
        for my $z (0, 1) {
            (!$x || $y) || (!$y || $z) or die "not Tautology"
        }
    }
}
print "Tautology\n";

式で示せば、 P → Q ∨ Q → R = ¬P ∨ Q ∨ ¬Q ∨ R = ¬P ∨ ⊤ ∨ R = ⊤。

蛇足的追記

排中律が前提になってるのが許しがたい
@maophilia

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

@hiratara はいCoqでは排中律は使えないですが、自然数のdecidability(任意の自然数n,mは等しいか等しくないかどっちかである)は証明できますので

@maophilia

@maophilia 納得です。初心者なので古典論理で勘弁して下さい！
@hiratara

あー、全然気がついてませんでしたが、 Q ∨ ¬Q = ⊤ で排中律使ってますね。。。

*1:最初つぶやいた時はこの変形を間違えてました。。。