様相論理 is Fun

様相論理の学習ノートです

MENU

ああ何て素敵な日だ

HuaweiのMediaPad M5liteを買った。

 

ELECOMキーボードとBluetooth接続して使う。

 

感度がいいので、PCの代わりに使える。

 

古いPCは不用になる。

 

多分これで漫画をいっぱい読むことになると思う。

 

このガジェットのおかげで生活が変わりそう。

 

S4.4のLTAが構成できたので、明日からはまたframework。

 

frameの構成に関しては、まだ、完全に、手探りだけれども、S4.2とS4.4に対応するframeが作れたら、少しは何かが見えてきそう。

 

もし、見えたら、生活が変わりそう。

 

変わるといいな。

経過

S4.2のLTAを構成.

 

対応するframeは明日以降に探す.

 

S5に対応するframeは2元だった. Tに対応するものが2元だから当然なのだろう.

 

S4.4のLTAの構成は明日考える.

 

結局、S4からS5の間の系列といっても、命題変数が1個、かつ、2次で考えているので、間にS4.2とS4.4しかない.

 

今日は、数学的にも非数学的にも楽しい一日だった.

 

ただただ感謝.

 

今日はぐっすり眠れそう.

 

眠れるといいな.

 

四の五の言う

S4の計算を終えて、少し肩の力が抜けた。

 

次は,S5に対応するframe探し。

 

2次のS5は、1次のTのLTAのultrafilter relationから定まるBAOに同型だろう. いずれにせよ、小さいので、すぐに見つかるはず.

 

それから、当面の計画は、H&Cのカタログ見ながら、S4からS5の間の系列を全部計算すること. ぞくぞくする. 検証に耐えるか、あるいは、水の泡に終わるかどうか.

 

過度の期待はしない. ただ、善良に数学をする.

 

一葉集をふと開いたら、「七つといふとしより・・・」のくだり。

 

「死ぬ斗(ばかり)悲しかりしかど学校は止になりけり 十五まで家事の手伝ひ裁縫の稽古とかく年月を送りぬ されども猶夜ごとゝ文机にむかふ事をすてず」とあった。

 

その後、上等の運が馬車に乗って迎ひに来たのか、運命は、この才人に傑作を授けた。そして、奇跡を世に残し、天の上の人となった。

 

Bumpのaurora arcを聞いていても思うことだが、日本語が母語で本当によかった。

 

傑作を味わえる幸運に感謝。この喜びを励みにしよう。

 

あはれくれ竹の一ふしぬけ出でしがな。

一段落

やっと欲しいframeが構成できた。

 

このframeに対応するBAOは、S4(ただし, 命題変数1個, かつ2次以下)のLTAに同型になる.

umemura-wataru.hatenablog.com

$W=\{w_1, w_2, \ldots, w_6\}$で, 到達可能関係は, $R=\{(w_1,w_1), (w_2, w_2), \ldots, (w_6, w_6), (w_1, w_2), (w_2, w_1), (w_5, w_6), (w_6, w_5), (w_3, w_1), (w_3, w_2),\ldots, (w_3, w_6), (w_4, w_1), (w_4, w_2), \ldots, (w_4, w_6)\}$.

 

$6$個が最小かどうかはわからない.

 

$2^6$通りのmodelを, 対称なものを飛ばして, しらみつぶしに計算した.

 

計算方法を改良したおかげで, このframeに見当をつけてから, 検証にあまり時間はかからなかった.

 

引き続き, 計算はしまくると思うが, いずれ計算機の手を借りざるを得なくなるので, 今のうちから何が使えるか調べておくことにする.

 

次に考えることは, 部分代数と各世界の対応. 同じ部分代数に異なる世界が対応することがあるので, 部分群と部分体の対応のように簡明ではない.

低スぺを生きる

禁煙して約10日。

 

禁酒して2日。

 

禁煙はニコチンガムがあれば、ひとまずは余裕。

 

本命は禁酒。

 

ノンアル+眠剤に頼る。

 

不健全だけど、悪習を続けるよりはまし。

 

枯死した集中力(数学力といいたいところだけど、そんなものがはなからあれば苦労はない)を蘇生するために、できる限りのことをやる。

 

少なくとも、phisical conditionは、コントロールする。

 

そろそろ、不真面目を改めて、真面目にやらないと、何も解決しないし、ぞろりもしない。

 

正当なトレーニングを積む。

 

数学的不毛生活はもういい。

 

"the real beauty of the subject"で酔いたい。

 

どうやら、欲しかったframeを構成ができたようなので、今日はこの辺で寝ることにしよう。

願望

S4のLTAと同型なBAOが対応するframe作りは未完成.可能世界は最低4個必要だが、4個では不十分な気がする.

 

明日5個の場合を計算する.

 

収穫はまだないけれども、2つのframeからそれぞれ作ったBAOの間に包含関係があるとき、必ずしもgenerated subframeになるような埋め込みは存在しないけれども、含まれる方の任意のモデルに対して、含む方のあるモデルで、bisimilarになるようなものが存在するかどうか、とか、新たな問題意識が湧いてきたりして、何かに結びつく可能性は耕せているといいな.

semanticsというかcombinatorics

2次のS4のLTAに対応するframe作りに苦戦中。

 

非連結なframeなら簡単だろうが、連結なものを探している。

 

4個以上の世界からなる、反射的かつ推移的なframeを片っ端から試そうとしている。

 

不安なことには、完全に手探りであること。

 

とはいえ、先のことは、いったん置いておいて、まずは探り当てよう。できれば今夜中に。

framework

$\mathcal{F}=(W, R)$をフレームとする.

 

命題論理のLTAを$L^0$と表し, 命題論理式$\phi$に対して, $\phi$が属する$L^0$における同値類を$[\phi]$と表す.

 

$\mathcal{F}$のvaluation $V$は, 各世界$w\in W$に対して, $L^0$のultra filterを定める:

 

$\{[\phi]\mid(\mathcal{F}, V), w\models\phi\}$

 

このultrafilterを, $U_w^V$と表す.

 

$V$がすべてのvaluationにわたるとき, $(U_{w, v}, \bigcup_{wRv}U_v^V)$全体をatomとするBoole代数$L^1$(すなわち, $L^1$は\{(U_{w, v}, \bigcup_{wRv}U_v^V)\}_{w, V}$のべき集合)は, $L^0$の拡大である1次のBAOである:

 

$[\phi]\in L^0$は$\{(U_{w, v}, \bigcup_{wRv}U_v^V)\mid[\phi]\in U_{w, v}\}$に対応する.

 

また$M[\phi]$($M$possibilityを表す様相演算子)は, $\{(U_{w, v}, \bigcup_{wRv}U_v^V)\mid[\phi]\in\bigcup_{wRv}U_v^V)\}$に対応する.

 

大体同様の手続きによって, 2回到達関係, 3回到達関係, $\ldots$から, $L^0$の2次拡大, 3次拡大, $\ldots$が構成される.

 

このとき, $k$次の様相論理式$\phi$に対して, $\phi$が$\mathcal{F}$においてvalid iff $\phi$に対応する$L^k$の元が$=1$が成り立つ.

 

$k$次拡大については, 曖昧なので, いずれまとめ直す.

 

また, 具体的な計算例も, いずれ記す.

リバースエンジニアリング

まだまとめていないけれども、frameから命題論理のLTAの拡大になっているBAOの構成($\phi$がvalidならその像が$=1$, satisfiableならばその像が$\neq0$になるようなやつ)の逆(ultrafilter frameよりも小さなやつ)がしたくて、模索中.

 

とりあえず、1次の場合に試行錯誤的にうまくいって、計算結果を放置したままにしていたので、それを一般性のある方法でやり直して、2次の場合の計算例を積み重ねる予定. 2次の場合は場合と計算量が格段に増えるので、時間がかかる.

 

ちょっと手ごたえがあるけれども、見当はずれなことをやっているかもしれない. いずれにしても夏の間に白黒がはっきりするといいな.

次の目標

frameからBAO(命題論理のLTAの拡大になる)の構成について、今度時間があるときにまとめる。

 

おそらく、frameから作られるクラスは、命題論理のLTAのultrafilterの置換(ここでは、全単射ではなく、ただの自身への写像の意)に関して不変であるように思われる。

 

ちなみに、KWのLTAは、不変ではない。←これは計算ミス。よくよく考えると、LTAも不変。

 

このあたりの事情、特に、上記の不変性が正しいかどうかは、まだまだ根拠足りないので、探ってみる。

 

LTAの場合は、ある種のfilterによる商として特徴づけられるが、frameから作られるクラスの特徴づけは、よくわからない。探る。

定式化 その2

前回の続き.

umemura-wataru.hatenablog.com

 以下において, 命題変数は有限個とする.

 

 $U_{ij}^\prime$をatomとするBAを$L^1$とすると, これは(1次以下の様相論理式全体から作られた)$K$のLTAと同型である. 

 

$L^1$のultrafilterとultrafilterの和集合のペア全体をatomとするBAを$L^2$とし, 同様の手続きで, $L^3$, $L^4$, $\ldots$を定義する. $L^k$は$k$次以下の様相論理式全体から作られたKのLTAと同型である.

 

また 自然に, $L^{k-1}$は$L^k$に埋め込まれるので, $L_0\subset L^1\subset L^2\subset\cdots$と考えられる. よって, $L^\infty=\bigcup_{k=1}^\infty L^k$という定義が意味をもつ.

 

$L^\infty$はKのLTAと同型である.

 

次回は, 正規様相論理$\varLambda$から作られる部分代数($\varLambda$のLTAと同型になるはず)と, frameから作る部分代数について書く.

 

2つの代数は異なるクラスであるように思われるが, 結論はまだ出ていない.

 

経過

H&Cのカタログを見ながら、各正規様相論理(ただし、命題変数は有限個かつ次数制限あり)のLTAを,命題論理のLTAを拡大して構成している.

 

T, D,T_c, D_c,Triv, Verの場合は構成済み..

 

S4は検証が必要.

 

2次以上の場合は、元の個数が指数関数的に増大するので, 大変.

定式化 その1

$\varPhi^0$を命題論理式全体の集合とし, $\varPhi^1$を1次以下の様相論理式全体, $\varPhi^2$を2次以下の様相論理式全体, $\ldots$とし, $\varPhi^\infty$を様相論理式全体とする.

 

$\varPhi^0$を"$\phi\rightarrow\psi$と$\psi\rightarrow\phi$が証明可能"という同値関係で割って得られるLindenbaum代数を$L^0$とする. $\phi\in\varPhi^0$に対して, $L^0$における$\phi$が属する同値類を, $[\phi]$と表す.

 

 $\{U_i\}$を$L^0$のultrafilter全体とし, 各$i$に対して, $\{V_{ij}\}$達は, 空集合およびultrafilter達の和集合全体に渡るとする.

 

このとき, ペア$U^\prime_{ij}:=(U_i, V_{ij})$に対して, $\phi\in\varPhi^1$の$U^\prime_{ij}$による解釈を次で定める.

 

$\phi\in\varPhi^0$に対しては, $U_{ij}^\prime\models\phi$ iff $[\phi]\in U_i$であり, $U_{ij}^\prime\models M\phi$ iff $\phi\in V_{ij}$と定める.

 

 すると, 論理式の構成により, すべての$\phi\in\varPhi^1$に対して, 解釈が定められる.

 

このとき, この解釈は, $\phi\rightarrow\psi$, $\psi\rightarrow\phi$が$K$で証明可能ならば, $U_{ij}^\prime\models\phi$ iff $U_{ij}^\prime\models\psi$が成り立つ.

足らぬ足らぬは・・・

証明はうまくいきそう。

 

定式化と併せて明日の休みに書く。

 

それから、LTAと同型になるための条件は、自己同型か自己準同型に関する不変性になりそう、というかなってくれたらいいな(願望)。

 

complex algebraとは同型でないことは、元の個数から容易に確かめられた。けれどもこのalgebraが有用かどうかは現段階では何とも言えない。

 

検証が足りない。全然足りない。

 

それから、あらためて読み返して、H&Cの本は聖書だと思う。

 

勉強が足りない。全然足りない。