次のようなシーケントスタイルの定義は、 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」シーケントはゲンツェンにより導入された概念であり、（数学の一分野としての）論理が扱う主要な対象物（のひとつ）である。論理式が論理の主役なのではない。 論理式は、論理式のリストを構成する素材に過ぎない。 論理式のリ…

※この記事は「記事9 問題集7」単一の論理式〈形式化された命題〉だけではなくて、論理式のリストを徹底的に使い倒した最初の人はおそらくゲンツェンだろう。プログラミングで言えば、単一タプル引数（パックされた多引数）、単一タプル戻り値（パックされた…

※この記事は「記事8 問題集6」2018-12-02: 冒頭に、スコット・ブラケット＝真理集合の役割の説明を追記。与えられた論理式〈形式化された命題〉に対して、そのスコット・ブラケットを実際に計算する練習。スコット・ブラケット（の値）と真理集合は同じもの…

※この記事は「記事7」（問題集ではない）演繹を遂行できる人工的なシステムである演繹システムを（少なくとも1つは）実際に構成して、その演繹システムの性質を調べるのが我々に課せられたタスクである。その演繹システムの論理パートを、仕様として定義する…

ずーーっと、用語法の整理、使える用語／使えない用語の選別をしている。酷い状況であることはもちろん承知はしていたが、作業してみると、その酷さをまざまざと実感する。命題を表す変数を「命題変数」と呼びたいが、「命題変数」は命題論理 -- コンテキス…

推論のストリング図をテキストで表したものがシーケントだと解釈すると、通常のシーケント記法はダメなことがわかる。シーケント矢印が 推論のスパイダーを表す矢印 ケーブリングを表す矢印 の区別ができないと、ストリング図を書き写すことができない。次の…

演繹システムのパート分類（モジュラー／レイヤード設計・実装のため）： 分野固有パート 論理パート（分野によらない共通パート） 分野固有パートは： 個体レベル 型レベル 論理パート 命題レベル 推論レベル システムが単ソート〈single{- | }sort{ed}?〉…

メタ(形容詞)＝我々が生きている現実世界の … 対象(形容詞)＝我々が調査と考察の対象（目的物）とする数学的モデル（対象演繹システム）内の … 例： メタ記号 vs. 対象記号 メタ変数 vs. 対象変数 メタ命題 vs. 対象命題 メタ定理 vs. 対象定理 メタ側がモヤ…

推論を次のように規定する。 推論には必ずプロファイルがある。 プロファイルは仮定命題リストと結論命題リストからなる。 推論はラベル付きのときもあれば、ラベル無しのときもある。 推論は組み込みのときもあれば、ユーザー定義のときもある。 組み込み推…

名詞 動詞能動態 形容詞-済み 形容詞-可能 証明 × × ○ 推論は- ○ 推論は-、命題は- 推論 ○ △ 仮定が結論を- × × リーズニング ○ ○ 上式が下式を- ○ 推論は- ○ 推論は- 言い方の候補： Γ infers Δ Γ concludes Δ Γ derives Δ Γ entailes Δ ξ reasons η ξ conc…

マルチスクリーンムービー ムービーフィルム フレーム（のコンテンツ） 絵コンテ〈ストーリーボード〉 {絵コンテの{コマ | シート} | {ストーリー}?シート} シーン {アクション}?コマンド スクリプト（ActionScriptは固有名詞） スクリプトのユーザー定義関…

なんかもう、ひたすら単語の選択と（必要なら）造語をしている。いいかげんウンザリはしている。全般的に、用語法において、関数と関数を表す式と関数値の区別が付いてない／付けてないことが分かる。これは普遍的（どこでも見いだせる）な現象だ。関数まわ…