\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}
\newtheorem{definition}{定義}[section]
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{情報数理学特論\Romannumeral{7}  試験 5}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2005 年 12 月 6 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item 論理式 \ $\forall x((px\to q)\to q)\to(\neg\neg\forall x \, \neg\neg px\to q)\to\neg\neg q$ \ が
	直観主義述語論理の体系 NJ で証明できることを示せ.
% 2
\item  $\forall x(\neg pxx\to pxy), \forall x(pxy\to\neg pxx) \vdash_{NJ} \bot$
 \ を示す直観主義述語論理の体系 NJ の証明図をえがけ。
%\vspace{5mm}
% 3
\item 次の推件式が体系 LK で証明できないことを示せ:
\[ \forall x \forall y \forall z ( rxy \to ryz \to rxz ), \forall x \exists y \, rxy \ra
		\exists x \, rxx .\]
%\vspace{2mm}
% 4
\item 次の推件式が体系 LK で証明できないことを示せ:
	\[ \forall x\, rxx \ra \forall x \forall y \forall z ( rxy \to rxz \to\neg ryz \to rzy) .\]
%\vspace{5mm}
% 5
\item 述語論理の体系 LJ の基本定理を述語論理の体系 NJ の正規化定理を使って証明せよ。
	(体系 NJ の正規な証明図の長さに関する帰納法によるが, 長さが 1 のとき, 最後に使われた規則が
	導入規則のときは省略してよい。最後に使われている規則が消去規則のときだけを書けばよい。)
%\vspace{5mm}
\end{enumerate}
\vspace{10mm}
%\newpage
%{\bf 注意:} これは試験終了後に回収しますので, 書き込みなどはしないで下さい。\\[2mm]
%
{\bf 注意:} 以下では, 細かな条件(変数条件など)は省略されている。
% また, LJ の体系は教科書とは
% 少し異なっている(右辺は空ということはなく, ちょうど一つの論理式)。

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

{\bf 直観主義述語論理 NJ} の推論規則は次の 5 つです。
\[ \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}}} \]
\[ \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} \]

{\bf 直観主義述語論理 LJ} の公理型は次の２つです.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]

{\bf 直観主義述語論理 LJ} の推論規則は次の 8 つです。
\begin{description}
\item[構造に関する推論規則]\ 
\[
\infer[(w \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(c \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\alpha, \alpha, \Gamma \rightarrow \gamma}
\]
\[
\infer[(e \rightarrow)]
	{\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
	{\Delta, \alpha, \beta, \Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\alpha, \Delta \rightarrow \gamma}
\]
\item[論理記号に関する推論規則]\ 
\[
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\beta, \Delta \rightarrow \gamma}, \hspace{7mm}
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \beta}
\]
\[
	\infer[(\forall \rightarrow)]
		{\forall x \alpha, \Gamma \rightarrow \gamma}
		{[t/x]\alpha, \Gamma \rightarrow \gamma}, \hspace{7mm}
	\infer[(\rightarrow \forall)]
		{\Gamma \rightarrow \forall x \alpha}
		{\Gamma \rightarrow \alpha}
\]
\end{description}

\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}

\end{document}
