\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{2002 �N 6 �� 25 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ $((q_0 \to q_0) \to p) \to (q \to r) \to (r \to q) \to r$
 \ �� �̌n HK �ŏؖ��ł��Ȃ����Ƃ�����.
\vspace{5mm}
% 2
\item ����_���̑̌n LJ �̊�{�藝(cut �����藝)�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
\vspace{5mm}
% 3
\item �̌n NJ, HJ �͂Ƃ��ɖ���_���̑̌n�Ƃ���B$\Gamma \vdash_{NJ} \gamma$ �Ȃ��
$\Gamma \vdash_{HJ} \gamma$ �ł��邱�Ƃ� HJ �̉�㈒藝���g���ďؖ�����B
\vspace{5mm}
% 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}{1}}
\]
\vspace{5mm}
\item �_���� \ \ $((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \neg\neg\alpha$
 \ \ �� NJ �̏ؖ��}���������B
\end{enumerate}
\newpage
{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]

{\bf ���ώ�`����_��}�̑̌n 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����_��}�̑̌n
 HK �̌����^�� HJ �� 5 �̌����^�Ǝ��� $L3$ �� 6 �ł��B
\[
\begin{array}{ll}
(L3) & ((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \alpha \\
\end{array}
\]

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

{\bf ���ώ�`����_��}�̑̌n LJ �̐��_�K���͎��� 7 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
\begin{description}
\item[����(weakening)]
$$
\infer[(w \rightarrow)]
	{\alpha, \Gamma \rightarrow \Theta}
	{\Gamma \rightarrow \Theta}
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\rightarrow w)]
	{\Gamma \rightarrow \gamma}
	{\Gamma \rightarrow}
$$
\item[�k��(contraction)]
$$
\infer[(c \rightarrow)]
	{\alpha, \Gamma \rightarrow \Theta}
	{\alpha, \alpha, \Gamma \rightarrow \Theta}
$$
\item[����(exchanging)]
$$
\infer[(e \rightarrow)]
	{\Delta, \beta, \alpha, \Gamma \rightarrow \Theta}
	{\Delta, \alpha, \beta, \Gamma \rightarrow \Theta}
$$
\item[�ؒf(cut)]
$$
\infer[(cut)]{\Gamma, \Delta \rightarrow \Theta}
	{\Gamma \rightarrow \alpha &
	\alpha, \Delta \rightarrow \Theta}
$$
\end{description}
\item[�_���L���Ɋւ��鐄�_�K��]\ 
\begin{description}
\item[$\to$ �Ɋւ���K��]
$$
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \Theta}
	{\Gamma \rightarrow \alpha &
	\beta, \Delta \rightarrow \Theta}
\ \ \ \ \ \ \ \ \ \ 
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \beta}
$$
\end{description}
\end{description}
�����S�Ă̐��_�K���ɂ����� $\Theta$ �͈�̘_��������Ȃ邩��񂩂ł���.

\end{document}
