- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
Gödelの不完全性定理についてのきちんとした証明（可証性述語を与えるところまでの膨大な構成），Chaitinの不完全性定理，Quineからの流れによるGrzegorczykの算術を介さない不完全性証明，その他のパラドックスの形式化，証明可能性論理などの諸々の話題をTypstでメモ書きすることにした
十分にサンプル自体はある筈だとは思うけど岩倉玲音(CV. 清水香里)の声をAIに突っ込んでBôa - Duvetを歌わせる動画って案外見たことがないな（手動でラグトレインを歌わせる試み( https://www.nicovideo.jp/watch/sm39295693 )はあるが）
真面目に考えたことがなかったけど日本語の索引は基本的に「あ行〜わ行」で作るから素朴にラテン文字での索引生成が使えないの不便すぎる
どのバージョンから入ったのかはいまいち追えていないがTypstにパッケージシステムが入ってうれしい！と思って文書を書いてNix内でビルドしようとしたら外部ネットワークに接続する必要があることを完全に失念していて今大変なことになっている
Typstで文書を書いている ここは楽しい おまえたちも早く来い
不完全性定理のスケッチが示された15年後にはQuineによって「算術というより連結という操作が良くない！」という洞察が得られているのあまりにも鋭いと思うし、その後Grzegorczykが取り上げるまで60年ぐらい下火だったっぽいの悲しすぎる（これは不確かな歴史です）
それぐらい出来てもらえないと困る、とは思うがLean4でおれが院試で要求されている線形代数、複素解析、微分方程式周辺ってMathlib無しで自力で形式化出来るのだろうか
うろ覚えだけども下の文よかったな（この分自体も誰かの又引きらしいが）
> 「すべての人に愛する人がいる」と「偶数は無限に存在する」は同じ論理構造であることに最初に気付いたのがFregeだった─
足立 恒雄『数とは何か そして何であったか』
1. シーケント内の論理式から任意の論理記号$を消すにはカット規則を使わざるをえない
2. カット規則無しでも証明できる
3. シーケントに$が増えるのは$右または$左のどちらかを使ったときにに限る
よって、結論のシーケントに$が入っていないなら$右または$左の両方を1度も使わずに証明していなければならない
Lean4プロジェクトのリポジトリをローカルに持ってきてコードを見ようとすると大抵Mathlib4に依存している部分の膨大な定理のビルドが走って大変時間がかかるがあれをNixとかで一旦ビルドしたものをキャッシュしてどうにかしてくれないのかというところに普及の鍵がある気もする
- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
