\documentclass{jarticle}
% \documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newtheorem{definition}{定義}[section]
\newtheorem{lemma}[definition]{補助定理}
\newtheorem{theorem}[definition]{定理}
\newtheorem{proposition}[definition]{命題}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{情報数理学特論\Romannumeral{7}  試験 4}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2008 年 12 月 9 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item 論理式 \ $\forall x(\neg px\to q)\to\neg\forall x\, px\to q$ \ に至る
	古典述語論理の体系 NK の証明図をえがけ。
% 2
\item 論理式 \ $\forall x((px\to q)\to q)\to(\forall x \, px\to q)\to q$ \ に至る
	古典述語論理の体系 NK の証明図をえがけ。
% 3
\item 次の論理式が古典述語論理で証明できないことを示せ:
	\[ \forall x \forall y \forall z ( rxy \to ryz \to rxz )\to\forall x\, rxx \to
	 \exists x \forall y \, rxy \to\exists x \forall y \, ryx \to \forall x \forall y
	  ( \neg rxy \to ryx) .\]
%\vspace{5mm}
% 4
\item 次の論理式が古典述語論理で証明できないことを示せ:
\[ \forall x \forall y \forall z ( rxy \to ryz \to rxz ) \to \forall x \forall y \exists z
   (rxy\to (rxz\wedge rzy)) \to	\exists x \, rxx .\]
%\vspace{2mm}
% 5
\item 述語論理の体系 NJ の正規化定理を証明せよ。
%\vspace{5mm}
\end{enumerate}
\vspace{10mm}
%\newpage
%{\bf 注意:} これは試験終了後に回収しますので, 書き込みなどはしないで下さい。\\[2mm]
%
{\bf 注意:} 以下では, 細かな条件(変数条件など)は省略されている。
% また, LJ の体系は教科書とは
% 少し異なっている(右辺は空ということはなく, ちょうど一つの論理式)。

\begin{itemize}
\item $\neg \alpha$ は $\alpha \to \bot$ を
\item $\alpha \wedge \beta$ は $\neg(\alpha \to \neg \beta)$ を
\item $\exists x\ \alpha$ は $\neg \forall x \neg \alpha$ を
\end{itemize}
それぞれ略して書いたものとします.

{\bf 古典述語論理 NK} の推論規則は次の 6 つです。
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha} \hspace{5mm}
 \infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}} \hspace{5mm}
  \infer{\mathsb{A}M:\alpha}{M:\bot} \hspace{5mm} \]
\[ \infer{\mathsb{J}M: \forall x \alpha}{M: \alpha} \hspace{5mm}
 \infer{\mathsb{F}M: [t/x]\alpha}{M: \forall x \alpha} \hspace{5mm}
 \infer{\mathsb{D}M:\alpha}{M:\neg\neg\alpha}\ \ . \]

\begin{theorem}[述語論理 NJ の正規化定理(Normalization theorem for NJ)]\em
NJ の推論図は何回かの $\beta\mathsb{J}$-変形を行なうことにより正規形にすることができる.
\end{theorem}

\begin{definition}[構造(structure)]\label{def-structure}\em
言語 $\cal L$ の構造 $\cal A$ は次の 3 つのものから構成されています:
\begin{enumerate}
\item $\cal A$ の世界と呼ばれる空でない集合 $|\cal A|$.
	$|\cal A|$ の元を $\cal A$ の個体といいます.
\item 言語 $\cal L$ の各々の $n$ 変数関数記号 $f$ に対して, $|\cal A|$ から
 $|\cal A|$ への $n$ 変数関数 $f_{\cal A}$.
 (とくに, 0 変数関数記号 $e$ に対して, $e_{\cal A}$ は $\cal A$ の個体です.)
\item 言語 $\cal L$ の各々の $n$ 変数述語記号 $p$ に対して, $|\cal A|$ の $n$
 個の直積 $|{\cal A}|^n$ の部分集合 $p_{\cal A}$.
\end{enumerate}
\end{definition}

言語 $\cal L$ に $\cal A$ の個体の全ての名前を付け加えて得られる言語
を $\cal L(A)$ と書きます. 個体 $c$ の名前を $\bar{c}$ と書きます. 

$t$ を言語 $\cal L(A)$ の閉項とします. 次に ${\cal A}$ の個体 ${\cal A}(t)$
 を帰納的に定義します.
\begin{enumerate}
\item ${\cal A}(\bar{c}) = c$,
\item ${\cal A}(ft_1...t_n) = f_{\cal A}({\cal A}(t_1),...,{\cal A}(t_n))$.
\end{enumerate}

$\alpha$ を言語 $\cal L(A)$ の閉論理式とします. 次に $\alpha$ の真偽値
 ${\cal A}(\alpha)$ を帰
納的に定義します.
\begin{definition}\em \ 
\begin{enumerate} 
\item ${\cal A}(pt_1...t_n) = \top \Longleftrightarrow p_{\cal A}
({\cal A}(t_1),...,{\cal A}(t_n))$,
\item ${\cal A}(\bot) = \bot$,
\item ${\cal A}(\alpha \to \beta) = {\cal A}(\alpha) \to {\cal A}(\beta)$,
\item ${\cal A}(\forall x \alpha) = \top \Longleftrightarrow 
{\cal A} の任意の個体 c に対して {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{definition}

\begin{theorem}\em \ 
次が成り立っている:
\begin{enumerate} 
\item ${\cal A}(\neg\alpha) = \top \Longleftrightarrow {\cal A}(\alpha) = \bot$,
\item ${\cal A}(\alpha\wedge\beta) = \top \Longleftrightarrow {\cal A}(\alpha) = \top
   かつ {\cal A}(\beta) = \top$,
\item ${\cal A}(\exists x \alpha) = \top \Longleftrightarrow 
{\cal A} のある個体 c に対して {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{theorem}

\end{document}
