Aに向ってBと呼びかければ、Aは同じ鳥Bの名を呼びもどすかもしれない。 その場合、鳥Aは鳥Bが好きであるという。 記号だと、AB = Bあらゆる鳥はすくなくとも一羽の鳥が好き。coqで。 Theorem any_bird_is_fond_of_least_one_bird : forall A, exists B, B = …

ひいた。正月そうそう縁起が悪い。

鳥xは自分自身が好きであれば、すなわちxのxへの応答がxであれば、自己中心的と呼ばれる。 記号的には、xx = x である。結合条件とものまね鳥がいる条件のもとで、少なくとも一羽の鳥は自己中心的であることを示せ。coqで。とりあえず。 Theorem there_is_eg…