\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}  ���� 5}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2003 �N 7 �� 8 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ \ $\neg\neg(((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \alpha)$
 \ \ �̖���_���̑̌n NJ �̏ؖ��}���������B
%\vspace{7mm}
% 2
\item �_���� \ $((q_0 \to q_0) \to p) \to (q \to r) \to (r \to q) \to r$
 \ �� �̌n HK �ŏؖ��ł��Ȃ����Ƃ������B
%\vspace{7mm}
% 3
\item ����_���̑̌n LJ �̊�{�藝(cut �����藝)�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
%\vspace{7mm}
% 4
\item ���̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[\infer{\gamma}{
\infer{\alpha\to\gamma}{
	\infer[2]{\beta\to\alpha\to\gamma}{
		\infer[1]{\alpha\to\gamma}{
			\infer{\gamma}{
				\infer{\beta\to\gamma}{\deduce{\alpha\to\beta\to\gamma}{3} & \deduce{\alpha}{1}} &
				\deduce{\beta}{2}}}}	&
	\infer{\beta}{\deduce{\alpha\to\beta}{2} & \deduce{\alpha}{1}}}	&
	\deduce{\alpha}{4}}
\]
%\vspace{7mm}
\item HJ �̉�㈒藝( $\alpha,\Gamma \vdash_{HJ} \beta$ \ \ �Ȃ��
	 \ \ $\Gamma \vdash_{HJ} \alpha \to \beta$ \ \ �ł���) �� $\alpha,\Gamma \vdash_{HJ} \beta$ ��
	 �������_�}�̒����ɂ��Ă̋A�[�@�ŏؖ�����\\
	 (HJ �� $(\alpha \to \gamma \to \beta) \to (\alpha \to \gamma) \to \alpha \to \beta$
	 ���ؖ��ł��邱�Ƃ͎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 ����_�� NJ} �̐��_�K���͎��� 3 �ł��B
\[ \infer[\mbox{($\to$-E)}]{\beta}{\deduce{\alpha\to \beta}{\Pi_1}  & \deduce{\alpha}{\Pi_2}}
\hspace{7mm} \infer[k\mbox{($\to$-I)}]{\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}}
\]
\[
\infer[\mbox{($\bot$-E)}]{\alpha}{\deduce{\bot}{\Pi}} \hspace{7mm}
\]

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

{\bf ���ώ�`����_�� LJ} �̐��_�K���͎��� 6 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
\[
\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[�_���L���Ɋւ��鐄�_�K��]\ 
\[
\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}
\]
\end{description}
\end{document}
