- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
ZenMLの中で埋め込むことを意図して設計されているのとMathMLに対応していないのもあってZoticaの採用は見送っているけど、Scrapboxでのメモ書きではなくちゃんとした数式入り文書を書きWeb上でHTML+CSS上で普通に見られる（pdfではなく！）という欲求があり、どうにかしている [参照]
Cirno's complete mathematics class
逆に今から不完全性定理の意味での"(in)completeness"（統語論的(不)完全性）を"(im)perfectness"に置き換える
Ziphil氏がメンテナンスしているZenML及びZotica、下のような証明図が比較的?簡潔かつ直感的に記述出来るのいいなと思う
XMLの`<?xml ...>`部分がprologという名前なのややこしすぎる
Lean4の内部実装ってpartial多くていいな
世界の複雑さに耐える
アルゴリズム的複雑さにも耐える
今日やったこと:
Chaitinの不完全性定理に抜き打ちテストのパラドクス的な見方を加えると第2不完全性定理と同じ主張が得られるという論文の証明を追い、実際得られたのでおもしれ〜！と思った
Girardの論文でフとヲを使っているのをチラ見したことがあるがこれらが何を指しているものなのか及びなぜこの記号で導入したのかはよくわかっていない
SnO₂WMaN
さんがブースト
@sno2wman p ∨ ¬p → ⊥ を仮定するとp → p ∨ ¬p, だから p → ⊥, よって p ∨ ¬pが証明できる（と思う）
https://scrapbox.io/kokuritsukouen/%E6%8E%92%E4%B8%AD%E5%BE%8B%E3%81%AFHPM_+_CM%E2%82%82%E3%81%A7%E8%A8%BC%E6%98%8E%E5%8F%AF%E8%83%BD
SnO₂WMaN
さんがブースト
@sno2wman とりあえず最小論理の自然演繹体系での証明を画像で上げます。ヒルベルト流はあまり詳しくないんですが、含意周りをS,Kでやるとたぶんいい感じになったと思います
話をちゃんと整理しました ずっと解けないので誰か解いてみてください
https://scrapbox.io/sno2wman/2023.07.27#64c0dc0a13a15800006c8be4
驚くべき帰結2こと`(¬φ → φ) → φ`は排中律と同値らしいのだが全然解けなくて普通に怒りに満ちた帰結2になってる
開発機と運用機が別れていないためおれがMathlib4の適当なファイルを開いてもし証明が非常に複雑だった場合はCPU使用率が100%になってOtoMADB側のAPIが重くなるというメチャクチャな事態でずっと生きている
現状ではVSCodeに限って言えば（Emacs等他はどうかは知らない）Nixの例えばdevshellなどが上手くVSCodeと上手く噛み合ってくれるかはかなり微妙で多分出来ておらず，おとなしくelanを入れるか，どうしてもクリーンな環境を保っておきたいならdevcontainerとかを使うのが良いと思う（Mathlib4のものを参照）
https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer
- site
- https://sno2wman.net
- Scrapbox
- https://scrapbox.io/sno2wman
- https://twitter.com/SnO2WMaN
- GitHub
- https://github.com/SnO2WMaN
嘘つきのパラドクス
2022年 11月 に登録
