直観主義，背理法と否定の導入

平泉 @hrizm_math

証明図を書く練習をちっともしてないのがバレるけど、もしかしてA \rightarrow B ⇒ \not A \vee B の証明って直観主義でできない？

平泉 @hrizm_math

NJでやろうとするとA \rightarrow BからB出そうとしてA仮定するけどAがキャンセルしなくて死ぬ

平泉 @hrizm_math

しかしAの上で排☆中☆律を使うとそっから上が全部キャンセルして幸せ

平泉 @hrizm_math

ちなみにLJで証明を試みても同様に式の右側に論理式を2個並べないといけなくて死亡

鏡 弘道 @kagami_hr

A → A を考えるとだめそう。

@ta_shim_at_nhn

@hrizm_math 既にかがみさんが B に A を代入すればダメそうということを指摘していますが、ひらいずみさんが書いた方針をきちんと述べることで LJ のカット除去定理を根拠にして LJ で証明できないことが示せます。

平泉 @hrizm_math

@ta_shim_at_nhn 鏡さんのツイート見逃してたかもしれません。言われてみれば確かにそうですね。ありがとうございます。

V-alg-d（ZZ） @alg_d

「直観主義，背理法と否定の導入」をトゥギャりました。 http://t.co/vb0M7yqg 両方の流派知らない人割といるのか。

V-alg-d（ZZ） @alg_d

脳子さんしか追ってないので出来が悪い。

@ta_shim_at_nhn

@alg_d 多分あとこれくらいが関連するツイート。 http://t.co/B8LY6fwZ