雑記帳
始対象と終対象
始対象 (initial object)
定義
(..)
一階の言語による定義
始対象 \(\varnothing\) は、それぞれ以下を満たす射 \(X\) として定義される。
\[
{\rm isInitial}(X) :\Leftrightarrow \forall f \forall g \forall \Lambda[(f:X\rightarrow \Lambda \wedge g:X\rightarrow \Lambda) \Rightarrow f=g]
\]
始対象の定義より、任意の対象 \(A:A\rightarrow A\) は、終対象 \(\varnothing\) に固有の一意的な射 \(!_{\varnothing,A}:\varnothing \rightarrow A\) を引き起こすのだが、便利のため与えられた射 \(h\) がその射であることを判定する述語を以下のようにして定義しておく。
\[
{\rm isUniqueArrFromInitial}(h,A,X) :\Leftrightarrow {\rm isInitial}(X) \wedge {\rm \_cod}(h,A)
\]
終対象 (terminal object)
定義
(..)
一階の言語による定義
終対象 \(1\) は、それぞれ以下を満たす射 \(X\) として定義される。
\[
{\rm isTerminal}(X) :\Leftrightarrow \forall f \forall g \forall L[(f:L\rightarrow X \wedge g:L\rightarrow X) \Rightarrow f=g]
\]
終対象の定義より、任意の対象 \(A:A\rightarrow A\) は、終対象 \(1\) に固有の一意的な射 \(!_{A,1}:A \rightarrow 1\) を引き起こすのだが、便利のため与えられた射 \(h\) がその射であることを判定する述語を以下のようにして定義しておく。
\[
{\rm isUniqueArrToTerminal}(h,A,X) :\Leftrightarrow {\rm isTerminal}(X) \wedge {\rm \_dom}(h,A)
\]
一意的に定まらない射に記号を割り当ててよいのか？
確かにその記号が、概念を定義する一階の言語で書かれた文の中で使用されていたら問題かもしれないが、あくまで記号の割り当ては、公理を使った演繹を間接的かつわかりやすくするために導入される表記の上だけでの話となっている。
具体的に例えば
\[
\forall A \forall B[A = \varnothing \wedge B = \varnothing \Rightarrow A=B]
\]
というように、形式化する文の中で一意的でない \(\varnothing\) が用いた文を想定してみる。
\(\varnothing\) はあくまで \({\rm isInitial}(X)\) を真にするような "任意の" 射 X として用いるため、上の文は
\[
\forall A \forall B[\forall X [{\rm isInitial}(X) \Rightarrow (A = X \wedge B = X \Rightarrow A=B)]]
\]
或いは
\[
\forall A \forall B[\forall X \forall Y [({\rm isInitial}(X) \wedge isInitial(Y)) \Rightarrow (A = X \wedge B = Y \Rightarrow A=B)]]
\]
などというように複数通りの解釈ができる。
タグ一覧: