SnO₂WMaN @sno2wman@fedibird.com

日報(2023.07.31)

https://scrapbox.io/sno2wman/2023.07.31

日報(2023.07.30)

https://scrapbox.io/sno2wman/2023.07.30

日報(2023.07.29)

https://scrapbox.io/sno2wman/2023.07.29

ZenMLの中で埋め込むことを意図して設計されているのとMathMLに対応していないのもあってZoticaの採用は見送っているけど、Scrapboxでのメモ書きではなくちゃんとした数式入り文書を書きWeb上でHTML+CSS上で普通に見られる（pdfではなく！）という欲求があり、どうにかしている [参照]

Cirno's complete mathematics class

逆に今から不完全性定理の意味での"(in)completeness"（統語論的(不)完全性）を"(im)perfectness"に置き換える

https://github.com/Ziphil/ZenmlZotica/blob/136a91d9f58438e13666e3dbce3a4f2907f3e35a/test/file/sample.zml#L584-L600

Ziphil氏がメンテナンスしているZenML及びZotica、下のような証明図が比較的?簡潔かつ直感的に記述出来るのいいなと思う

https://ziphil.github.io/ZenmlZoticaDemo/

XMLの`<?xml ...>`部分がprologという名前なのややこしすぎる

Lean4の内部実装ってpartial多くていいな

日報(2023.07.28)

https://scrapbox.io/sno2wman/2023.07.28

世界の複雑さに耐える

アルゴリズム的複雑さにも耐える

今日やったこと:

Chaitinの不完全性定理に抜き打ちテストのパラドクス的な見方を加えると第2不完全性定理と同じ主張が得られるという論文の証明を追い、実際得られたのでおもしれ〜！と思った

https://arxiv.org/abs/1011.4974

https://scrapbox.io/sno2wman/Krtchman_S.,_Raz_R.,_"The_surprise_examination_paradox_and_the_second_incompleteness_theorem"#64c2436a13a15800006c8c42

日報(2023.07.27)

https://scrapbox.io/sno2wman/2023.07.27

Girardの論文でフとヲを使っているのをチラ見したことがあるがこれらが何を指しているものなのか及びなぜこの記号で導入したのかはよくわかっていない

https://girard.perso.math.cnrs.fr/trsy4.pdf

ありがとうございました！

https://mstdn.jp/@palalansouki/110780132085245415

https://bi.cbult.space/objects/245ba11d-0ea2-416b-96f7-d4e0ad0be0e2 [参照]

@elpinal

こういう話です．言葉足らずで申し訳ありません

https://fedibird.com/@sno2wman/110779681768923884 [参照]

話をちゃんと整理しました　ずっと解けないので誰か解いてみてください

https://scrapbox.io/sno2wman/2023.07.27#64c0dc0a13a15800006c8be4

驚くべき帰結2こと`(¬φ → φ) → φ`は排中律と同値らしいのだが全然解けなくて普通に怒りに満ちた帰結2になってる