\documentclass[11pt]{jarticle}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\usepackage{latexsym}
\usepackage{proof2}
\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]{�n}
\newtheorem{proposition}[definition]{����}
\newtheorem{example}[definition]{��}
\newtheorem{remark}[definition]{����}
\newtheorem{conjecture}[definition]{�\�z}
\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 6}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2005 �N 1 �� 25 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item  �_���� $((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \neg\neg\alpha$
�� NJ ��(�ȗ��`�łȂ�)�ؖ��}��������.
\vspace{4mm}
% 2
\item ���̂��Ƃ� HJ �̉�㈒藝�� $M_H$ �̒�`�ɂ��A�[�@�ɂ��ؖ�����:\\
$\Gamma \vdash_{NJ} M:\gamma$ \ \ �Ȃ�� \ \ $\Gamma \vdash_{HJ} M_H:\gamma$ \ \ �ł���.
\vspace{4mm}
% 3
\item 
����(�ȗ��`��)���_�}��(�ȗ��`�łȂ�)���K�`�����Ƃ߂�. �r���o�߂���������. �܂�,
�K�v�ŏ����� $\alpha$-�ϊ������邱��.
\begin{enumerate}
\item\label{normal_4}
\[\infer{\gamma}{
\infer{\alpha\to\gamma}{
	\infer[\lambda x]{\beta\to\alpha\to\gamma}{
		\infer[\lambda y]{\alpha\to\gamma}{
			\infer{\gamma}{
				\infer{\beta\to\gamma}{z:\alpha\to\beta\to\gamma & y:\alpha} &
				x:\beta}}}	&
	\infer{\beta}{x:\alpha\to\beta & y:\alpha}}	&
	u:\alpha}
\]
\item\label{normal_5}
\[
\infer{\alpha\to\gamma}{
\infer[\lambda x]{((\beta\to\gamma)\to\gamma)\to\alpha\to\gamma}{
\infer[\lambda y]{\alpha\to\gamma}{
\infer{\gamma}{x:(\beta\to\gamma)\to\gamma &
	\infer{\beta\to\gamma}{z:\alpha\to\beta\to\gamma & y:\alpha}}}}
&
\infer[\lambda z]{(\beta\to\gamma)\to\gamma}{\infer{\gamma}{z:\beta\to\gamma & y:\beta}}}
\]
\end{enumerate}
\vspace{4mm}
% 4
\item ���̃����_���͌^�t���\��? �^�t���\(���̃����_���� $M$ �Ƃ���)�Ȃ��
	$\vdash_{NJ} M:\alpha$ ���������_�}��`��. �^ $\alpha$�͂Ȃ�ׂ���ʓI�Ȍ^�����߂�.
	�^�t���\�łȂ��Ƃ��͂��̂��Ƃ��������:
	\[(1)\ \lambda xyz. xz(yz) \ ,\ \ \ (2)\ (\lambda xy.xy)(\lambda xy.x),\ \ \ 
		 (3)\ \lambda xy.xxy \ .\]
\end{enumerate}
%\vspace{4mm}
\newpage
{\bf ���ώ�`����_�� NJ} �̐��_�K���͎��� 3 �ł��B
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha},
\hspace{7mm}
 \infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}} \]
\[ \infer{\mathsb{A}M:\alpha}{M:\bot} \]

\vspace{5mm}
{\bf ���ώ�`����_��} HJ �̌����^�͎��� 3 �ł��B
\[
\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{A}: \bot \to \alpha
\end{array}
\]

\vspace{5mm}
\begin{definition}[����]\em \ 
$M$ �� CL-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ� CL-�� $(\lambda^* x.M)$ ���ȉ��̂悤��
�A�[�I�ɒ�`����.
	\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}

\vspace{5mm}
\begin{theorem}[HJ �̉�㈒藝]\label{eneki-teiri}\em
$x:\alpha,\Gamma \vdash_{HJ} M:\beta$ \ \ ���� \ \ $\Gamma$ \ \ �ɕϐ� $x$ ������Ȃ��Ȃ�� \ \ 
$\Gamma \vdash_{HJ} \lambda^* x.M:\alpha \to \beta$ \ \ �ł���.
\end{theorem}

\vspace{5mm}
�����_�� $M$ ���� CL-�� $M_H$ �ւ̕ϊ��͎��̂悤�ɋA�[�I�ɒ�`�����:
\[ x_H\equiv x, \ \ \mathsb{A}_H\equiv\mathsb{A} \ \ (MN)_H\equiv M_HN_H, \ \ (\lambda x.M)_H\equiv
\lambda^* x.M_H.\]

\vspace{5mm}
\end{document}
