使う言葉： 述語 → (述語関数 | 述語記号) 命題〈単純命題〉 構造化命題〈structured proposition〉 導出〈derivation | デリベーション〉 シーケント リーズニング 背景指標 導出可能〈derivable | デライバブル〉 使わない言葉： 判断 証明 推論 推論規則 …

名前〈記号〉とモノを区別できない。a と [​[a]​] （スコットブラケット）で区別する。 命題と主張を区別できない。P と |- P で区別する。 要素と集合を区別できない。a ∈ A で区別する。 内包と外延を区別できない。A = {x∈A | P(x)} で区別する。 所属と…

話し手の態度（意図の復元可能性）： 話し手基準： 自分（話し手）なら、この言い方で分かる（復元可能）。 聞き手基準： 聞き手は、この言い方で分かる（復元可能）だろう。 主要な責任： 話し手責任： コミュニケーションを成立させる責任は話し手にある。…

「‥‥とは何か？」という疑問・質問。例えば「型とは何か？」 合意目的の質問： 何かを便宜的に約束しよう、という提案 追求目的の質問： 一意的なホントの意味を探ろう、という提案 追求目的のの質問は、追求すべき実態が存在しないとナンセンスになる。しば…

元の概念（例：多様体） そこからはみ出した概念（例：境界を考える） 2つの排他的概念（例：境界無し、境界あり） 元の概念の再確認（例： 境界無し） 統合した概念（例：境界があってもなくてもよい） 実例 1： 多様体 境界付き多様体 多様体と境界付き多…

同義語、曖昧多義語が多いのを利用して、連想ゲームをする。「代入」の用法： 上書き割り当て〈overwrite assignment〉 手続き型プログラミング言語の代入文 束縛〈binding〉 関数型プログラミング言語の let, where など 置換〈substitution〉プレースホル…

型無し演算子指標は untyped operator signature だが、untyped ＝ single sorted 。また、演算子は代数的指標の演算〈operation〉。したがって、 op:(S, ..., S) → S と書ける。通常のプログラミング言語と同様に引数変数を使うと、 op: (a:S, ..., z:S) → …

次の可換図式がある。$`\require{AMScd} \begin{CD} |{\bf FinSet}| @>{\mathrm{card}}>> {\bf N}\\ @AAA @AAA \\ |{\bf ThinSet}| @>{\mathrm{IsNonEmpty}}>> {\bf B} \end{CD}\\ \:\\ \text{commutative in }{\bf SET}`$やせた集合は空集合または単元集合…

型： String: 文字列、特にバリデーション〈検査〉しない。 MailAddr ⊆ String: バリデーションする。 ZipCode ⊆ String: バリデーションする。 旧スキーマ： ( givenName : String, familyName : String, mailAddr : MailAddr, userId: String, geoAddr : S…

集合 A の要素の順列の個数と、集合 A の分割〈パーティション〉に順番〈全順序〉を付けたモノの個数は同じ。だが、解釈が違う。以上の事実は、バンドルの移送方向（前送り〈押し出し〉か引き戻し）に関して基本的な見方を与える。同様に、組み合わせ的な議…

n-圏の離散化持ち上げ〈discretization {lift | promotion | ascent}〉をδ、打ち切り引き下げ〈truncation {fall | demotion | descent}〉をτとすると。$`\quad {\bf SET}(A, \tau {\bf Set}) \cong \tau {\bf CAT}(\delta A, {\bf Set})\text{ in }{\bf SET…

書き方と印象。文字は変えない。 $`(f_i:A_i \to B_i)_{i\in I}`$ まー、写像の族だわな、うん。 $`(f[i]:A[i] \to B[i])_{i\in I}`$ スキーマ〈集合の配列〉 A とスキーマ〈集合の配列〉 B のあいだの値変換に見える。$`i\in \{1, 2, 3\}`$ とか。 $`(f_i:A…

https://www.academia.edu/28844867/Quantum_Kan_Extensions_and_Applications（ローカルにダウンロード済み）の記法の約束Guide to NotationNew terms are underlined when defined. Bibliography citations appear in brackets such as [102]. Cross refer…

論理的な推論の能力や抽象化の能力などは常に言及されるが、言及されないか、むしろ否定的に扱われるスキルは： 記憶スキル エラボレーション・スキル 特に記憶スキルに関して： 歴史上の事実やエピソードから憶える。事例：なし。 人物名を憶えるために顔写…

線形代数 セオリー論 事例1：遷移系 事例2：階層構造 基底 指標 集合＝アルファベット 単純DAG＝ハッセ図 基底の要素 記号セル 要素＝文字 アロー、辺 線形結合 コンビネーション 文字列＝ストリング パス 自由ベクトル空間 セオリー 自由モノイド 自由やせ…

命題が提示されると、提示されただけで真、または提示されただけで偽と即断しがち。真偽不明だと保留するのは苦手。 見た目上の相関があると、必然的相関だと考えがち。偶然的相関〈疑似相関〉だと考えるのは苦手。→ http://tylervigen.com/spurious-correla…

自然言語の印象・連想に影響されないで、必ず形式的な定義を確認する。 用語・記法には、合理的な根拠も一貫したルールもないので、個別に暗記する。 細部に神経を使う。例えば、空集合や単元集合、空集合／単元集合からの写像、空集合／単元集合への写像な…

命題が出現する文脈として、定理、予想、問題などがあるがハッキリと区別するために： assertion ： 「正しい」という判断を伴った主張。 judgement ： assertion と同じ。 demand ： 「正しい」ことが不明なので、証明の要求。 enquiry ： demandと同じ。問…

カリー化： 引数なし関数： f() = f(*) = f( () ) 要素とポインティングマップ： a = a() = a(*) タプルと関数： 要素と単元集合の意図的混同 要素と単元リストの意図的混同 引数内の囲み括弧省略： f( (x, y) ) = f(x, y) ニセの和（区切り記号としてのプラ…

話が通じない原因が全単射と可逆写像を別物だと思っていたことだった。たくさんの言葉があると、すべて同義語とは判断しにくいらしい。 全単射 双射 バイジェクション 可逆{写像 | 射} 同型{写像}? 1：1対応

可換モノイドは、モノイドの☓☓☓に加えて、◯◯◯の☓☓☓を付け加えて定義される代数系である。 ☓☓☓ 公理 等式 法則 条件 性質 〇〇◯ 交換法則 可換律 可換性 演算の交換可能性

"Canonical Structures for the working Coq user" by Assia Mahboubi, Enrico Tassi （https://hal.inria.fr/hal-00816703v1/document）の最初の段落： One of the key ingredients to the concision, and intelligibility, of a mathematical text is the …

よくある混同・混乱 構文的表現と意味的実体 要素と集合 射と写像（射＝写像 と思いこんでいる） 要素と単元集合 要素と長さ1のリスト 空集合と単元集合（入力や出力が「ない」ときなど） 特定状況 多圏の基本対象（AtomObj(M)）と多対象（PolyObj(M) = List…

上が新しい。 用語ペアの具体例 - (新) 檜山正幸のキマイラ飼育記 メモ編 用語ペアの関係性 - (新) 檜山正幸のキマイラ飼育記 メモ編 否定の接頭辞、拡張的形容詞 - (新) 檜山正幸のキマイラ飼育記 メモ編 排他的否定、拡張的否定、制限的否定 - (新) 檜山正…

曖昧多義語の例：確率変数 単なる可測写像 確率空間からの可測写像 確率空間のあいだの測度保存写像 特に、同時確率分布の射影写像 確率空間、または確率空間の台集合を変域とする変数 確率測度 標本空間 可測空間 可測写像の域 可測写像の余域 確率空間の台…

固有名：他でもないそのモノだけを指す名前 種別名：いくつかの個体達に共通する性質の名前。その性質により個体が分類される。 役割名：構造物や組織体の構成素／構成員の役割の名前 実際には、これらの名前の用法が頻繁に入れ替えられる。 固有名 → 役割名…

イイカゲンの原理： 用語・記法は適切とは限らない。整合性・一貫性を期待してはならない。 モノグサの原理： 用語・記法は省略やオーバーロードにより書く労力を節約している。読み手側に負担を押し付ける。 暗黙の原理： 暗黙の前提や約束ごとが存在する。…

ラムダ図は、ラムダノードとワイヤーからなる。 ラムダノードは三角または台形で描く。 ノードに接合するワイヤーには、入力ワイヤー（0本以上）、ラムダワイヤー（0本以上）、出力ワイヤー（1本だけ）がある。ラムダノードは逆行ワイヤーとして描く。 ワイ…

「-----」は、アトミックな証明＝推論ルール 「~~~~~」は、アトミックとは限らない証明（アトミックを排除しない） 「=====」は、アトミックなリーズニング＝タクティク 「+++++」は、アトミックとは限らないリーズニング＝スクリプト (A∧B)→C ⇒ A→(B→C) の…

連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。モヤモヤを晴らすためにすること。 ラムダ項の圏論的位置付けをハッキリさせる。 単なる圏ではなくて復圏〈オペラッド〉を使う。 デカルト閉復圏＝…