新しいものを表示

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

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

github.com/Ziphil/ZenmlZotica/

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

ziphil.github.io/ZenmlZoticaDe

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

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

世界の複雑さに耐える

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

今日やったこと:

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

arxiv.org/abs/1011.4974

scrapbox.io/sno2wman/Krtchman_

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

girard.perso.math.cnrs.fr/trsy

SnO₂WMaN さんがブースト
SnO₂WMaN さんがブースト
とりあえず最小論理の自然演繹体系での証明を画像で上げます。ヒルベルト流はあまり詳しくないんですが、含意周りをS,Kでやるとたぶんいい感じになったと思います

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

開発機と運用機が別れていないためおれがMathlib4の適当なファイルを開いてもし証明が非常に複雑だった場合はCPU使用率が100%になってOtoMADB側のAPIが重くなるというメチャクチャな事態でずっと生きている

現状ではVSCodeに限って言えば(Emacs等他はどうかは知らない)Nixの例えばdevshellなどが上手くVSCodeと上手く噛み合ってくれるかはかなり微妙で多分出来ておらず,おとなしくelanを入れるか,どうしてもクリーンな環境を保っておきたいならdevcontainerとかを使うのが良いと思う(Mathlib4のものを参照)

github.com/leanprover-communit

古いものを表示
Fedibird

様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。