固定された投稿

Gödelの不完全性定理についてのきちんとした証明(可証性述語を与えるところまでの膨大な構成),Chaitinの不完全性定理,Quineからの流れによるGrzegorczykの算術を介さない不完全性証明,その他のパラドックスの形式化,証明可能性論理などの諸々の話題をTypstでメモ書きすることにした

github.com/SnO2WMaN/incomplete

固定された投稿

このアカウントでは

- 論理学に関する様々な話題
- 命題論理あるいは様相論理の諸々の結果のLean4による形式化の進捗
- 開発中の音MADのデータベースOtoMADB(otomadb.com)の進捗
- 日報

などが放送される予定です。よろしくおねがいします。

標準様相論理の強完全性定理のコミットがマージされた.今後は有限モデル性などを示す予定.

github.com/iehality/lean4-logi

SnO₂WMaN さんがブースト
SnO₂WMaN さんがブースト
SnO₂WMaN さんがブースト

アドベントカレンダーつくった!何でも良いので書いてください

adventar.org/calendars/9022

SnO₂WMaN さんがブースト

この前の様相論理の記事の続きを書きました

様相論理: 可能世界意味論(1階述語論理) - liewecmays
liewecmays.net/articles/modal-

Gödel-Mckinsey-Tarskiの定理を直観主義命題論理=S4だけでなく古典命題論理=S5などにも一般化できる事実を知らなかった

liewecmays.net/articles/modal-

証明可能性論理の形式化のために最近少しずつやっているが,可証性述語が存在する算術が不動点補題を満たし導出可能性条件/形式化された完全性定理などを満たすならば,不完全性定理やLöbの定理などが証明できるという事実をLean4で形式化していた(どうやって可証性述語をとったりそのような条件を満たすかを示すかは一切触れていない)

github.com/SnO2WMaN/lean4-moda

松本『復刊 数理論理学』には様相論理の入門編があったが古すぎてLewisのS1~S5ベースで議論しておりKripke意味論とかについて一切触れていなくてすごかった

(Taitの?)片側シーケント計算が結局の所どういう点で証明論的な分析や形式化において良い点があるのかをいまいち把握出来ていないのと、様相論理のシーケント計算におけるそれの文献は遥かに無さそうという点で迷っている(GLのTait計算は見たことがあるが論文は結局読めていない)

link.springer.com/book/10.1007

> M. Fitting; "Types, Tableaus, and Gödel’s God"

Gödel Godが何かは知ってはいるけど、それにしても並べられると字面が物騒すぎる

Boolosによると「第2不完全性定理を用いたLöbの定理の証明」は1966年のKripkeに帰するらしくKripke何でもやりすぎと思った

多分これなのだろうけどJaparidzeがDzhaparidzeともスペリングされるのでわけがわからないことになっている

scrapbox.io/sno2wman/可証性論理D

スレッドを表示

冬はG.Boolos; "The Provability of Logic"をチビチビと読んでいこう

OtoMADBの開発をしたい一方で、算術的完全性定理の証明(いまだにわかっていない)や証明可能性論理の発展的な話題にも触れたいというジレンマに挟まれて大変なことになっている
少なくともOtoMADBがクローンしてdocker compose up -dなどを済ませればローカルでも動かせるような環境であれば他の開発者(いるのか?)もコントリビュートしやすいとは思うが、現状そうなっていない、主にAuth0周りが原因で…

Youtubeの音MADをWeb側からも登録できるようになった これも皆さんには関係のないことではありますが…

古いものを表示
Fedibird

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