Mizarは（潜在的には）イプシロン記号で関数を定義している。同じ方法で定義するとして、 関数 部分関数 スコーレム関数 定義形式は仮にだが、 function foo:X->Y := λx∈X.εy∈Y.P(x, y) partial function foo:X->Y := λx∈X.εy∈Y.P(x, y) Skolem function foo…

次の命題を考える。 ターゲット命題： fが各点で連続ならば連続 通常は無意識に使っている選択公理の使い所が分かるように書いたので、証明が長くなった。記号の乱用記号の乱用をして、位相空間とその台集合を同じ記号で表す、つまり、X = (X, OX) のように…

途中までだ。A⊆N が、次の3つの性質を持つとする。 Aは空ではない ---(1) n∈A ⇒ -n∈A ---(2) n, m∈A ⇒ n+m∈A ---(3) このとき、非負整数kがあって、 n∈A ⇔ nはkの倍数 ---(4) 上のパラグラフをまとめると、 $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4) しかし、条…

とりあえず、分かりやすいのだけ列挙する。⇒導入 Aと仮定する。 ： Bである。 以上により、したがって、 A⇒B である。∧導入 Aである。 ： Bである。 $(A)だったので、したがって、 A∧Bである。∨除去 A∨Bである。 場合分けをしよう。 Aの場合： : Cである。 B…

集合と論理の練習問題： ツリー状の集合族 - 檜山正幸のキマイラ飼育記

目標設定文〈ターゲティング文〉：証明すべきターゲット命題を明らかにする。ターゲティングの時点では、ターゲット命題はもちろん証明されてない。 結論付け文〈コンクルーディング文〉：ローカルであれグローバルであれ、ターゲットが証明されて、定理にな…

ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) - 檜山正幸のキマイラ飼育記の証明部分（枠内）は、半形式的になるように意識したのだが、そのとき感じた雑多なこと。 任意のxを選ぶ。 xを任意とする。 任意のxに対して 以上は同義で、自由変数xを含…

次の区別は曖昧。 …により …から …を使って 「により」と「から」は同義だと思っていいが、「使って」は例えば証明シェマ（マクロ）を使うことに限定するとかの用法もある。ただし、「定理命題を使う」と「証明シェマを使う」の境界も実はあいまい。 A∈Γ | B…

自分が使っている言葉をとりあえず列挙する。メタな言明 …（命題）が言える。 行為の予告 …を計算する。 …を示す。 …を示そう。 行為と結果 …（行為する）と、 文と文のあいだの接続詞 …（命題）(に)?より、 …（命題）から、 …（命題）なので、 …（命題）(だ…

n-圏Cがあるとして、この対象が何であるによって扱いが変わると思う。 |C|∈0-Cat であるとき、Cの深さは0。このとき、対象類＝0-モーシングは集合。 |C|∈1-Cat であるとき、Cの深さは1。このとき、対象類＝0-モーシングは圏。圏を対象とするn-圏。 |C|∈2-Cat…

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

コンピュータッドの圏を単に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〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張…

https://ncatlab.org/nlab/show/transfor に、n-圏のあいだのk-変換手（k-transfors between n-categories）に関する表があるが、なんかレンダリングが崩れている。日本語にして書いておく。 k↓ -2 -1 0 1 2 3 ... 0 自明 含意 関数 関手 2-関手 3-関手 ... …

あれ、これって指標のラムダ計算に役立つぞ。 「確率変数」の一般論は可能か - 檜山正幸のキマイラ飼育記

CafeOBJで、タイト意味論とルーズ意味論という言葉を使っていたが、いまいちハッキリしないので、次の3種に分ける。 ホール〈whole | 全体〉意味論 始対象意味論 終対象意味論 Σが指標のとき、〚Σ〛をどうするか、という話。これをハッキリさせないで指標の…

指標の圏が有限余完備であることが本質的。ただし、非モノイド的なので、モノイド積は定義できない。非モノイド的有限余完備圏。それと、ゴグエンのいうinclusiveで、やせた部分圏としてinclusionが定義されている。双対的にはprojectionだが、inclusioinと…

nに対して、n-指標はn-セル＝n-項までを持つコンピュータッドとして定義される。n-指標はn-コンピュータッドだから、n-圏を生成する。このn-圏に、(n+1)-射の族を追加する役割が(n+1)-表明。n-指標と(n+1)-表明の組み合わせがn-仕様（(n+1)-仕様ではない）。…

ユグドラシル・エクスプローラー - 檜山正幸のキマイラ飼育記 メモ編の続き。ワールドのなかにある項目を、ミクロ項目とマクロ項目に分けたほうがいい。 マクロ項目： 項目なので区分〈division〉、プロファイル、名前を持つが、名前だけでなくて、名前に関…

https://ncatlab.org/nlab/show/transfor トランスフォー〈変換手〉はワールドの項目として必要となる。nとkで、k≦n に対して (n, k)-トランスフォーが定義できる。 (0, 0)-トランスフォーは写像〈map〉 (1, 0)-トランスフォーは関手〈functor〉 (1, 1)-トラ…

ユグドラシル “ユグドラシル”は、Coqのuniverseの話を読んだ時連想した。 エクスプローラー ブラウザと言ってもいいんだけど、“エクスプローラー”のほうが探索・探検・究明の意味があるから。 我々が何かするときの文脈を世界〈world〉と呼んでしまおう。世…

だいたいの感じは掴めた。 概念 表現方法 ソフトウェア 圏 コンピュータッド データ（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と同型である、という事だと…