次のようなシーケントスタイルの定義は、 For C in Cat, D in 0Cat For FO : C.Obj → D.Obj in Set For FM(A, B in C.Obj) : C(A, B) → D(FO(A), FO(B)) in Set Define F : C → D in Cat // F is-a-functor :⇔ F = (FO, FM) SuchTaht ... End仕様としてまと…

リテラチャーは、セオリーのk-レイヤーの構成素 - 檜山正幸のキマイラ飼育記 メモ編で初めて出てくる概念。基本的な関係は、 Lk = k-Lit(Σk+1) Σk in Lk ここで、 Lkは、k次元レイヤーにいるリテラチャー Σk+1は、(k + 1)次元レイヤーにいる特定された指標 k…

随伴に関する注意事項 - 檜山正幸のキマイラ飼育記で書いた、「構造か命題か」の問題があるので、構造としての随伴対は、adj(L -| R) と書いて、L -| R は命題として使うことにする。ほんとは絵で描くのが良いのだが、なんとかアスキーで定義を書いてみる。…

dRAdjL, dLAdjR を随伴系の二重圏だとする。その構成素〈constituents〉は、 0-射は圏（または厳密2-圏の対象） 垂直1-射は随伴系を左関手方向で考えたもの。 水平1-射は関手（または厳密2-圏の射） 2-射は、右または左の四脚2-射 右四脚2-射、左四脚2-射と…

モナドの圏を σMndγ(K) の形で書く。σは圏のソート、γは圏の修飾子とする。まず、修飾子は形容詞を組み合わせて作る。 形容詞記号 意味 L 左 R 右 Alg 1-射が代数的 EM アイレンベルク／ムーア、1射が右斜め加群 Kl クライスリ、1射が左斜め加群 S 単純、2-…

コック／ツーバライン https://ja.forvo.com/search/Z%C3%B6berlein/

ガースキイ https://www.youtube.com/watch?v=h3M5AMkZ1u4

「関手オートマトン」で検索： http://d.hatena.ne.jp/m-hiyama/searchdiary?word=%B4%D8%BC%EA%A5%AA%A1%BC%A5%C8%A5%DE%A5%C8%A5%F3 「関手データ」で検索： http://d.hatena.ne.jp/m-hiyama/searchdiary?word=%B4%D8%BC%EA%A5%C7%A1%BC%A5%BF

※この記事は「記事19 解答10」問題集10とは、次の記事（の問題部分）のことです： スパイダーパズル (A17P10) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。内容： スパイダーパズルと演繹システム 書き方の注意 …

当初（2018-12-18）、「スパイダーパズル (A17P10)」において、「次の定理を証明せよ」という問題を出しました。 構成不可能性定理： プロファイルの形が Γ → Δ で、リストΓ内に出現するBの個数が、リストΔ内に出現するBの個数より少ないとき、このプロファ…

※この記事は「記事17 問題集10」この記事の問題をやれば、形式化された証明や演繹システムに対して、（詳細はともかくとして）かなりの程度のイメージが持てると思います。問題の解答例は、早めに（たぶん次回）出す予定です。[追記]解答はこちら → 問題集10…

※この記事は「記事16」次の問題はやってみましたか？ ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答（の一例）は次の記事にあります。 問題集1の目的と解答と追加説明 重要！ (A13R1) 引き続く次の記事も類似の問題です。 整数式の操作 (A3P2) 整数式…

※この記事は「記事15 解答8-1」問題集8とは、次の記事（の問題部分）のことです： シーケントとスコット・ブラケット (A10P8) 「シーケントとスコット・ブラケット (A10P8) // 組み込み推論を表すシーケント」の解答例＋解説。 シーケント (x, y∈R), x2 = -3…

※この記事は「記事14 解答6-2」問題集6とは、次の記事（の問題部分）のことです： 命題と、そのコンテキスト／真理集合 (A8P6) 「その1」は、次の記事です。 問題集6の目的と解答と追加説明 (A14R6-1) 内容： 書き方の注意 限量子を含む閉論理 コンテキスト…

※この記事は「記事14 解答6-1」問題集6とは、次の記事（の問題部分）のことです： 命題と、そのコンテキスト／真理集合 (A8P6) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。誤解されがちなメタ論理やメタ論理記号…

※この記事は「記事13 解答1」「だ・である調」から「です・ます調」に変更します。問題集1とは、次の記事（の問題部分）のことです： ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項…

※この記事は「記事12」シーケントは論理の中核的な概念であり、演繹システムを構成するにしろ、意味論を考察するにしろ、シーケントを基本的対象物とみなすことなる（そうするのが、現状では最良の選択肢だと思われる）。「シーケントとは何であるか？」とい…

※この記事は「記事11 問題集9」記号的表現に対して「自然言語（日本語や英語）による読み下しが出来ないと馴染めない」という事情も当然だから、シーケントの読み下し練習をする。そして、「“シーケントの正しさ”を正しく判断する／判断できる」とはどういう…

※この記事は「記事10 問題集8」シーケントはゲンツェンにより導入された概念であり、（数学の一分野としての）論理が扱う主要な対象物（のひとつ）である。論理式が論理の主役なのではない。 論理式は、論理式のリストを構成する素材に過ぎない。 論理式のリ…