$`\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]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%\newcommand{\When}{\Keyword{When } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Subject}{\Keyword{Subject } }%
\newcommand{\Profile}{ \Keyword{Profile } }%
\newcommand{\Notation}{ \Keyword{Notation } }%
%
\newcommand{\H}{\mathrm{H}}
\newcommand{\N}{\mathrm{N}}
\newcommand{\A}{\mathrm{A}}
`$
形式的定義
恒真述語（1 を値とする定数値関数）
$`\For X \in |{\bf Set}|\\
\Subject \mrm{True}_X : X \to {\bf B} \In {\bf Set}\\
\quad \ie \mrm{True}_X \in \mrm{Map}(X, {\bf B})\\
\Define \mrm{True}_X := \lambda\, x\in X. 1\\
\Profile \mrm{True} \in \prod_{X\in |{\bf Set}|} \mrm{Map}(X, {\bf B})
`$
肯定的判断「成立する」
$`\For X \in |{\bf Set}|\\
\Subject \H_X: \mrm{Map}(X, {\bf B}) \to {\bf B} \In {\bf Set}\\
\quad \ie \H_X \in \mrm{Map}( \mrm{Map}(X, {\bf B}), {\bf B} )\\
\Define \H_X := \lambda\, f\in \mrm{Map}(X, {\bf B}).\, f = \mrm{True}_X\\
\Profile \H \in \prod_{X\in |{\bf Set}|} \mrm{Map}(\mrm{Map}(X, {\bf B}), {\bf B})\\
\Notation \mrm{Holds}_X f := (\H_X(f) \; \in {\bf B}) \\
\Notation f \text{ は }X\text{ 上で成立する。} := (\H_X(f) \; \in {\bf B}) \\
`$
否定的判断「成立しない」
$`\For X \in |{\bf Set}|\\
\Subject \N_X: \mrm{Map}(X, {\bf B}) \to {\bf B} \In {\bf Set}\\
\quad \ie \N_X \in \mrm{Map}( \mrm{Map}(X, {\bf B}), {\bf B} )\\
\Define \N_X := \lambda\, f\in \mrm{Map}(X, {\bf B}).\, f \ne \mrm{True}_X\\
\Profile \N \in \prod_{X\in |{\bf Set}|} \mrm{Map}(\mrm{Map}(X, {\bf B}), {\bf B})\\
\Notation \mrm{NotHold}_X f := (\N_X(f) \; \in {\bf B})\\
\Notation f \text{ は }X\text{ 上で成立しない。} := (\N_X(f) \; \in {\bf B}) \\
`$
全称限量子の定式化
$`\For X \in |{\bf Set}|\\
\Subject \A_X: \mrm{Map}(X, {\bf B}) \to \mrm{Map}({\bf 1}, {\bf B}) \In {\bf Set}\\
\quad \ie \A_X \in \mrm{Map}( \mrm{Map}(X, {\bf B}), \mrm{Map}({\bf 1}, {\bf B} ) )\\
\Define \A_X := \text{割愛 or 口頭}\\
\Profile \A \in \prod_{X\in |{\bf Set}|}
\mrm{Map}( \mrm{Map}(X, {\bf B}), \mrm{Map}({\bf 1}, {\bf B} ) )
`$
定理
$`\require{AMScd}
\For X \in |{\bf Set}|\\
\quad \begin{CD}
\mrm{Map}(X, {\bf B}) @>{\A_X}>> \mrm{Map}({\bf 1}, {\bf B})\\
@V{\H_X}VV @VV{\H_{\bf 1}}V \\
{\bf B} @= {\bf B}
\end{CD}\\
\quad \text{commutative in }{\bf Set}
`$
$`\For X \in |{\bf Set}|\\
\quad \begin{CD}
\mrm{Map}(X, {\bf B}) @>{\A_X}>> \mrm{Map}({\bf 1}, {\bf B})\\
@V{\N_X}VV @VV{\N_{\bf 1}}V \\
{\bf B} @= {\bf B}
\end{CD}\\
\quad \text{commutative in }{\bf Set}
`$
$`\For X \in |{\bf Set}|\\
\quad \begin{CD}
\mrm{Map}(X, {\bf B}) @= \mrm{Map}(X, {\bf B})\\
@V{\N_X}VV @VV{\H_X}V \\
{\bf B} @>{\mrm{flip}}>> {\bf B}
\end{CD}\\
\quad \text{commutative in }{\bf Set}
`$
問題
$`\mathscr{F}`$ を、集合 $`X`$ 上で意味をもつ論理式だとする。上付きチルダ $`^\sim`$ は、ポインティング関数を表すとして、以下の3つは同じ意味であることを証明せよ。
- $`\mrm{Holds}_X\, \mathscr{F}`$
- $`\mrm{Holds}_{\bf 1} (\mrm{Holds}_X\, \mathscr{F})^\sim`$
- $`\mrm{NotHold}_{\bf 1} (\mrm{NotHold}_X\, \mathscr{F})^\sim`$
$`x`$ と $`x^\sim`$ を同一視して、下付きの $`_{\bf 1}`$ は省略するなら：
- $`\mrm{Holds}_X\, \mathscr{F}`$
- $`\mrm{Holds}\; \mrm{Holds}_X\, \mathscr{F}`$
- $`\mrm{NotHold}\; \mrm{NotHold}_X\, \mathscr{F}`$
