今日は…何をしたのか思い出せません、と言おうと思いましたが、そういえばやったことをちょっと思い出しました。
まずプロジェクトを開いて、閉じました。具体的にどう作業をするかが定まってない気がしたので、考える時間が必要だと思って。
で、それを考えるべきと思いつつ概念について思いを馳せたところ、それをscrapboxで管理することを思いつきました。
今「因果」とか「現象」みたいな項目がいっぱいあっていい感じです。まだ中身は薄いんですが、ちょこちょこ書き足してるのでそのうち使えるようになったらいいな、と思っています。
あと直観主義の話について色々考えていたんですがそれは後述。
で、Capが開催してくれたラ会の時間が来て、観て、あとはのんびりぶいちゃ。うーん。そんなものかもしれません、一日。
ラ、こう、やっぱりいいですね。特に今回は一公演並べてだったので「本質には関わらないが暗に示された文脈」を回収できた分がありました。とは言え既に見たものが多かったかも。おもしろいからね。
これについての色々考えたいことは今度に回すことになります。うん。
さて今日はどうしましょうね。とりあえず「やること」があるので主進捗は出せないんですが、テクスチャ…というか柄を考察するくらいはまたできるでしょうか。というか柄をちょっと描いた後で、私は既に簡単なスケッチをしていたことを思い出したわけですけど。自分の作り出したリファレンスすら見ないのはなんだか「物を参考にしたくない症」とは違うんじゃないかという気がしてきました。
たぶん、手癖に頭を使っていて物を参考にする余裕がないのではないでしょうか。するべきは模写な気がします。私模写って今までにやったことないんじゃないだろうか。やろうとしたことはあるが、できたことはないきがする。アナログでさえ、デジタルでさえ。やろうとしたことはどっちもあったはず。
絵の解析が足りないとどうすれば正解に近づくのかわからない気がするんです。そして解析が足りないことがわからないとどうしようもない。うーん。
小物…というかディティール強化月間みたいなのをやりたいと思ってるので、そこで回収しておきたい所存です。
まぁ、それはそれとして。
結局メインタスクをどう動かすのかが確定していないのでそれを考える必要もありました。そんな感じでいきます。
おまけ。
一般的に人類が信じている (ベースとしているという意味) 古典論理とは違う、直観主義論理という論理体系がありまして。
直観的でないことで有名 (冗談) なんですが、それの可視化を是非やりたいと思っているんです。それは Inter-action on the Math を作ろうとした初期の頃から構想がありました。
古典論理では「真」か「偽」の2通りについて考えることで概ね十分なわけですが、直観主義は「正しい証拠」について考えることになります。それは「正しい証拠が複数ある」とか「正しくない証拠が無いことは証拠にならない」みたいな帰結を生み、まぁ、複雑なわけです。でもいい子なんですよ。まぁそれはおいといて。
これを可視化する為の方法として純粋に「何と何が等しい意味を持つか」「何なら何が成り立つか」みたいなことを表示することが考えられます。が、上の理由によってそれは簡単ではありません。
そこで割とよく (分野内で) 知られている Rieger-Nishimura lattice という構造をどうにか綺麗に表示することを考えました。これは「pという事象しか無い世界で展開される直観主義論理の世界」です。
古典論理では明らかに「pが正しい」「pは正しくない」のどちらかしかありません。ですが、直観主義では「何もわからない」「pが証明できる」「pが正しくないことが証明できる」「pが正しいかpが正しくないかのどちらかは証明できる」から続いて無限に可能性があることが…知られています。
で。これは割と理解ができる構造をしているんです。いや、まぁ、理解していると思ってたけど理解していない部分はありました。が、今日いろいろ調べていてやっと理解した部分がありました。
今日の参考文献です。自分のメモ用。
つまり「pしかない」ならうまくいきます。けど、それってなんだかもったいないですよね。p∧qくらい書きたいじゃないですか。
古典論理で「pとqがある世界」を展開すればたった4通りで十分なのは知られている通りです。けど、直観主義論理でこれをやろうとすると、こんなことになるようです。
無限に続く最初の2段階でこれです。2段目までは真面目に計算した結果ですが3段目は意味わからないので適当ですけど。根本的にはくらいで要素が掛かってきそうなのが問題なのです。
この事実を今回いろいろ知って始めてわかったわけですが、まぁ、なんか可視化するにはだいぶしんどそうです。はい。
…とはいえこの「道をつくるルール」そのものは単純なので、その意味とかを完全に理解していればそれごと可視化することで膨大な計算をやめることは…できるかもしれません。
今回は表層的に文献を読んだだけなのでそこまではわかりませんが。まぁ可能性の一つです。
この話は本当に前からずっとやりたくて、「できる」ことも「できない」こともわからなくてずっともやもやしていたわけですが、今回やっと「しんどいことがわかった」のでよかったです。とても。もやが無くなったので今後の時間の消費が減るわけです。やったね。
いつか IotM に追加したいね。
おわり。
