|| 要請から実体を得て文の意味から真偽が
数学における『意味論』と考えて良いです
スポンサーリンク
目次
意味論「言語の意味とは何かを考察した成果」
モデル理論「意味論の言語を整論理式にした感じ」
理論「こうであって欲しいという要請（公理など）」
構造「モデルの候補として予想されるもの」
モデル「要請を満たす具体的な実体（集合の構成など）」
充足「モデルが要請を満たすこと」
解釈「文に『主観で』真理値を割り当てる」
環境「構造の中身を扱う写像みたいなもの」
変数割り当て「文の変数に値を入れて真偽を確定させる」
真理値割り当て「真理値を割り当てる関数」
言語「記号の数や引数の数が定義された記号の集まり」
L-集合モデル「言語と集合論に基づくモデル」
同型写像「言語に由来するモデル間の関係」
完全性定理「モデル内なら論理的帰結は証明可能と同義」
コンパクト性定理「一部にモデルがあるなら全体にも」
Löwenheim-Skolemの定理「一階の範囲なら無限を制御可能」
意味論 Semantics
|| 言語の真偽条件について考察した成果
「言語（入力）」から「真偽（出力）」を得る
\begin{array}{ccc} 言語 &\to& 言語を解釈 &\to& 真偽の判定 \end{array}
この「条件」を考察した成果が意味論で
\begin{array}{lcl} 意味論 && モデル理論 \\ \\ \\ 自然言語 && 形式言語（整論理式など）\\ \\ 真偽条件を与える && 真偽を厳密に評価 \\ \\ 真偽不確定（条件依存） && 真偽確定（モデル依存） \\ \\ 曖昧さ許容 && 曖昧さ排除 \end{array}
「モデル理論」はこの一部になります。
（モデル理論では確定で真偽が定まる）
モデル理論 Model Theory
|| 数学を使って具体的に制限した意味論
「真偽が確定するとは何か」を定めたもの
\begin{array}{lcc} 公理・定義の段階 && こんな感じであって欲しい \\ \\ モデルの定義段階 && こういう構成なら満たすはず \\ \\ \\ 充足の確認段階 && 実際に確認してみる \\ \\ 充足された段階 && 要請を満たすモデルの完成 \end{array}
この手順をより厳密化した成果がこれです。
（「言語」と「真偽」の橋渡し）
モデル理論の役割
形式的には ↓ みたいな感じで
\begin{array}{c} 命題 & 真偽 &\to& 解釈 & 真偽 \\ \\ \\ P_1 &\mathrm{Unknown} &\to& M(P_1) & \mathrm{Defined} \\ \\ P_2 &\mathrm{Unknown} &\to& M(P_2) & \mathrm{Defined} \\ \\ & & \vdots \\ \\ P_n &\mathrm{Unknown} &\to& M(P_n) & \mathrm{Defined} \end{array}
「真偽が定まっていない言語」に対して
「真偽を与える」というのがモデル理論の役割になります。
（言語から真偽への手順の全てをこの理論は扱う）
理論 Theory
|| こうなって欲しいという要望の集まり
「理論」というのは『直感を記号化したもの』で
\begin{array}{lcc} 理論の段階 && 記号化された要請 \\ \\ モデルの段階 && 要請を満たす具体的なもの \end{array}
その具体的な形は
\begin{array}{ccc} 非形式段階 && 直感的に理解できる && 真偽不明 \\ \\ 形式化段階 && こうだとしてみる && 矛盾する可能性 \\ \\ 形式段階 && こういうもの && 矛盾しない形 \end{array}
「こんな感じ」という「要請」を集めた
（モデル理論では形式化段階から扱う）
\begin{array}{ccc} 理論 &\Longleftrightarrow& 要請の集まり \end{array}
「形式言語で作られた文の集まり」になります。
（記号には形式言語の縛りがある）
モデル理論の文という概念
これは「広義の意味」では
当然「自由変数」を持つ概念ですが
\begin{array}{ccc} ただの文 && 真偽不明 \\ \\ モデル理論の文 && 真偽を確定させたい \end{array}
「モデル理論」では
「真偽が確定するもの」を扱いたいので
\begin{array}{ccc} 真偽が確定する文 \\ \\ ↓ \\ \\ 形式言語で書かれた自由変数を持たない文 \end{array}
「モデル理論で定義される文」には
\begin{array}{ccc} 形式言語で書かれてる &∧& 自由変数を持たない \end{array}
このような制限が課せられています。
（形式言語の代表例は整論理式）
構造 Structure
|| モデルの候補とも言えるけどって感じの概念
この記事では「モデルの候補」として扱いますが
\begin{array}{ccc} この記事での「構造」 &\to& モデルの候補 \\ \\ L\text{-}構造 &\to& ほぼモデルのこと \end{array}
文献によっては
「L-構造」なる概念で定義されていたりします。
（L-構造は意味論の指針に反するなど問題だらけなので不採用）
この記事では
意味論の指針に沿う形で
\begin{array}{ccc} 構造 &\Longleftrightarrow& 集合のように振舞う何か \\ \\ 構造 &\Longleftrightarrow& 言語を満たしそうな実体 \end{array}
「集合（あるいは型や圏）のようなもの」と定義しておきます。
（解釈という主観評価でしか使わないのでこれで十分）
厳密な定義として扱われるのは
\begin{array}{ccc} 構造 &\to& モデル &\to& 構造 \\ \\ 真偽不明 &\to& 真偽確定 &\to& 真偽確定 \\ \\ 何かの理論 &\to& 集合論 &\to& 集合論 \end{array}
「形式が定まる」という過程を経た後で
それまでは直感理解の段階にあると思ってください。
（モデルを経由することで構造は厳密に定義される）
モデル Model
|| 理論という要請を満たすなにか
「こうであってほしい」を満たすもの
\begin{array}{lcc} 理論の段階 && 記号化された要請 \\ \\ 構造の段階 && 要請を満たしそうな具体的なもの \\ \\ モデルの段階 && 充足が確認された \end{array}
「モデルだと予想されるもの（構造）」が
「要請を全て満たす」なら
\begin{array}{ccc} 構造が要請を満たす \\ \\ ↓ \\ \\ その構造がモデル \end{array}
その「構造」が「モデル」になります。
（つまり理論の要請を満たす構造がモデル）
充足 Satisfaction
|| 構造が要請を満たす
「充足」は「満たす」の言い換えで
\begin{array}{lcc} 理論の段階 && 記号化された要請 \\ \\ 構造の段階 && 要請を満たしそうな具体例 \\ \\ 充足の段階 && 構造が要請を満たす \end{array}
『構造が要請を満たす』の「満たす」を
（満足民ならサティスファクションで分かるはず）
\begin{array}{ccc} M\vDash φ &\Longleftrightarrow& 構造Mが文φを充足する \end{array}
「モデル理論」では「充足」と言います。
（充足が確認された構造のことをモデルと呼ぶ）
解釈 Interpretation
|| これは要請を満たしてるように思える
「充足する」を判定する段階で必要になる概念
\begin{array}{lcc} 予想段階 && 構造が候補に上がる \\ \\ 選定段階 && 構造と比較する要請の一文を選ぶ \\ \\ 解釈段階 && 構造が文を満たすか判定する \\ \\ 確認完了段階 && 要請の全てを調べ終わる \end{array}
これは「充足の段階」を細分化した時に出てくるもので
（与えられた要請となる文を読むのは人間や機械）
\begin{array}{lcc} 文の解釈段階 && モデル理論の文を読む \\ \\ 変数割り当て段階 && 自由変数があるなら固定する \\ \\ 構造の確認段階 && 構造が文を満たすか確認 \\ \\ 真理値割り当て段階 && 充足するなら真 \end{array}
「解釈段階」も更に細分化されることになります。
（変数の処理や真偽の出力はこの段階で行う）
環境 Assignment
|| 構造の中身を扱うための専用概念
これは見た目はほぼ「写像」のこと
\begin{array}{ccc} F&:& \mathrm{Variable} & \to& M_* \end{array}
「構造（集合にもなり得る）」を使って
「関数のような操作」を行うためのものになります。
（ほぼ変数割り当てを厳密に定義するためだけの概念）
変数割り当て Variable Assignment
これは一言で言うと
\begin{array}{ccc} \forall x\,\, φ(x) &\to& φ(x) &\to& φ(c) \end{array}
「自由変数を処理する操作」で
\begin{array}{ccc} φ(x,y) &&\to&& \mathrm{Const}(x)=a,\mathrm{Const}(y)=b \end{array}
具体的にはこんな感じのことをやります。
（自由変数を定数に置き換えて真偽を確定させる）
ちょっと分かり辛いかもしれませんが
これは「構造 M 」を使って
\begin{array}{ccc} \mathrm{Const}&:& \{文φの自由変数\} &\to& M_* \end{array}
こんな感じに定義されます。
（扱うものは構造の中身なので集合とは限らない）
真理値割り当て Satisfaction Relation
そのまま「真理値を割り当てる操作」のこと
\begin{array}{rlc} \mathrm{Boolean}(φ) &=& \left\{ \begin{array}{ccc} \mathrm{True} && M,\mathrm{Const} \vDash φ \\ \\ \mathrm{False} && M,\mathrm{Const} \not\vDash φ \end{array} \right. \end{array}
これの形式はこんな感じで
この \mathrm{Boolean} が「真理値割り当て」と呼ばれます。
（変数割り当て \mathrm{Const} が無いと定義できない操作です）
真理値 Truth Value
「真偽を表す値」のことで
\begin{array}{ccc} 真 & 偽 \\ \\ \\ 1&0 \\ \\ \mathrm{True} & \mathrm{False} \end{array}
だいたいこういうのが使われます。
（詳しくは『真理値』の記事を参考にしてください）
この部分だけ数学は主観に依存する
実はこの話で出てくる ↓ だけは
\begin{array}{ccl} M,\mathrm{Const} \vDash φ &\Longleftrightarrow&M,\mathrm{Const}はφを充足する \\ \\ M,\mathrm{Const} \vDash φ &\Longleftrightarrow&φはM,\mathrm{Const}の論理的帰結である \end{array}
「人間の主観」に完全に依存する部分で
（記号や操作は可能な限り厳密に与えられている）
\begin{array}{ccc} 仮にM,\mathrm{Const}が存在するなら \\ \\ 文φはその解釈の下では真である \end{array}
ここだけは機械的に判定されません。
（構造と環境の定義がふわっとしてて良い理由はこれ）
「形式言語」という縛りと
「主観の総体（多数決）」により
\begin{array}{lcc} 形式言語 &\to& 意味の曖昧さがほぼ無い \\ \\ 主観の総体 &\to& 不正な主観は排除される \end{array}
「ほぼ 100\% 正しくなる」んですが
この部分だけは他の数理概念とは根本的に異なります。
（ここだけ人間の「正しいと思う」が公理になる）
モデル理論の細分化
ざっとまとめると
\begin{array}{lll} 理論段階 \\ \\ & 形式言語化段階 \\ \\ 構造段階 \\ \\ & 予想段階 \\ \\ & 選定段階 \\ \\ & 解釈段階 \\ \\ &&文の解釈段階 \\ \\ && 変数割り当て段階 \\ \\ &&構造の確認段階 \\ \\ && 真理値割り当て段階 \\ \\ &確認完了段階 \\ \\ モデル段階 \end{array}
「モデル理論」ではこういうことをやっています。
（要請と構造から最終的にモデルが出力される）
厳密に定義されてる部分とそうじゃない部分
↑ のプロセスの厳密さですが
\begin{array}{lcc} 理論段階 && 厳密 \\ \\ 構造段階 && 記号だけ厳密 \\ \\ モデル段階 && 厳密 \end{array}
その内訳は実はこのようになっていて
（数理的に考察対象にできるのは理論とモデルの部分）
「構造段階」では
\begin{array}{ccc} 予想段階 && 主観的な予想 &&記号は厳密 \\ \\ 選定段階 && 主観的な選択 && 記号は厳密 \\ \\ 解釈段階 && 主観的な判断 && \vDash は主観的 \end{array}
特に「解釈段階」は主観に大きく寄っています。
（このためL-構造は実際には数理的に扱えない）
具体例の一部
全部やると長くなりすぎるのでやりませんが
\begin{array}{lcc} 自然数への要請 && ペアノの公理＋加法 \\ \\ 自然数の構造 && M=\{0,1,2,3\} \\ \\ 要請の一部を確認 && \forall n \,\, φ(n) \end{array}
「選定段階まで」の具体例はこんな感じで
（厳密にはもうちょい複雑）
\begin{array}{lcc} 文を読む && \forall n \,\, φ(n) \\ \\ 自由変数を定数へ && \mathrm{Const}(n)=1 && Mの中身を調べきるまで \\ \\ 構造が満たすか && φ(1) && 変数割り当てと確認をループ \\ \\ 真理値を割り当てる && \mathrm{Boolean}(φ) \end{array}
「解釈段階」はこんな感じです。
（確認完了段階は全ての要請を調べたという確認）
モデル理論の基本定理
ここからは「集合論」上の話で
（型理論を採用するなら型理論上の話）
\begin{array}{ccc} \mathrm{Model} &=& \Bigl( \mathrm{Elements},\mathrm{Constants},\mathrm{Functions},\mathrm{Relations} \Bigr) \end{array}
『形式言語 L で記述されている』という
「言語」の制限がある話になります。
（言語はほとんど整論理式）
言語 Language
形式的には ↓ のような形で与えられますが
\begin{array}{ccc} L&=& \{ \mathrm{Constants}, \mathrm{Functions}, \mathrm{Relations} \} \end{array}
この時点のこれには
『名前（表現のための記号）』が定まっておらず
\begin{array}{ccc} \mathrm{Constants} & \mathrm{Functions} & \mathrm{Relations} \\ \\ 定数記号1 & 関数記号1 & 関係記号1 \\ \\ \\ 0 & + & < \\ \\ a & \mathrm{Suc} & R \end{array}
そういった具体的な形は
「モデル」の段階で定まることになります。
（どの記号を採用するかは人間が決める）
L-集合モデル L-Model
確認しておくと
\begin{array}{ccc} \mathrm{Model} &=& \Bigl( \mathrm{Elements},\mathrm{Constants},\mathrm{Functions},\mathrm{Relations} \Bigr) \end{array}
これの中身は
\begin{array}{ccc} \mathrm{Elements} &\Longleftrightarrow& 定数と関数からの出力を全て集めた集合 \\ \\ \mathrm{Constants} &\Longleftrightarrow& 最初に必要な定数記号を集めたもの \\ \\ \mathrm{Functions} &\Longleftrightarrow& 入力から何かを出力することを意味する組 \\ \\ \mathrm{Relations} &\Longleftrightarrow& 要素同士の関係を表現するn\text{-}組 \end{array}
厳密にはこんな感じになっていて
この「モデル \mathrm{Model} 」が考察対象のメインになります。
（これは同型写像由来のモデルなのでL-構造ではない）
また生成の順番は以下のようになっていて
\begin{array}{ccc} 定数の確認段階 & \mathrm{Constants} \to \mathrm{Constsnts} \subset \mathrm{Elements} \\ \\ 関数の確認段階 & \mathrm{Functions} \subset \mathrm{Elements}\times \mathrm{Elements} \\ \\ 定数を入力する段階 & c,f(x) \\ \\ 関数の出力段階 & f(c) \to f(c) \in \mathrm{Elements} \\ \\ 記号の定義段階 & f(c)=a \end{array}
ここまでが「 \mathrm{Elements} の新たな要素の生成」過程
（全ての定数記号の入力から関数の出力を得る）
\begin{array}{ccc} 要素の確認段階 & a \in \mathrm{Elements} \\ \\ 関数の確認段階 & \mathrm{Functions} \subset \mathrm{Elements}\times \mathrm{Elements} \\ \\ 要素を入力する段階 & a,f(x) \\ \\ 関数の出力段階 & f(a) \to f(a)\in \mathrm{Elements} \\ \\ 記号の定義段階 & f(a)=b \end{array}
ここからが「 \mathrm{Elements} の全ての要素を得る」過程で
（全ての要素の入力から関数の出力を得る）
これが終わった後に
（ \mathrm{Elements} の全ての要素が揃う）
\begin{array}{ccc} \mathrm{Relations} & \subset & \mathrm{Elements}^n \end{array}
「関係記号」が定義されます。
（関係は要素を出力する操作ではない）
L-集合モデルの具体例
補足しておくと
\begin{array}{ccc} \mathrm{Natural} &=& \Bigl( N,\{0\},\{\mathrm{Suc}\},\{<\} \Bigr) \end{array}
「自然数のモデル \mathrm{Natural} 」の概形はこんな感じで
\begin{array}{lcr} && 0 \in \mathrm{Elements} \\ \\ \mathrm{Suc}(0)=1 &\to& 1 \in \mathrm{Elements} \\ \\ \mathrm{Suc}(1)=2 &\to& 2 \in \mathrm{Elements} \\ \\ &\vdots \end{array}
中身の生成過程はこんな感じになります。
（集合モデルの中身を分割している）
\begin{array}{ccl} \mathrm{Suc} &=& \{ (n,n+1) \mid n\in N \} \\ \\ < &=& \{ (n,m) \mid n,m\in N ,n\in m \} \end{array}
またこれらの定義は
集合論の文脈ではこのようになります。
言語を共有するモデルと同型写像
主要な基本定理を考察する道具として
\begin{array}{llcl} & M && N \\ \\ \mathrm{Constants} & \{c^M_1,c^M_2,...,c^M_i\} && \{c^N_1,c^N_2,...,c^N_i\} \\ \\ \mathrm{Functions} & \{f^M_1,f^M_2,...,f^M_j\} && \{f^N_1,f^N_2,...,f^N_j\} \\ \\ \mathrm{Relations} & \{R^M_1,R^M_2,...,R^M_k\} && \{R^N_1,R^N_2,...,R^N_k\} \end{array}
「言語が同じ異なるモデル」の間には
\begin{array}{ccc} F &:& M &\to& N \end{array}
「記号の全対応」を意味する
「全単射の写像 F 」が定義されていて
（記号の数や引数の数が完全一致するという意味で同型）
\begin{array}{ccc} F(c^M) &=& F(c^N) \\ \\ F\Bigl( f^M(a_1,a_2,...,a_n) \Bigr) &=& f^N\Bigl( F(a_1),F(a_2),...,F(a_n) \Bigr) \\ \\ (a_1,a_2,...,a_m)\in R^M &\Leftrightarrow& \Bigl( F(a_1),F(a_2),...,F(a_m) \Bigr)\in R^N \end{array}
この F は「 \mathrm{Elements} 以外」の「数が同じ」なら
「モデルは同型である」という
\begin{array}{ccc} M& \overset{f}{=} &N \end{array}
「 M と N の同値関係」として機能してくれます。
（これを基準にするとモデル同士が比較しやすい）
言語と同型写像
補足しておくと
\begin{array}{llcl} & M && N \\ \\ \mathrm{Constants} & \{c^M_1,c^M_2,...,c^M_i\} && \{c^N_1,c^N_2,...,c^N_i\} \\ \\ \mathrm{Functions} & \{f^M_1,f^M_2,...,f^M_j\} && \{f^N_1,f^N_2,...,f^N_j\} \\ \\ \mathrm{Relations} & \{R^M_1,R^M_2,...,R^M_k\} && \{R^N_1,R^N_2,...,R^N_k\} \end{array}
「定数記号・関数記号・関係記号の数」と
「関数記号・関係記号の引数の数」は
\begin{array}{ccc} L&=& \{ \mathrm{Constants}, \mathrm{Functions}, \mathrm{Relations} \} \end{array}
「言語 L 」の時点で定義されていて
これらが変動することはありません。
（言語の変更をする場合に変わる）
完全性定理 Completeness
|| モデル上の論理的帰結は証明可能を意味する
「理論 T 」と「 T を充足するモデル M 」が存在する場合
\begin{array}{ccc} 論理的帰結 && {} && 証明可能 \\ \\ T\vDash φ && ⇒ && T\vdash φ \end{array}
「論理的帰結（モデルにより真偽確定）」は
「証明可能」であることを意味する。
これがこの定理の主張で
\begin{array}{ccc} T\vDash φ &\Longleftrightarrow& \forall M \,\, M\vDash T⇒M\vDash φ \end{array}
この時の「論理的帰結」は
厳密にはこのように定義されています。
（モデルの存在により真偽確定が保証される）
証明の概形
これは「理論」「モデル」の存在から
\begin{array}{ccc} T\vDash φ_* && ⇒ && T\not\vdash φ_* \end{array}
このような「証明できない T の文 φ_* 」を考えることで
（背理法の手順を踏んで矛盾を得る）
\begin{array}{ccc} T∪\{\lnot φ_*\} &&\to&& M\vDash T ∧ M\vDash \lnot φ \end{array}
結果的に示すことができます。
（Henkinモデルや前提が長くなるので詳しくは別記事で）
コンパクト性定理 Compactness
|| 理論の一部にモデルがあるなら全体にもある
「理論の一部から理論全体のモデル」が得られる保証
\begin{array}{ccc} \mathrm{Model}(T_*) &\to& \mathrm{Model}(T) \end{array}
『一階述語論理』に強く依存する性質で
（一階述語論理が主に採用される理由がこの定理）
\begin{array}{ccc} 一部で矛盾する &\Longleftrightarrow& 全体が矛盾する \end{array}
この感覚を拡張したものになります。
（証明は長くなるので別記事で）
Löwenheim-Skolemの定理
|| 一階の言語なら無限を制御できる保証
「無限の段階」を柔軟に制御できるという保証
\begin{array}{ccc} 下方 && 可算無限へ \\ \\ 上方 && いくらでも上位の無限へ \end{array}
「上から」と「下から」に分かれています
（詳細は長くなるでこれも別の記事で）