宗教や政治とは離れて、論理として信念体系〈belief system〉を考える。述語論理の体系Lを固定して、命題とはLの論理式のことだとする。命題と述語は区別せずに、命題＝述語の全体はPredとする。ただし、議論域があるので、X上の命題はPred[X]とする。Pred[-…

ボックスの絵は、"Natural deduction for predicate logic"（https://cs.uwaterloo.ca/~plragde/cs245old/06-prednd.pdf）から抜粋。最後の絵は他の文献からコピーしたが、その文献が分からんから出所不明になってしまった。しかし、同じ絵だから"Natural de…

Cは一般的なモノイド圏、X = (X, δ, ε)がC内の余モノイド（余モノイド構造、余モノイド対象）のとき、Xのスタンピング関手（域側に掛け算する）から余モナドが定義できる。 上記の余モナドの余クライスリ圏を作れる。これは一般的な構成。 余モナドがテンソ…

論理記号 導入規則 除去規則 ∧ ∧導入 BOX ∧除去1, ∧除去2 BAR ⊃ ⊃導入 BOX ⊃除去（モダスポネンス）BAR ∨ ∨導入1, ∨導入2 BAR ∨除去 BOX ¬ ¬導入（背理法）BOX ¬除去（矛盾）BAR BOXまたはBARのラベル 論理記号 導入規則 除去規則 ∧ pair BOX proj1, proj2 B…

図そのものより、図示の基礎を書く。デカルト閉圏Cを固定して、I := IdC、直積を∧、単位を1、始対象を0とする。Δ:C→C×C はコピー、Πi:C×C→C は射影、K:C→I は一点への潰し、S:C×C→C×Cはスワップ。 自然変換 自然変換の記号 プロファイル 名前 略称 ι I⇒I 恒…

L, L', Mなどはローヴェア・セオリーとする。 ローヴェア・セオリーの直和 L + M ローヴェア・セオリーのテンソル積 LM テンソル積はどの程度存在するかよくわからんが、次が成立する。 Mod(L, Mod(M, C) Mod(LM, C) この同型は（それが存在するなら）超便利…

ステイ／メレディス(↓)から辿って、主にローヴェル・セオリー関係の文献。 Logic as a distributive law Mike Stay, Lucius Gregory Meredith 17p https://arxiv.org/abs/1610.02247 ステイ／メレディス(↑)が参照しているもの。まずはハイランド／パワー： T…

ステイ／メリディスの次の論文、とても良い。 Title: Logic as a distributive law Author: Mike Stay, Lucius Gregory Meredith URL: https://arxiv.org/abs/1610.02247 僕がふだん考えていることだから、問題意識が一致して分かりやすい。本論じゃないとこ…

困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 で述べたこと： 自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出…

トランスフォーマーを考えると、定義体の内部で使う名前の供給源として、 名前は環境から供給される（名前は環境内のモノを参照する） 名前は引数から供給される（名前は引数内のモノを参照する） 名前はパラメータから供給される（名前はパラメータ内のモノ…

Standard MLではモロに関手（functor）と呼んでいるのだが、やり過ぎだと思うので： トランスフォーマー： 現状、これを使っている。問題は、自然変換のトランスフォーメーションと似ていること。 リダクト： インスティチューションではリダクト関手（reduc…

第一級オブジェクトとしてのトランスフォーマーを考えると： トランスフォーマーに名前を付けられる。名前無しでも扱える。 概念的には、トランスフォーマーが等しいかどうかを判定できる。現実的には無理なこともある（つうか、たいていは無理だけど）。 ト…

相対指標とパラメータ化指標は同じ概念である。が、相対指標は原理的で、パラメータ化指標は実用的。Σが指標のとき、指標に出現するすべての名前の集合を全名前集合〈whole name set〉と呼ぶ。全名前集合の部分集合を単にΣの名前集合〈name set〉と呼ぶ。指…

指標とコンピュータッドはまったく同義語だとする。指標の理論とはコンピュータッドの理論。 （具体）指標＝コンピュータッド＝ポリグラフ＝（高次）箙 コンピュータッドは、背景としている形状により定義が変わるが、ここでは常に球体形状〈globular shape…

システム全体もひとつの指標を持つから、それをシステム指標と呼び、Ωで表す。システム指標に含まれる名前はso-called大域名で、いつでもどこからでも自由に参照できる。システム指標Ωの環境（文脈）下にあるトランスフォーマーtを次のように書く。 Ω| t:Σ→Γ…

n-Comをn-コンピュータッドの圏だとする。Fn -| Vn : n-Com ←→ n-Cat をn次元のコムキャット随伴性だとする。この随伴性から導かれるn-Com上のモナドの台関手を Sn とする。コンピュータッドΣに対してSn(Σ)をS*と書く。上付きの星印をクリーネ／ストリート・…

Σが指標、ΔをΣの部分指標とする。Σに対して、Δ部分だけをインスタンス化したものをΣの部分インスタンスと呼ぶ。これはまーいい。ΔとΣの組 (Δ, Σ) を相対指標と呼ぶ、ただし、Δ⊆Σ。次のように考える。 部分インスタンスは、相対指標のインスタンス 完全インス…

コンピュータッドの圏を単にCom（コム）と書くことにする。n-圏のn-構造を忘れて、(n-1)-構造をそのままにして忘却関手 V:n-Cat→n-Com が定義できる。この忘却関手を使うと、 n-Cat⊆n-Com とみなせる。これは、モデル論も含めてすべてコムのなかで出来ること…

ComCat随伴性。Comはコンピュータッド、Catは圏で、 n-Compd(Σ, V(D)) n-Cat(F(Σ), D) という自由・忘却スタイルの随伴性。これがメチャクチャ重要だと思う。コムキャット随伴性から誘導されるモナドをコムキャットモナドとする。このモナドももちろんメチャ…

具体的な指標＝コンピュータッドの圏は面白い。単純そうだが実際は色々と複雑で、ジャングルを探検する気分。指標の射は基本射〈basic morphism〉と拡張射〈extended morphism〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張…

弱2-圏 モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） 弱2-圏内のモナドに関する補足：モナドが作る2-圏の多様性 米田 困った時の米田頼み、ご利益ツールズ 「確率変数」の一般論は可能か 2次元の圏における米田の補題がわからない ラックス…

だいたいの感じは掴めた。 概念 表現方法 ソフトウェア 圏 コンピュータッド データ（JSO形式？） ドクトリン 等式的仕様 拡張機能 圏はドクトリンに所属するが、プレーンドクトリン＝単なる圏は最初から入っている。システムコアには、銀河に相当する唯一の…

自然演繹系のUIをglobular風にする。 globular 自然演繹系 パレット パレット セル 項（ターム） ラベル ラベル（名前） 色 (なし) 次元 次元 ダイアグラム 式 キャンバス ノート キャンバスビュー ノートエリア コマンド コマンド コマンド Globularのコマ…

今までのレイヤー0 → レイヤー1 今までのレイヤー1 → レイヤー2 レイヤー1の論理とレイヤー2の論理に変更する。 レイヤー1 レイヤー2 論理代数 構造付き集合 構造付き圏 議論域 単なる集合 単なる圏 論理代数のレパートリ 具象圏 具象2圏 n 議論域の圏 集合…

変数宣言 vars {x:real, y:real} 代入系 subst :vars {x:real, y:real}->>vars{s, t:real} {s := x + y, t := x - y} インターフェイス interface { ... } アダプター adapter : List ->> Stack { ... } 用語： 構文形式として、まとめて記述するためのレコ…

構文 レコード ::= '{' 文並び '}' 文並び ::= 空 | 文並び ';' 文 文 ::= 空文 | 宣言文 | 定義文 宣言文 ::= 種 名前 プロファイル 定義文 ::= 種 名前 ':=' 項種付きレコードは、 種付きレコード ::= 種 レコード種〈区分 | division〉を列挙： type func…

value x:X を function x:->X の略記とするなら、type X:Set を functor X:->Set の略記と考えることが出来るな。 Cat in Doctrines functor F:C->D in Cat functor X:->C 略記⇒ type X:C トランスフォーを使うと： 1Cat in 2Cat(Doctrines) 1transfor F:C->…

ゴグエンが、指標の圏にはインクルージョン構造が必要だといっていた。ΔからΣへのインクルージョンはあってもひとつだから、Δ⊆Σ という記法が意味を持つ。Δ⊆Σのとき、引き算Σ＼Δが意味を持ち（持たせて）、Σ Σ＼Δ # Δ が成立するようにする。そうすれば、変…

最初に与えられるハイパードクトリンとエルブランモデルで作られるインスティチューションをレイヤー0（L0）と言うことにする。L0の上にレイヤー1インスティチューションを構成するのが問題なのだが、結局、レイヤー1はレイヤー0と同型である、という事だと…

データ型と型シノニム - 檜山正幸のキマイラ飼育記 メモ編 で、コンプリヘンションとコンビネーションと言ったが、 コンプリヘンション（了解） コンストラクション（構成） にする。定義を、 了解〈コンプリヘンション〉による定義 構成〈コンストラクショ…