\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\newtheorem{definition}{��`}[section]
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{corollary}[definition]{�n}
\newtheorem{proposition}[definition]{����}
\newtheorem{example}[definition]{��}
\newtheorem{remark}[definition]{����}
\newtheorem{conjecture}[definition]{�\�z}
\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔊w\Romannumeral{1}  ���� 6}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2006 �N 7 �� 18 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���̏ȗ��`�̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\infer{\alpha\to\delta\to\gamma}{
\infer[\lambda x]{((\beta\to\gamma)\to\delta\to\gamma)\to\alpha\to\delta\to\gamma}{
\infer[\lambda y]{\alpha\to\delta\to\gamma}{
\infer{\delta\to\gamma}{x:(\beta\to\gamma)\to\delta\to\gamma &
	\infer{\beta\to\gamma}{z:\alpha\to\beta\to\gamma & y:\alpha}}}}
&
\infer[\lambda x]{(\beta\to\gamma)\to\delta\to\gamma}{\infer[\lambda z]
	{\delta\to\gamma}{\infer{\gamma}{x:\beta\to\gamma & y:\beta}}}}
\]
\vspace{4mm}
% 2
\item 
\begin{enumerate}
\item ������ \ $(\alpha \to \beta) \to \alpha \ra \neg\neg\alpha$ \ ���̌n LJ �ŏؖ��\�ł��邱�Ƃ�
�����B
\item ������ \ $(\alpha \to \beta) \to \alpha \ra \alpha$ \ �Ɏ���̌n LK �� cut �Ȃ��̏�
���}�������B
\end{enumerate}
% 3
\item 
\begin{enumerate}
\item ������ \ $\alpha\to\gamma, (\alpha \to \beta) \to \gamma \ra \neg\neg\gamma$ \ ���̌n LJ �ŏ�
���\�ł��邱�Ƃ������B
\item ������ \ $\alpha\to\gamma, (\alpha \to \beta) \to \gamma \ra \gamma$ \ �Ɏ���̌n LK �� cut �Ȃ�
�̏ؖ��}�������B
\end{enumerate}
\vspace{4mm}
% 4
\item
 ����_���̑̌n LJ �̊�{�藝�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
% 5
\item ������ \ $(((q \to p)\to\neg q)\to r) \ra r$
 \ �� �ÓT�_���̑̌n LK �ŏؖ��ł���Ȃ�Ώؖ��}������, �ؖ��ł��Ȃ��Ȃ�΂��̂��Ƃ������B
\end{enumerate}
\newpage
{\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 �ÓT����_�� LK} �̌����^�͎��̂Q�ł�.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]

{\bf �ÓT����_�� LK} �� cut �ȊO�̐��_�K���͎��� 8 �ł��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}
	$$
	\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}
\end{document}
