Redundanz

僕の言葉は、人と話をするためにあるんじゃない。

0122

 数学の勉強をして、それからバイト。ダルブーの定理、そんな難しいこと言ってないやん。なんで昔引っかかったのだろう。頭が悪かったからというのはまあ、仕方ないとして。
 バイト先で問題を解いていて思ったのですが、P→Q ⇒ ¬P∨Q という定理、なぜか難し目の中学、高校数学でよく見かける。知ってて良いけども余り直感的でない命題として独り歩きしちゃってるのかしらん、みたいな。まあ真理値分析してみれば自明だし、良いのだけど。(僕が高校時代不勉強だっただけなのかな)そういえば真理値分析をするときに僕らが従っている理屈、これは数論の標準モデルということで良いのですかね。まあ述語論理とか理論とかいうものは主に証明を扱うものであり(ほんとか?)、それで問題ないはずなのだけど、ほら確かにそうなるだろうみたいなこと言われても、なー、とか。内包と外延が無限の彼方で一致するお話?とても頭悪いことを言ってしまった気がする。
 とりあえずさっきの命題はベン図書けば直感的にも理解できるのだから、それで良いとして。集合論と対応しない図式はあり得るか、みたいなことを考えます。逆のほうが多そうではあるのだけども。
 ちなみにさっきの証明は、仮定したP→QとPからQを導いて、それから¬P∨Qとして仮定した¬(¬P∨Q)と⊥、Pの仮定から¬Pを出してもう一度仮定した¬(¬P∨Q)と⊥、これで¬¬(¬P∨Q)から¬P∨Q、で良いのだっけ。証明のプロセス、結構抜け落ちてしまっている。何かと便利だからしっかり身につけておきたいのだけど。ゲンツェンシステムが公理として採用しているA→Aが、僕らの意味するところのAの仮定に対応する、みたいな話、非常にフェヨいなあと思います。何の話をしていたのだっけ。

 帰宅してから、Twitterの友人とワンナイト人狼なるものに興じました。まあ一夜限りの甘い人狼というやつで(少嘘)、よくわからないけども人心掌握術が全てでした。マイクの機能しなかった僕はタイピングで参加したのだけど、これだとどうもね。試験期間が終わったらもう一度やりましょうということになっているので、それまでにマイクをなんとかせねばなりません。そうそう、人狼をベースにした大規模なゲームを考えているのだけど、なかなか良いアイディアが浮かびませんね。何かテンプレになれたらと素敵よね。

 明日は英語一列の試験があるらしいので、少々勉強して寝ましょう。実験がないから、峠を越せば時間のある一日のはず。
 ああ、そういえばサークルの新歓期に歌う曲、soon ah will be doneになったらしくわくわくしています。意訳して僕はもうダメだ。かっこ良い曲です、楽しみ。