述語という概念により、Propositions-as-Functions なのだが、$`\mathrm{Pred}(X)`$ を型ファミリー $`\mathrm{PRED}(X)`$ に持ち上げる。すると： 真偽値は、型になる。 述語は、型ファミリーになる。 真偽値／述語を型／型ファミリーに持ち上げることによ…

第一段階： 型＝集合、インスタンス＝要素、関数も（関数空間型の）インスタンス 第二段階： 型＝集合、型ファミリー＝関数、型ファミリーはインスタンスとは別 第三段階： 型は特殊な型ファミリー、インスタンス＝セクション 第四段階： 型＝型ファミリー …

実線は望ましい対応。点線は連想や混同。$`\xymatrix{ \text{型構成子} &\text{論理演算} \ar[l] \\ \text{型} & \text{命題}\ar[l] \ar@{.>}[d] \ar@{.>}@/^/[dd] \\ \text{関数} \ar@{.>}[d] \ar@{.>}@/_/[dd] \ar@{.>}@/_1.5pc/[ddd] & \text{定理}\ar[l]…

関係＝非決定性写、像部分写像、写像は二部グラフで表される。二部グラフは、片側有向二部グラフ。辺は対応ペア〈correspondence pair〉、付値ペア〈{value assignment | valuation} pair〉。 対応ペアを表わす矢印〈ストランド〉は $`\mapsto`$ だが、単な…

無交差である ＝ 分離している ＝ 排他的である 交差している ＝ 共通部分がある 包含している 同一である それぞれ $`A\cap B = \emptyset`$ $`A\cap B \ne \emptyset`$ $`(A\subseteq B) \lor (B\subseteq A)`$ $`A = B`$ 相互関係のあいだの相互関係は： …

一般名〈普通名詞〉で表される概念の外延をベン図に描かせるトレーニングをするべきだった。「それくらいやるだろう」と思っていたフシがあるが、実際は、ほとんどやらないみたいだ。パンダネーミングが理解できないのはそのせいかも。とりあえず、ベン図（…

最外表明と対象化引用符 - (新) 檜山正幸のキマイラ飼育記 メモ編 で述べた最外表明、重要だ。命題を P として、肯定的最外表明 Holds P とする。命題を述語で対象化〈objectify | 具体化 | 客体化 | 物体化〉して、肯定的最外表明を等式で表わすと：True_X …

「集合の要素とモノイドの要素は違う、あるいは、モノイドは要素を持てないのではないか？」の背景として： 「彼の会社のビル」を「彼のビル」とは言わない。 「会社のビルの窓」を「会社の窓」と言ってもよい。 「ベクトル空間のスカラー体の要素」を「ベク…

lie述語の "lie" の意味とか由来を自然言語ベースでこだわっていた人がいた。言霊信仰。 「集合の要素とモノイドの要素は違う、あるいは、モノイドは要素を持てないのではないか？」 -- これはある意味正しいというか鋭い指摘。ほんとは、モノイドの台集合の…

次が基本になる。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}}`$$`\quad D^n_k := \{x\in \mbf{N}^n \mid ||x|| \le k\}`$ $`\quad S^n_k := \{x\in \mbf{N}^{n + 1} \mid ||x|| = k \}`$ 次が成立している。 $`D^0_r = \{0\} \s…

可測空間上の述語は、真理集合が可測集合になるとする。まず、測度がないときに、以下はすべて同じこと。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\Iff}{ \Leftrightarrow } \newcommand{\OQ}[1]{``(#1)"} `$ $`…

最外表明〈outer-most assertion〉とは、それ以上はファクトチェックをしないで信じることにする命題と極性〈{logical}? porality〉のペア。次の2つの形式で書く。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\Iff}…

「多義語」タグで、同義語、類義語も扱う。 音・綴・義 「綴」は「テツ」と読む。もちろん、文字にしたときの綴り〈つづり〉のこと。 同音異綴語 異義語：台集合、大集合〈large set〉 異義語：全順序集合、前順序集合 同義語： ベキ集合、べき集合、冪集合…

"Chap"〈「チャプ」〉 は計算システムとその言語の固有名。Chap言語は完全ホモアイコニックな言語で、Chap のデータは順序ツリー。関数呼び出し形式 $`f(x, y)`$ のネイティブ形式は$` \text{"App"}[\\ \quad \text{"f"},\\ \quad \text{""}[\text{"x"}, \te…

$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\H}{\text{-} } \newcommand{\Iff}{ \Leftrightarrow } `$昔の記述をコピー$`L\H\mrm{Formula}_{(\$1\in D)}`$ に属する論理式 $`\mrm{lie}`$を次のように定義する。$`\…

実験用（半分実用）のボード： URL: https://miro.com/app/board/uXjVLKSgrFg=/ URL+α: https://miro.com/app/board/uXjVLKSgrFg=/?share_link_id=857673275163 単なるURLだけでもアクセスできる。 Miroにログインしてない別ブラウザでアクセスると、Google…

URL https://miro.com/app/settings/teamy/〈長い番号〉/user-profile が Profile Settings 。プロファイルの Language を日本語にする。長い番号はチームを識別するIDらしい。ミロの管理はチーム単位っぽい。https://miro.com/app/settings/companyy/〈長い…

$`x = f(x)`$ $`x \ne f(x)`$ これの解釈： $`\forall x\in X.\, x = f(x)`$ $`\exists x\in X.\, x = f(x)`$ $`\forall x\in X.\, x \ne f(x)`$ $`\exists x\in X.\, x \ne f(x)`$ 関数レベルでの等式： $`\mathrm{id}_X = f`$ $`\mathrm{id}_X \ne f`$

気力がなくなる理由： 何のためにやるのか分からない。動機不足、不毛感、虚無感。 何をやったらいいか分からない。困惑感、不安感、無力感。 難しすぎる。どうせ無理。徒労感、劣等感。 目標と前提： ターゲット 前提（過程、仮説）、あるいは資源〈リソー…

トピックワードとは、記述本体内に散在して出現するワードで、トピックを表すキーワード。以下、実際に予定しているトピックワード。 基本データ型 基本データ値 複合データ型 複合データ値 自然数による非負有理数の構成 自由な帰納的構成 自由な相互再帰的…

カントール 1845 -- 1918 ヒルベルト 1862 -- 1943 ラッセル 1872 -- 1970 ハスケル・カリー 1900 -- 1982 ノイマン 1903 -- 1957 チャーチ 1903 -- 1995 ゲーデル 1906 -- 1978 ゲンツェン 1909 -- 1945 チューリング 1912 -- 1954

Lisp由来であることを強調する必要はない。MiniLisp - (新) 檜山正幸のキマイラ飼育記 メモ編 で書いた以外の構成素： var宣言、または初期化構文 let式 if文、case文、while文 ブロックスコープ構造 論理言語のインタープリター実装 $`\newcommand{\MPL}{\m…

データ型 Nat Bool String Nil Basic := Nat | Bool | String | Nil Tree(X) List(X) 基本関数 Nat, Bool, String の色々 Tree: left, right, pair, isBasic List: fst, rest, cons, nth, isNil プログラム式の評価：$`\quad (p, \rho) \overset{E}{\mapsto}…

ラムダ記法＋適用：$`\quad (\lambda x\in X. P(x))(a) \equiv (P(x) \mid x = a)`$証明可能性：$`\quad \vdash_S (P(x) \mid x = a)`$エミュレーション：$`\quad \vdash_T \sigma(\ulcorner p \urcorner, a) \iff \vdash_S p(a)`$自己エミュレーション：$`\…

課題と参考文献： インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩：変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩：有限変換キューと半…

数学の時代区分 エジプト／バビロニア／中国の時代 事実と手法の集積 ギリシャ、ユークリッドは紀元前300年前後アレクサンドリアの人、 公理と証明の発明 19世紀 古典述語論理と集合論による厳密化・体系化、ヒルベルト ？ コンピュータで検証可能な記述 問…

いずれの描画法でも、平面を順方向エリアと逆方向エリアに区切っている。この区切り線を中心線と呼ぶことにする。代表的な3つの描画法を述べる。もちろん、他の選択肢もある。描画の約束によりファントム交差／ファントムカーブは生じる。相互変換には鏡映変…

アリーナ1 {旅行 → {1日目, 2日目, 3日目}} $`y^3`$ アリーナ2 {和 → {焼き魚, 煮魚, 刺し身}, 洋 → {グリルチキン}, 中華 → {エビチリ, 麻婆豆腐}} $`y^3 + y + y^2`$ アリーナ3 {和 → {羊羹, わらび餅}, 洋 → {ショートケーキ, モンブラン, ババロア}} $`y…

トレース付きモノイド圏の新しい定義 圏論的レンズ 4： テレオロジー圏 トレース付き圏の公理を次のように名付ける。 バニシング バンドリング （通常はバニシング 2） タイトニング スライディング ヤンキング スーパーポージング テレオロジー圏のトートロ…

確かムーアは論理式の集合の上の閉包作用素として演繹系を定義したと思う。アクツェルの推論系〈inference system〉の定義は以下のよう： 判断〈judgement〉の集合 U 演繹ルール〈deduction rule〉は A⊆U と c∈U の組 (A, c) 、これを A/c とも書く。 A を演…