2025.11.11
https://gyazo.com/0e51c9c900b327a881ed2a1d66ffbd82
思った
酒を飲む人は自分の頭の中にあるやってはいけなかったり言ってはいけないことリストの制限を勝手に緩めるギャンブルを常にしててすごい．ジブんいは分の悪い賭けだ
思った
思った
https://gyazo.com/0f9185e437155f5897609840d9df7c9b
自然演繹を形式化しようと思ってやってみたけどこの形になる気がするから勝手にBHK解釈っぽい感じになってそれはそうなんだけど驚いてる ところでこれは定義出来ない．どうすれば上手く定義出来るんだろう
初心者用の論理学入門記事のために自然演繹で導入している（各規則の正当化の自然な説明が出来るという意味で自分も書きやすい）と思っていたけど、別に→導入とかCurry-Howard同型対応的なことに触れずにどうやって正当化して書けばいいのかわからないから普通にHilbert流で導入したほうが良い気がしてきた メモ
論理学の既存の事実をを形式化することに何の意味があるのか？と思ったがやはりカタログを作れるというだけでも十分なヴァリューがある用に思える．
思った
Visserの論文，簡単に，という部分はそんんなに簡単ではないように思えて，実際やってみるとそんなに難しくない，みたいなことがある ．？