新しいものを表示
SnO₂WMaN さんがブースト

今lean4-logicで採用している方法では論理式0 = 1のゲーデル数は935319734277578879273555234912656324244635888525662333723386717104793974747307706000946757839613990108227396487674599112298224133835455479797684718532327704919669033277927248672439400930905780539310948141167795875680399885836866734847451791344024484329550631775805419608027972015818561000739343253563007945350184910033971876879754597654645132096911041199614874696969038805225053580411215684158738776904337761136760151729990515106646661045385956293637であることがわかった

SnO₂WMaN さんがブースト

lean4-logic, うまく行けば今年中にゲーデルの不完全性定理が示せそうという感じがある

「理論Tで証明できない命題があれば理論Tは少なくとも矛盾はしていない(逆に矛盾しているなら任意の命題が証明できるから)」という事実未だに非直感的すぎて慣れない

Auth0からのユーザ取得が確率的にコケるという意味不明のバグのせいで開発が全然進まない

Robinson算術が本質的決定不能かつZF集合論を解釈可能という事実などから行けるかと思ったけどこれから導かれるのは第1不完全性定理であって言明の第2不完全性定理ではないハズだから冷静に考えるとどうやって示すのかは知らないな モデル理論的な方法なのだろうか?

スレッドを表示

結局行くことが出来なかった若手による数理論理研究集会2023に証明可能性論理D(森岡 蒼; "証明可能性論理Dのモデルの拡張")についての発表があったが調べても出てこないためどういうものなのかさっぱりわからない

educ.titech.ac.jp/ila/news/202

東工大の教養卒論の優秀賞に趙 瑛希; "MADムービーは創作活動として認められるべきか"という謎の論文があり、これが指すものが我々のいうアレと同じものなのか気になる しかし学外の人間が読む手段は無い

 

twitter.com/SnO2WMaN/status/17

『涼宮ハルヒの憂鬱』の8話『笹の葉ラプソティ』の長門の台詞「無矛盾な公理的集合論は自己そのものの無矛盾性を証明できないから」、よりによってなんで公理的集合論の方を採用したんだ

Buchholzの第2不完全性定理の証明がドイツ語の講義テキストにしかないっぽいのどういうことなんだ

古いものを表示
Fedibird

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