カフェラテ カフェモカ カプチーノ
目標をセンターに入れてスイッチ
明後日に世界は滅亡するが、同時にそっくりな別の世界が誕生するため、私たちは滅亡したことに気づくことができない
良いスペックの PC を買った理由の半分くらいが定理証明支援系だったのに、購入以降一度も触っていない
人生
事務作業を終えた
deep research の結果、今回は全体的に ChatGPT くんのほうがよさげだった、Gemini くんも直接関係があるかはわからないが気になる文献を一つ出してきたのでよしとする
研究室の大変優秀な先輩が人と人をつないでくださっていてとてもありがたい
shushing
9/30 [東京] ちょこっと団 《女子大生が独特なズレを醸し出す》 【ナイスアマチュア賞】 - YouTube
うー
Gemini くんがエラーを吐いたので再挑戦
これは deep research の途中で突然ペルシャ語？をしゃべりだした ChatGPT
いまやっていることの関連文献がないかを Gemini と ChatGPT の deep research に投げてみた。どうだろう
あ、ヤバ、オンラインのセミナー出るの忘れてた
何事も慣れの影響は極めて大きい
大きな声で ピリカピリララ
微妙にお腹が痛くて 3 時間くらい家の中を歩き回っている
心身の健康管理ですよやっぱり
そして毎週 Toggl Track の Weekly Overview が来たタイミングでここで反省会をする
とにかく最遅就寝時刻 02:00・起床時刻 10:00 を徹底しよう、これを 7 月の目標とする
だめだー
デジタル隠居
うおー、今日は疲れたので早く寝ようという気持ちだったのにもうこんな時間
ということで、長文で考えごとをだらだら書いてみるテストでした
むしろ、面白いのは、素直に意見という概念を受け入れる、いわば保守的な立場が成り立つ仕組みのほうにあると思う。こういう立場では、普遍的な正しさを判断する理性に先立って、私たちはなんらかの超越的枠組みの中にいる。そして、この枠組みが、「正しさ」よりももっと基礎にあり、したがって、それぞれの枠組みに相対的な正しさに基づいて「意見」が生まれる。意見が依拠する超越的原理は、普遍的真理を追究する理性の対象範囲の外にある。
胡桃ふゅさん北朝鮮！？と思ったら韓国から北朝鮮を望むスポットがあるのね
とてもすごい成果を上げているとてもすごい人々が職に苦労している話を聞いて、えー……って感じですよもう
研究倫理教育みたいなやつを終わらせた、偉い
今日で 6 月終わりか
シャロさん
ヴァンパイアガール
人が多すぎるので帰ります……
ズガガガガ
「フレーゲの授業って 3 人くらいしかいなかったようなのでそれに比べればまあ」
無矛盾性と同じで、正規化定理やらなんやらは最後は「信じる」しかないという立場ですよね、おそらく
あ～、原論文にそういう正当化がついているのか、まあそれならなるほど
突っ込みを全部ここに放流することで解消するメソッド
judgemental equality の規則は型がついていること以外はふつうのロジックと同じでは
別に全称・存在量化を依存型で見るのは Martin-Löf に始まったことではないと思うけど、それをプリミティブに置く哲学的正当性みたいなのを気にしているのか
Martin-Löf は definitional equality と judgemental equality を区別しているのか
W-type なにもわからないの良くない気がしてきた
MLTT は型の等しさは本当はむしろ入れたくなかったんじゃないのという感じもあるけどなあ。等しさが分裂してる時点で、"no entity without equality" の思想かは怪しいんじゃないか
だからこそ HOTT に興味がある
Brouwer 的な等しさの概念は MLTT / HoTT では完全にキャプチャーできてないと思うんだよなあ