2025.08.08
https://gyazo.com/449bcf25e47dbcdba264fcf9d98cdbe0
前：2025.08.07
後：2025.08.09
#日報
メモ
https://gyazo.com/e15c7ad48b0ee2ce6ccdd0fefa183aed
再帰的可算だが再帰的ではない集合から第1不完全性定理を導くを形式化した．
停止性問題は既にMathlib4にあるので言えてほしいのだが，N上ではないのでもう少し手間が必要だが，面倒なのでやってない．
メモ
https://prtimes.jp/main/html/rd/p/000000002.000113283.html
意味がわからない．PRTimesはこんなものを世に出さないでほしい．
それはそれとしてaspidaの開発者がおもいっきりトンデモになってるのｈは何なんだ
思った
モデル的な議論で証明できることがわかっている論理式の形式的証明を逆算する方法ってどうすればいいんだろう
もちろん証明探索すればいいというのはそうなんだけども…
そんなこと可能なのか？
$ \models \varphiなら$ \exists \mathcal{P}, L \vdash_\mathcal{P} \varphiが言える：$ L \vdash_\mathcal{P} \varphiは証明$ \mathcal{P}によって$ Lで証明可能，の意味．では$ \existsから具体的に構成するには？