形式的定義 定理 問題 $`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\hyp}{\text{－} } \newcommand{\id}{\mathrm{id}} \newcommand{\In}{\text{ in } } \newcommand{\ie}{\text{i.e. }\: } \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcol…

次の2つのタイプの発言を考える。 ～ は成立するぞ。 ～ は成立しないぞ。 「～」の部分は、等式・不等式などの命題。構文をキチンと約束すれば「～」の部分は論理式だとしてよい。$`\newcommand{\mrm}[1]{\mathrm{#1}}`$発言の定式化〈数理モデリング〉とし…

全称限量子が関数と思えないのはなぜか？ 「限量子が関数なわけない」という思い込みもあるだろうが、独特な呼び名と書き方が大きな原因だろう。呼び名・書き方は習慣・伝統だから変えられない。が、個人・集団内で、一時的に変えるのは自由だ。フルスペルで…

ブール値関数の基礎事項をまとめる。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\hyp}{\text{－} } \newcommand{\id}{\mathrm{id}} \newcommand{\In}{\text{ in } } \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} …

どんな分野でも固有の歴史と文化があるから、分野固有の用語を変えることは（ほぼ）出来ない。が、翻訳することはできる。以下、ブール値とは、「true としての 1 または false としての 0」のこと。 論理の方言 普通の言い方 述語〈predicate〉 ブール値の…

ほんとに基本的なんだけど、納得も利用もなかなかに難しいようだ。が、ほんとに基本的なんだから納得してくれ。ほんとに基本的な同型による対応は、場合により同一視に使われる。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ in }} \newc…

古典論理の「ならば」を誤解・曲解したままで、「ならば」を使えない／間違える人は多い。「前件（$`\Rightarrow`$ の左側）が偽なら含意命題は真」というところがカナメ。$`\Rightarrow`$ は演算記号で関係記号ではない。のだが、関係記号としてもオーバー…

有限集合だけを考える。 $`A = \{a_1, a_2, a_3\}`$ $`B = \{b_1, b_2\}`$ $`C = \{c_1, c_2\}`$ $`A`$ を次のように描く、$`B, C`$ も同様。 関数も関係も集合だと思えば列挙可能。有限集合の世界では、あらゆるものが具体的に列挙可能。 関数は逆関数が作…

(仮名)アルファさんの図法は、ちょっと衝撃的だった。「こだわりのなさ」に驚いた。アルファ図法のアイディアをまとめておく。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\u}[1]…

(仮名)アルファさんの発想が面白い。本人のなかでは一貫している（飛躍がない）のかも知れない。「教わったとおりにやった」だけかも知れない。檜山が言ったであろうこと（あまり憶えてないが絶対言いそう）： 無限集合は難しいから最初は有限集合で考えたほ…

スパイダー〈デルタ〉を持つテンソル計算系では、スパイダー定理が成り立つ。あるいは、スパイダー定理の主張を公理として要請する。スパイダー定理は包括的な主張だが、より具体的な事例はいくらでも自分で作れるだろう。many spiders が2匹、3匹のときの簡…

[含意問題] 含意と論理順序が混同されており、その混同が常態化している。 [メタ問題] オブジェクトレベルとメタレベルの区別、命題と判断〈メタ命題〉の区別や使用法が難しい。 [イコール問題 1] イコール記号が等値じゃなくても使われる。やめさせたいが、…

我々（人類）は、名付けと名前解釈の問題で悩み続ける宿命なのだろう。我々は、直示（名付けによらない直接指示）コミュニケーションが特別な（同じ絵を見ていて、指差し可能とかの）場合しか出来ないから、名付け・名指しを避けられない。名指しによらない…

中身が同じでも、所属組織や肩書きが変われば違うモノ 「同じだけど違う」「違うけど同じ」に慣れるのは、どうも非常に難しいらしく、慣れるまでに何年もかかるかも知れない。 射〈morphism〉： 1-in 1-out 複射〈multimorphism〉： n-in 1-out (n = 0, 1, 2…

「慣れる」とは、いちいち考えなくても自然に反応できるようになること。サッカーで例えるなら、ボールに慣れるためにリフティング練習やトラップの練習を繰り返す。「慣れる」トレーニングは単純作業的になるのは致し方ない。基礎動作の反復練習とはそうい…

色々と紆余曲折・右往左往は忘れて結果だけまとめれば、出現する概念は少数で、後から見れば当たり前だったりする。 テーブルスキーマに相当する集合のリストを考える。 集合の直積を作る。 その直積の部分集合を考える。 部分集合と述語（ブール値の関数）…

「絵の描き方 3： 行列の掛け算」の続き、テンソルは主にブーリアン係数。ストリング図： 左から右に向きを付けているが、実際は向きは不要。https://tensornetwork.org/diagrams/ が向き無しのテンソルなので、参照するとよい。 ストランド図： 赤いグニョ…

ストリング図： 行列の掛け算は反図式順なので、右から左に描いてみた。 行列の掛け算： $`a\in X`$ と $`c\in Z`$ を固定して、$`h`$ の $`c`$行$`a`$列成分 $`h(c\leftarrow a) = h_a^c`$ を計算する。 赤いグニョグニョ矢印に沿って、$`y\in Y`$ を同時並…

「絵の描き方」の続き、あるいは詳細化。絵の実例を付ける。いつも思うのだが、 なんで描かないの？ ベン図が基本： 集合はひろがり 要素は一点 風船図： 集合（ひろがり）がいくつか集まっている。 “集まり方”は、直和もあれば、合併もある。 集まりのメン…

抽象的な概念に対してメンタルモデルを作るには、絵を描いたり簡単で親しみやすい事例を見つけたりする。現在の数学における概念的事物は、集合と写像から構成されるから、集合と写像を絵に描く技法は重要。とはいえ、特に変わったやり方があるわけでもなく…

マイルドな（心理的拒絶感が少ない）例：$`A \subseteq \mathrm{Pow}(X)`$ とする。すると、$`\mathrm{id}_A : A \to A`$ は恒等写像。ところで、$`A \subseteq \mathrm{Pow}(X)`$ だったので、$`\mathrm{id'}_A : A \to \mathrm{Pow}(X)`$ とみなせる。この…

グロタンディーク宇宙の階層があれば、大きな（より正確には「小さくない」「真に大きい」）有限集合は作れる。したがって、次は成立しない。 集合 $`x`$ が有限ならば、$`x`$ は小さい集合である。 グロタンディーク宇宙の定義は Wikipedia グロタンディー…

現在、おそらく最も強力な型システムを持つと思われるLean 4によるコード。型ファミリーや依存タプルを含む型を定義して、型チェックは型システムに任せる。プログラマは、データの整合性をチェックするようなコードは書かない。処理のみを書く。 /-- 既婚か…

「ピンとこない」「自分の直感に反する」「つかみどころがない」「意味がハッキリしない」などの感覚を持つ理由のかなりところ（大部分かも知れない）は、 具体的な作業をした経験がない このようなとき、「具体的な作業をしなさい〈get your hands dirty〉…

※ この記事は、清書して「ストリング図と相性が良いテンソル計算 2/2」の続きの記事にするかもしれない（しないかも知れない）。テンソル計算のストリング図で次のように輪〈ループ〉を作ると、それはトレース〈対角和〉になる。$`\newcommand{\I}{\mathrm{I…

基本 素朴論理とは 変数に関する絶対厳守のルール 変数を含む命題 論理式の真偽値 フビニの定理 全称と存在の混合 存在と射影 型コンテキスト記述の例 キーワード／キーフレーズ 素朴論理とは 素朴集合論 ： 公理的集合論 ＝ 素朴論理 ： 形式論理 素朴集合…

元記事： https://m-hiyama-memo.hatenablog.jp/entry/20180918/1537241141 参照のためにコピーした（わずかに変更）。「マイクロコスモ原理と構造の無限タワー」に補足。記法を少し改善する。「掛け算」「乗法」「積」などと呼ばれる演算の中置記法で使われ…