\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔊w\Romannumeral{1}  ���� 5}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2011 �N 6 �� 25 �� (�y)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���̏ȗ��`�̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\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}
\]
% 2
\item
\begin{enumerate}
\item ������ \ $\rightarrow((\alpha \to \beta) \to \gamma) \to (\alpha \to \gamma) \to \neg\neg\gamma$ \ �Ɏ���̌n LJ
 �� cut �Ȃ��̏ؖ��}���������B
\item ������ \ $\rightarrow\neg\neg(((\alpha \to \beta) \to \alpha) \to \alpha)$ \ �Ɏ���̌n LJ
 �� cut �Ȃ��̏ؖ��}���������B
\end{enumerate}
% 3
\item
 ����_���̑̌n LJ �̊�{�藝�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
% 4
\item �_���� \ $p_0\to(((q \to p) \to p) \to r) \to r$
 \ �� �ÓT����_���̑̌n�ŏؖ��ł���Ȃ�΂ł��邱�Ƃ�, �ł��Ȃ��Ȃ�΂ł��Ȃ����Ƃ������B
%\vspace{5mm}
%\vspace{2mm}
%\vspace{5mm}
%\vspace{5mm}
\end{enumerate}
\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
%{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\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}
\]

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

{\bf ���ώ�`����_�� LJ} �̐��_�K���͎��� 6 �ł��B
% {\bf ���ώ�`�q��_�� 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}
