\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\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]
\newtheorem{lemma}[definition]{補助定理}
\newtheorem{theorem}[definition]{定理}
\newtheorem{corollary}[definition]{系}
\newtheorem{proposition}[definition]{命題}
\newtheorem{example}[definition]{例}
\newtheorem{remark}[definition]{注意}
\newtheorem{conjecture}[definition]{予想}
\newtheorem{problem}[definition]{問題}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{情報数学\Romannumeral{1}  試験 3}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2005 年 5 月 31 日 (火)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item
演繹定理を証明せよ。
\vspace{4mm}
% 2
\item\label{2} 
\begin{enumerate}
  \item $\vdash_{NJ} ((\alpha \to \beta) \to \gamma) \to (\alpha \to \gamma) \to \neg\neg\gamma$
    を示せ(すなわち, 式 $M: ((\alpha \to \beta) \to \gamma) \to (\alpha \to \gamma)
    \to \neg\neg\gamma$ が NJ で証明可能となる閉項 $M$ を見つけ, その式の証明図をえがく)。
  \item
    $\vdash_{NJ} \lambda xy.y(\lambda z.\mathsb{A}(xz(\lambda z.y(\lambda y.z)))):
     (\alpha\to\neg\neg\beta)\to\neg\neg(\alpha\to\beta)$ \ \ \ を示せ。
  \item\label{3}
    $\vdash_{NJ} \neg\neg\neg\neg\alpha\to\neg\neg\alpha$ \ \ を示せ。
  \item\label{4}
    $\vdash_{NJ} \neg\neg(\alpha\to\gamma)\to\neg\neg\alpha\to\neg\neg\gamma$ \ \ を示せ。
\end{enumerate}
\vspace{4mm}
% 3
\item 上の \ref{3}, \ref{4} で求めた閉ラムダ項をそれぞれ $U, V$ とする。
  $M$ を定数 $\mathsb{D}$ を含むかも知れないラムダ項とする。$\mathsb{D}$ を含ま
  ないラムダ項 $M^j$ を以下のように帰納的に定義する。
\begin{enumerate}
  \item $x^j \equiv \lambda y.yx \ ,$
% \item $x^j \equiv \lambda y.x \ と間違っていた。
  \item $(\mathsb{D}N)^j \equiv UN^j \ ,$
  \item $(\mathsb{A}N)^j \equiv (\lambda x.\mathsb{A}(x(\lambda x.x)))N^j \ ,$
  \item $(NR)^j \equiv VN^jR^j \ ,$
  \item $(\lambda x.N)^j \equiv (\lambda xy.y(\lambda z.\mathsb{A}(xz(\lambda z.y(\lambda y.z)))))
    (\lambda x.N^j) \ .$
\end{enumerate}
このとき, $\Gamma \vdash_{NK} M:\gamma$ ならば $\Gamma \vdash_{NJ} M^j:\neg\neg\gamma$ であることを
  ラムダ項 $M$ の長さについての帰納法で証明せよ。(体系 NK の定義は次ページにある。)
\vspace{4mm}
% 4
\item 次の省略形の推論図の正規形をもとめよ。途中経過も書くこと。また, 必要最小限の $\alpha$-変換
	をすること。正規形については省略形でないものをえがけ。
\[\infer{\gamma}{
\infer{\alpha\to\gamma}{
	\infer[\lambda y]{\beta\to\alpha\to\gamma}{
		\infer[\lambda x]{\alpha\to\gamma}{
			\infer{\gamma}{
				\infer{\beta\to\gamma}{z:\alpha\to\beta\to\gamma & x:\alpha} &
				y:\beta }}}	&
	\infer{\beta}{y:\alpha\to\beta & x:\alpha}}	&
	x:\alpha }
\]
\end{enumerate}
\newpage
{\bf 古典命題論理\index{こてんめいだいろんり@古典命題論理}
(classical propositional logic)} HK の公理型は次の 4 つである:
\[
\begin{array}{l}
\mathsb{K}: \alpha \to \beta \to \alpha \\
\mathsb{S}: (\alpha \to \beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma\\
\mathsb{P}: ((\alpha \to \beta) \to \alpha) \to \alpha \\
\mathsb{A}: \bot \to \alpha
\end{array}
\]

{\bf 直観主義命題論理(intuitionistic propositional logic)} NJ の推論規則は次の 3 つである:
\[ \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}  \ \ .\]

{\bf 古典命題論理}\index{こてんめいだいろんり@古典命題論理} NK は体系 NJ に次の
二重否定の除去規則を付け加えたものである:
\[ \infer{\mathsb{D}M:\alpha}{M:\neg\neg\alpha}\ \ . \]

\begin{definition}[抽象]\label{def-abstract}\em \ 
$M$ を CL-項, $x$ を変数とする. 変数 $x$ を含まない項 $(\lambda^* x.M)$ を以下のように
帰納的に定義する.
	\begin{enumerate}
		\item $(\lambda^* x.M) \equiv (\mathsb{K}M)$ \ \ ($x \notin FV(M)$ のとき),
		\item $(\lambda^* x.x) \equiv \mathsb{I}$ \ \ (ただし $\mathsb{I} \equiv \mathsb{SKK}$),
		\item $(\lambda^* x. UV) \equiv \mathsb{S}(\lambda^* x.U)(\lambda^* x.V)$ \ \ ($x\in FV(UV)$ のとき).
	\end{enumerate}
\end{definition}

\begin{theorem}[演繹定理]\label{eneki-teiri}\em
$x:\alpha,\Gamma \vdash_{HK} M:\beta$ \ \ かつ \ \ $\Gamma$ \ \ に変数 $x$ が現れないならば \ \ 
$\Gamma \vdash_{HK} \lambda^* x.M:\alpha \to \beta$ \ \ である.
\end{theorem}

\end{document}
