素朴論理の基本主に変数 - (2nd) 檜山正幸のキマイラ飼育記

$\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right]} \newcommand{\cat}[1]{\mathcal{#1}}$ 基本

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

素朴論理とは

素朴集合論：公理的集合論＝素朴論理：形式論理

素朴集合論と素朴論理のどちらが先か（鶏と卵）の議論はしない（不毛！）。

変数に関する絶対厳守のルール

変数の型〈変域〉は必ずハッキリさせる。正体不明の変数を使ってはいけない。

変数の型〈変域〉は次のどれか。

集合
真の類（集合でも宇宙でもない）
宇宙

変数の型〈変域〉を明確にする宣言を {型}?{判断 | 宣言 | 環境 | コンテキスト〈文脈〉}などと呼ぶ。型理論の（論理も）同義語の多さは例えば：

型理論ってば

変数を含む命題

型コンテキストの構文は色々あるが、ここでは次の形を使う（決まっていれば構文は何でもいい！）。

$[var_1 \in type_1, \cdots \mid var_k \in type_k, \cdots ]$
同じ型の複数の変数はまとめてよい。ただし、あくまで略記。
縦棒の右がないときは、縦棒ごと省略してよい。ただし、あくまで略記。

縦棒の左に宣言されている変数を主題変数〈subject〉、右に宣言されている変数をパラメータ変数〈parameter〉と呼ぶ。パラメータ変数は定数〈constant〉とも呼ぶ。単に変数と言えば、主題変数のことが多い（曖昧だけど）。

例： $[n\in {\bf N}, x, y\in {\bf R} \mid a \in {\bf R}_{\ge 0}]$

[追記]縦棒の左右は逆のほうが良かった気がする。が、所詮暫定的な構文だから修正はしない。[/追記]

注意：特定具体物を表す記号表現はリテラルという。定数がパラメータの意味かリテラルの意味かハッキリさせること。

論理式 $P$ が変数を含むなら、その変数（パラメータも含む）はすべて型コンテキストで宣言されている必要がある。型コンテキストは暗黙に想定されるが、それが諸悪の根源。省略は慣れた人間がやるもので、入門者・初心者が省略しては絶対にダメ。慣れるまでは面倒でも省略しないで律儀にちゃんと書く。

型コンテキストを $\Gamma, \Delta$ などのギリシャ大文字で表して、常に論理式に付けることにする。

例： $[n\in {\bf N}, x, y\in {\bf R}_{\ge 0} \mid a \in {\bf R}]\; x^n + y^n \le a$

変数を含む論理式を $P(x, y)$ のように書くとき、パラメータ変数〈定数〉は縦棒の後に書く（約束が決まっていれば何でもいい）。

例： $P(x, y \mid a) :\equiv x^n + y^n \le a$

論理式の真偽値

同義語を並べる。

真偽値 ＝真理集合＝解集合＝意味＝外延＝セマンティクス＝デノテーション＝値

$\quad \BR{ \Gamma\; P}$

と書く。これは、

型コンテキスト $\Gamma$ のもとでの論理式 $P$ の真偽値〈意味〉。

型コンテキスト $\Gamma$ に出現したすべての主題変数の型〈集合 | 変域〉を出現順に全部直積した集合を $X$ （論域という）、出現したすべてのパラメータ変数の型〈集合 | 変域〉を出現順に全部直積した集合を $A$ とすると：

$\quad \BR{ \Gamma\; P} : A \to \mrm{Pow}(X)$

論理式の意味〈真偽値 | 真理集合 | 解集合 | 外延 | セマンティクス | デノテーション | 値〉は、パラメータ領域でパラメータ〈インデックス〉付けられた集合族〈{parameterized | indexed} family of {sub}sets〉

注意：スコットブラケットのほうが広い範囲で使えるが、 $\{\Gamma \mid P\}$ と同じ。したがって、 $\{\Gamma \mid P\}$ も命題の真偽値〈真理集合 | 解集合 | 意味 | 外延 | セマンティクス | デノテーション | 値〉。

注意： $\mrm{Pow}({\bf 1}) = {\bf B}$

注意：論域やパラメータ域の構成は、正確に言えば直積を取るとは限らない。直積構成とは限らず一般にはパイ構成。

命題（型コンテキスト付き論理式）が真であるとは：

$\BR{ \Gamma\; P} = \lambda\, a\in A.X$

フビニの定理

元祖（積分）

$\quad {\displaystyle \int_{y\in Y} \left(\int_{x\in X} f(x, y)\,dx \right)\, dy}\\ = {\displaystyle\int_{x\in X} \left(\int_{y\in Y} f(x, y)\,dy \right)\, dx}\\ = {\displaystyle\int_{(x, y)\in X\times Y} f(x, y)\,d(x, y)}$

総和

$\quad {\displaystyle \sum_{j\in J} \left(\sum_{i\in I} f_{i, j} \right) }\\ = {\displaystyle \sum_{i\in I} \left(\sum_{j\in J} f_{i, j} \right)}\\ = {\displaystyle\sum_{(i, j)\in I\times J} f_{i, j}}$

総積

$\quad {\displaystyle \prod_{j\in J} \left(\prod_{i\in I} f_{i, j} \right) }\\ = {\displaystyle \prod_{i\in I} \left(\prod_{j\in J} f_{i, j} \right)}\\ = {\displaystyle\prod_{(i, j)\in I\times J} f_{i, j}}$

全称限量子

$\quad {\displaystyle \forall {y\in Y}. \left(\forall {x\in X}. P(x, y)\right) }\\ \equiv {\displaystyle\forall {x\in X}. \left(\forall {y\in Y}. P(x, y) \right)}\\ \equiv {\displaystyle\forall {(x, y) \in X\times Y}. P(x, y) }$

存在限量子

$\quad {\displaystyle \exists {y\in Y}. \left(\exists {x\in X}. P(x, y)\right) }\\ \equiv {\displaystyle\exists {x\in X}. \left(\exists {y\in Y}. P(x, y) \right)}\\ \equiv {\displaystyle\exists {(x, y) \in X\times Y}. P(x, y) }$

全称と存在の混合

$\forall x\in X. \exists y\in Y. P(x, y)$ 真なら全域セクションが取れる。横方向に延びた図形
$\exists x\in X. \forall y\in Y. P(x, y)$ 真ならフルファイバーが取れる。縦方向に延びた図形

存在と射影

$\quad \BR{[x\in X ]\;\exists y\in Y. P(x, y)} = \pi^1_{X, Y}(\BR{ [x\in X, y\in Y ]\;P(x, y)})$

型コンテキスト記述の例

コンテキストなしの命題

$\quad f;g = f;h \Rightarrow g = h$

直接的な型コンテキスト

$\quad [f \in \cat{C}(A, B), g, h\in \cat{C}(B, C) ]$

直接的な型コンテキストに出現する変数の型コンテキスト

$\quad [A, B, C \in |\cat{C}| ]$

直接的な型コンテキストに出現する変数の型コンテキストに出現する変数の型コンテキスト

$\quad [\cat{C} \in |{\bf Cat}| ]$

すべての型コンテキスト

$\quad [\cat{C} \in |{\bf Cat}|, A, B, C \in |\cat{C}|, f \in \cat{C}(A, B), g, h\in \cat{C}(B, C) ]$

型コンテキストの一部を限量子に組み込んで、整理する。

$[\\ \quad \cat{C} \in |{\bf Cat}|, \\ \quad A, B \in |\cat{C}|,\\ \quad f \in \cat{C}(A, B),\\ ]\\ \forall C\in |\cat{C}|.\\ \forall g, h\in \cat{C}(B, C). f;g = f;h \Rightarrow g = h$

型コンテキスト含めて命題の表現なのであり、論理式部分だけでは断片的情報でダメ！ 断片的情報で正確な議論が出来るわけがない。

キーワード／キーフレーズ

命題
論理式
述語〈predicate〉
主題〈subject〉＝変数
パラメータ＝定数
リテラル
型コンテキスト
パラメータ域
論域〈domain of discourse〉
真偽値
外延
等式、方程式、恒等式〈equation〉