\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof2}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{��񐔊w\Romannumeral{1}  ���� 3}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2002 �N 6 �� 4 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item
	\begin{enumerate}
		\item\label{p1.-1} �_���� $\alpha\to\alpha$ �̌����^ $W$ ���g��Ȃ� HJ �̏ؖ��}��
		�������B(�q���g: $CKK$)
		\item\label{p1.2} �_���� $\neg \neg \alpha \to \alpha$ �� HK �̏ؖ��}���������B
		(�q���g: $C(L3)N$)
	\end{enumerate}
%\vspace{7mm}
% 2
\item �_���� $(\alpha\to\beta\to\gamma)\to(\alpha\to\beta)\to\alpha\to\gamma$ �� NJ �̏ؖ��}
	�������B
\vspace{7mm}
% 3
\item $\Gamma \vdash_{NJ} \gamma$ �Ȃ�� $\Gamma \vdash_{HJ} \gamma$ �ł��邱�Ƃ��ؖ�����B
\vspace{7mm}
% 4
\item ���̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\infer{(\alpha\to\beta) \to \alpha\to\beta}
   {\infer[4]{\beta \to (\alpha\to\beta) \to \alpha\to\beta}
	       {\infer[3]{(\alpha\to\beta) \to \alpha\to\beta}
		   {\infer{\alpha\to\beta}
		       {\infer{\beta \to (\alpha\to\beta)}
		           {\infer[2]{(\alpha\to\beta) \to \beta \to
			    \alpha\to\beta}
	         {\infer[1]{\beta \to \alpha\to\beta}
		           {\deduce{\alpha\to\beta}{2}}}
			&
			    \deduce{\alpha\to\beta}{3}} &
			\deduce{\beta}{4}}
           }} &
    \deduce{\beta}{3}}
\]
\vspace{7mm}
\item ������ $\Gamma \ra \gamma$ �� LK �ŏؖ��\�ł���Ȃ�� $\Gamma \vdash_{HK} \gamma$ ��
	���邱�Ƃ�̌n HJ �� LJ �Ƃ̓��l���ƃO���x���R�̒藝���g���ďؖ�����B
\end{enumerate}
\newpage
{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]

{\bf ���ώ�`����_��} HJ �̌����^�͎��� 5 �ł��B
\[
\begin{array}{ll}
(B) & (\beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma \\
(C) & (\alpha \to \beta \to \gamma) \to \beta \to \alpha \to \ \gamma \\
(K) & \alpha \to \beta \to \alpha \\
(W) & (\alpha \to \alpha \to \beta) \to \alpha \to \beta \\
(N) & \bot \to \alpha
\end{array}
\]

{\bf �ÓT����_��}\index{���Ă�߂���������@�ÓT����_��}
 HK �̌����^�� HJ �� 5 �̌����^�Ǝ��� $L3$ �� 6 �ł��B
\[
\begin{array}{ll}
(L3) & ((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \alpha \\
\end{array}
\]

{\bf �Q���c�F�����̌ÓT����_��} LK �̌����^�͎��̂Q�ł��B
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & 
\end{array} \]

{\bf �Q���c�F�����̌ÓT����_��} LK �̐��_�K���͎��� 9 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
	\begin{description}
	\item[����(weakening)]
	$$
	\infer[(w \rightarrow)]
		{\alpha, \Gamma \rightarrow \Theta}
		{\Gamma \rightarrow \Theta}
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow w)]
		{\Gamma \rightarrow \Theta, \alpha}
		{\Gamma \rightarrow \Theta}
	$$
	\item[�k��(contraction)]
	$$
	\infer[(c \rightarrow)]
			{\alpha, \Gamma \rightarrow \Theta}
		{\alpha, \alpha, \Gamma \rightarrow \Theta}
	\ \ \ \ \ \ \ \ \ \ 
		\infer[(\rightarrow c)]
		{\Gamma \rightarrow \Theta, \alpha}
		{\Gamma \rightarrow \Theta, \alpha, \alpha}
	$$
	\item[����(exchanging)]
	$$
	\infer[(e \rightarrow)]
		{\Delta, \beta, \alpha, \Gamma \rightarrow \Theta}
		{\Delta, \alpha, \beta, \Gamma \rightarrow \Theta}
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow e)]
		{\Gamma \rightarrow \Theta, \beta, \alpha, \Lambda}
		{\Gamma \rightarrow \Theta, \alpha, \beta, \Lambda}
	$$
	\item[�ؒf(cut)]
	$$
	\infer[(cut)]{\Gamma, \Delta \rightarrow \Theta, \Lambda}
		{\Gamma \rightarrow \Theta, \alpha &
		\alpha, \Delta \rightarrow \Lambda}
	$$
	\end{description}
\item[�_���L���Ɋւ��鐄�_�K��]\ 
	\begin{description}
	\item[$\to$ �Ɋւ���K��]
	$$
	\infer[(\to \rightarrow)]
		{\alpha \to \beta, \Gamma, \Delta \rightarrow \Theta, \Lambda}
		{\Gamma \rightarrow \Theta, \alpha &
		\beta, \Delta \rightarrow \Lambda}
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow \to)]
		{\Gamma \rightarrow \Theta, \alpha \to \beta}
		{\alpha, \Gamma \rightarrow \Theta, \beta}
	$$
	\end{description}
\end{description}
\vspace{3mm}
{\bf �O���x���R�̒藝}\ \ ���̂Q�̏����͓��l�ł���B
\begin{enumerate}
\item $\Gamma \ra \Delta$ �� LK �ŏؖ��\�ł���B
\item $\neg \Delta, \Gamma \ra $ �� LJ �ŏؖ��\�ł���B
\end{enumerate}
\end{document}
