最近マシンの電源をオフにしている間は時計が止まってしまうようになったので、起動時に自動で同期したいという需要が発生しました。なんか調べて出てきた通りにやってもうまくいかないなあと思ったら、デフォルトでは 15 時間以上時刻がずれている場合には…

{\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} 最初は \mid\hspace{-5}= などとしていたが、左の縦棒が出力されず、ついカッとなってやった。悪いことをしたとは思っていない。

細かいところはだんだん書くのが面倒になってきたので気になった部分だけ informal に。わりと技術的なところからくる動機づけがあって、実はそれが counterpart theory という古くから考えられてきた話と関係がありそうだという展開。*1 代入の問題 前節で…

この間読んでよくわからなかったところを再読。 10.2 The need for the continuity axiom geometric morphism が適当な条件を満たすと epi-mono factorization を使って past modality も定義できる。そのように定義された様相 は (continuity) は満たすが、…

重箱の隅に残ったごはんつぶ、二粒目。昨日の話と同じ設定で、次は同値。 で が valid 証明は、地道にやればできると思いますよ。valid なら条件を満たすほうは とか とかして背理法を使うといいと思いますよ。

やったからといって特に何があるわけでもないけど、気になるので重箱の隅に残ったごはん粒をつつくお仕事。 問題 直観主義様相論理の Kripke semantics では、定式化によっては次の公理が必ずしも真になりません。 で、この二つの公理のうち一方だけが真にな…

後でやろうと思っていた hyperdoctrinal model による Kripke model の再構成をやってみました。少しは理解が進んだと思いたい。 元になる意味論 constant domain model が与えられたとき、 が定義される。ここで W は集合、R はその上の関係 D は集合 I は…

このあたりから数学的にハードに感じるようになってきました。基礎体力が足りませんね。しかしここで頑張らなければいつまで経っても成長しないことがこれまでの幾多の経験から実証されているので頑張る。 10.1 Geometric morphisms and modal logic とりあ…

少し時間ができたので "Handbook of Modal Logic" 再開。9.1 は言葉の準備。なんか de Bruijn level っぽい表記を導入している様子。で自由変数が高々 n 個の term/formula を n-term/n-formula と呼ぶ、と。簡単に言ってしまうとそれだけのことのような。 9…

興味のある人は滅多にいないでしょうが、真面目に調べたので自分用にメモ。直観主義様相論理の birelational Kripke semantics では ◇ の解釈のしかたに何通りかのバリエーションがあります。これまでに見たことがあってすぐに思い出せるのは の三つ。下の二…

間がちょっと飛んで part 2 の途中、Section 8 から。Section 5 は参考文献リストがメインだし 6 は Part 2 への導入なので飛ばしたのは 7 だけですが。この節は first-order modal logic の Kripke-completeness について……なのですが、どうやら constant d…

この節は hybrid logic を first-order にする話。特別興味があるわけではなかったので軽く流し読みして済ませてしまいました。hybrid logic というのは様相論理に特定の世界でだけ真になる命題変数を付け加えた論理です。この命題変数を nominal と呼びます…

個体の解釈が可能世界ごとに違う意味論。単に object の解釈を世界に依存するように変えるだけかと思ったら、そうではなくて object と intention の二種類の sort を用意してます。 syntax intention variable (i, j, ...) が新たに term として加わります…

なんか Section 15 を読んでみたときのまとめが下書きに残っていたので公開しときましょう。余代数は代数の双対なのだけど、単純に双対をとるだけで対応するわけではない。実際これまでに扱ったような話では、必ずしもすべてが双対で対応付けられているわけ…

"Handbook of Modal Logic" の Chapter 9, First-order Modal Logic 読んでみようかなと思いました。Section 2 からが技術的な話。 意味論の定義 この節では、簡単な axiomatization をもつ三種類の意味論を与えています。 constant domain semantics: indiv…

代数の variety に対応する、余代数の covariety の話。HSP theorem の余代数版をやります。ちなみに実際に本を読んでいるときは、図式を大量に描きながら計算しています。 homomorphic images 代数と同様に余代数にも準同型像というものが考えられる。定義…

昨日の続き。Ω は set functor で (や、その添え字のついたやつら) は Ω-coalgebra とします。 relation lifting ここからさらに圏論の香りが強くなります。嬉しい。関係 の relation lifting とは、図式 を Ω で写した から定まる の像のこと。これを と書…

代数の congruence に相当する bisimulation と behavioral equivalence について。圏論っぽい雰囲気が漂っていて楽しい節です。ほとんど set functor ですけど。*1以下、特に断らないかぎり Ω は set functor で は Ω-coalgebra とする。添え字や prime が…

終余代数 (final coalgebra) の基本的な話。終余代数とは、余代数の圏の終対象のこと。関手を fix するごとに定義される。理論はだいたい知ってるので例を中心に見ていく。 some examples black box machine . M が機械の内部状態で C が出力。状態遷移を起…

余代数の入門。基本的な定義と例だけです。代数が演算子を計算することで構造を簡単にする仕組みを持っている (e.g. 1+2+3 -> 6)のに対して、余代数は単純なものを分解して構造を作り出す仕組みを持つ対象である、というようなことが書かれています。こんな…

8.1 が tense logic で 8.2 が global modality & discriminator varieties というタイトル。詳細はフォローしないで軽く目を通しただけです。8.1 では、tense logic の future modality と past modality から adjoint が作れて、その結果これらの様相は必…

7.5 Canonical equations "Time to harvest."ようやく目的であった canonical equation の話になりました。でも細かいところはフォローしていない。等式を考えるので term が出てきます。代数を与えるときには term に現れる関数記号と代数の演算は一対一に…

7.4 Composite maps 今度は関数合成と canonical extension が可換になるかどうかという話。位相的な特徴づけをします。まず使う位相の定義。ブール代数の canonical extension の上で次の位相を考える。 : up-directed joins で閉じた down-set が閉集合 (S…

7.1 Introduction Section 7 は canonical equation の話。等式が canonical であるというのは、それがある BAO で成立するとき、その embedding algebra でも成立すること。論理の方では Kripke completeness に関係する。 7.2 Canonical extensions of Boo…

Section 6 Logics and varieties の続き。 6.3 Interpolation 基礎論サマースクールで聞いたような話。Craig interpolation proporty と superamalgamation property が対応する。superamalgamation から interpolation は Lindenbaum-Tarski algebra を考え…

Section 5 Frames and algebras の続きと Section 6 Logics and varieties の一部。 5.6 Class operations complex algebra をとる関手 と ultrafilter frame をとる関手 の関係について最初に触れられている。 これらの関手はいずれも全射を単射へ、単射を…

Section 5, Frames and Algebras. 途中 5.5 まで。 5.1 Introduction 有限な BAO に対し atom の集合の上にで関係を定義して frame を作ることができる。また、有限な frame が与えられたとき、その冪集合上に BAO の構造が自然に入る (complex algebra)。こ…

Handbook of modal logic の中にある "Algebra and Coalgebra" という章を読んでます。http://staff.science.uva.nl/~yde/papers/ac.pdf に、だいたい同じ内容のものが置いてあります。Section 4 は "Varieties of Expanded Boolean Algebras" というタイト…

□, ◇ の単調性 if p → q then □p → □q if p → q then ◇p → ◇q と、axiom B に相当する公理の組*1 p → ◇□p ◇□p → p から intuitionistic reasoning で distributivity law ◇(p∨q) → ◇p∨◇q が導けることに気がついたので証明をメモ。 p → □◇p from the axiom □…

今度は A. Palmigiano の論文。概要だけ見てみたのでメモ。昨日の Hilken の論文と同じで直観主義様相論理の duality の話。ただし、こちらの論理は Hilken の考えたものよりも強くて、様相を intuitionistic first-order logic での quantifier とみなすこ…