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

k @mathink

@tmiya_ @hyuki @katayama_k 横からですが,御参考までに. http://t.co/QFgJmQtQ

Hiroyasu Kamo @kamo_hiroyasu

@y_bonten あ、ごめんなさい。鹿島先生の教科書に載っているのは NJ + (A→B)∨(B→A) でした。

Takashi Miyamoto @tmiya_

@mathink @hyuki @katayama_k おー。これは確かに Q に対する排中律が必要で古典論理で無いと駄目ですね。 Theorem really_strangeness: forall P Q R: Prop, (P -> Q) \/ (Q -> R).

片山 功士 @katayama_k

@mathink @tmiya_ @hyuki なるほど、「自然数の等式で構成された命題」のような前提がなければ排中律が必要になるんですね。勉強になります。

Hiroyasu Kamo @kamo_hiroyasu

ぼけてました。NJ + (A→B)∨(B→C) ≡ NK です。(A→B)∨(B→C) はその意味で面白いのでした。

Hiroyasu Kamo @kamo_hiroyasu

@koyama41 実は、(A→B)∨(B→C) から一瞬で A∨￢A が出てくるんです。(￢⊥→A)∨(A→⊥) の形で。