2023.11.01
https://gyazo.com/535b02ede8b2c59790a96be3a8f515dc
Hilbertの無限ホテル
前：2023.10.31
後：2023.11.02
#日報
知った
Frutiger Metro
https://scrapbox.io/files/65423e2c8ec81d001b42b62b.webphttps://scrapbox.io/files/65423e30cbccf0001bb5cb99.webp
Memo
https://ja.wikipedia.org/wiki/日本空間_(位相空間論)
ポーランド空間 / 日本空間
ポーランド空間は日本空間である。
思った
今日読んだ論文はLecture Notes in Artificial IntelligenceのオープンアクセスのTABLEAUXという雑誌の中にある
のでpdfを分割したいのだが…
普通にコマンドラインでやらずにWeb上のやつでやってしまった．
まっとうな手段ってあるのか？
様相論理GLS(SはSolovayによる)と証明可能性論理GLのシーケント計算体系GLS(SはSequent Calculi)があるのありえなさすぎる
https://twitter.com/SnO2WMaN/status/1719619706943160578
普通にありえないだろ
読んだ
R. Gore, R. Ramanayaka, I. Shillito; 2021; "Cut-Elimination for Provability Logic by Termination Proof-Search: Formalized and Deconstructing Using Coq"
I. Shillito, I. van der Giessen, R. Goré, R. Iemhoff; 2023; "A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised"
SnO2WMaNというハンドルネームは相当ありえない表記（間に数字が入っている上にアルファベット大文字小文字が入り乱れている）とは思っているが、証明論の証明体系に同じ感じの名前の体系(G4iSL)があって親近感が湧いている
直観主義証明可能性論理iGLの為のシーケント計算体系$ \sf G4iGL
Strong Löb Logic$ \sf SLという論理の直観主義バージョン / Intuitional Strong Löb Logic$ \sf iSLのためのシーケント計算体系$ \sf G4iSL
一番長いバージョンはTerminationをする前なので$ \sf G4iSLtとなっている．