\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}  ���� 4}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2004 �N 6 �� 22 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ����_���̑̌n LJ �̊�{�藝(cut �����藝)�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
\vspace{4mm}
% 2
\item �_���� $\neg(\alpha \to \beta) \to \neg\neg\alpha$
 �� NJ �̏ؖ��}���������B
\vspace{4mm}
% 3
\item 
\begin{enumerate}
  \item
  $\vdash_{NJ} (\alpha\to\neg\neg\beta)\to\neg\neg(\alpha\to\beta)$ \ \ \ �����\\
  $\vdash_{NJ} \neg\neg(\alpha\to\gamma)\to\neg\neg\alpha\to\neg\neg\gamma$ \ \ �������B
  \item
  $\Gamma \vdash_{NK} \gamma$ �Ȃ�� $\Gamma \vdash_{NJ} \neg\neg\gamma$ �ł��邱�Ƃ�
  $\Gamma \vdash_{NK} \gamma$ ���������_�}�̒����ɂ��Ă̋A�[�@�ŏؖ�����B(�̌n NK ��
  ��`�͎��y�[�W�ɂ���B)
\end{enumerate}
\vspace{4mm}
% 4
\item ���̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\infer{\alpha\to\gamma}{
\infer[2]{((\beta\to\gamma)\to\gamma)\to\alpha\to\gamma}{
\infer[1]{\alpha\to\gamma}{
\infer{\gamma}{\deduce{(\beta\to\gamma)\to\gamma}{2} &
	\infer{\beta\to\gamma}{\deduce{\alpha\to\beta\to\gamma}{3} & \deduce{\alpha}{1}}}}}
&
\infer[3]{(\beta\to\gamma)\to\gamma}{\infer{\gamma}{\deduce{\beta\to\gamma}{3} & \deduce{\beta}{1}}}}
\]
\vspace{4mm}
\item ������ $\Gamma \ra \gamma$ �� LK �ŏؖ��\�ł���Ȃ�� $\Gamma \vdash_{HK} \gamma$ ��
	���邱�Ƃ�̌n HJ �� LJ �Ƃ̓��l���ƃO���x���R�̒藝���g����(��㈒藝�͎g�킸��)�ؖ�����B
\end{enumerate}
\newpage
{\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 �ÓT����_��}\index{���Ă�߂���������@�ÓT����_��} NK �͑̌n NJ �Ɏ���
��d�ے�̏����K��($\neg$-E)��t�����������̂ł���:
\[ \infer[(\mbox{$\neg$-E})]{\alpha}{\neg\neg\alpha}. \]

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

{\bf �Q���c�F�����̒��ώ�`����_��} LJ �̐��_�K���͎��� 6 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
	\begin{description}
	\item[����(weakening), �k��(contraction)]
	$$
	\infer[(w \rightarrow)]
		{\alpha, \Gamma \rightarrow \gamma}
		{\Gamma \rightarrow \gamma},
	\ \ \ \ \ \ \ \ 
	\infer[(c \rightarrow)]
			{\alpha, \Gamma \rightarrow \gamma}
		{\alpha, \alpha, \Gamma \rightarrow \gamma}
	$$
	\item[����(exchanging), �ؒf(cut)]
	$$
	\infer[(e \rightarrow)]
		{\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
		{\Delta, \alpha, \beta, \Gamma \rightarrow \gamma},
	\ \ \ \ \ \ \ \ 
	\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
		{\Gamma \rightarrow \alpha &
		\alpha, \Delta \rightarrow \gamma}
	$$
	\end{description}
\item[�_���L���Ɋւ��鐄�_�K��]\ 
	\begin{description}
	\item[$\to$ �Ɋւ���K��]
	$$
	\infer[(\to \rightarrow)]
		{\alpha \to \beta, \Gamma, \Delta \rightarrow \gamma}
		{\Gamma \rightarrow \alpha &
		\beta, \Delta \rightarrow \gamma},
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow \to)]
		{\Gamma \rightarrow \alpha \to \beta}
		{\alpha, \Gamma \rightarrow \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 \bot$ �� LJ �ŏؖ��\�ł���B
\end{enumerate}
\end{document}
