\documentclass[11pt]{jarticle}
\renewcommand{\to}{\supset}
\usepackage{latexsym}
%\usepackage{proof2}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
% \def\ra{\rightarrow}
% \renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{��񐔊w\Romannumeral{1}  ���� 2}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2004 �N 5 �� 18 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item\label{c-p1.1} $\delta(K(CKK)\alpha\beta) \rhd \delta\beta$ �Ɏ��� CLw �̏ؖ��}������.
%\vspace{7mm}
% 2
\item $B(BW)(BBC)(CKK)\alpha\beta \rhd \beta(\alpha\beta)$ ���̌n CLw �ŏؖ��\�ł��邱�Ƃ�����(�K�������ؖ��}��`���Ȃ��Ă��悢).
\vspace{7mm}
% 3
\item �C�ӂ̍� $\alpha$ �ɑ΂���, ���̎����̌n CLw �ŏؖ��ł���ϐ� $x$, $y$ ���܂܂Ȃ��� $\beta$
	�����݂��邱�Ƃ�����: \[ \beta xy \rhd \alpha \ . \]
\vspace{7mm}
% 4
\item
	\begin{enumerate}
		\item\label{p1.-1} �_���� $\alpha\to(\alpha\to\beta)\to\gamma\to\beta$ �� HK �̏ؖ��}��
		�������B(�q���g: $C(BK)$) 
		\item\label{p1.2} �_���� $(\neg\alpha \to \neg\neg\alpha) \to \alpha$ �� HK �̏ؖ��}���������B
		(�q���g: $B(C(L3)N)W$)
	\end{enumerate}
\end{enumerate}
\newpage
�̌n CLw �̌����^�͎��� 4�ł�.
\[
\begin{array}{ll}
(B) & B\alpha\beta\gamma \rhd \alpha(\beta\gamma) \\
(C) & C\alpha\beta\gamma \rhd \alpha\gamma\beta \\
(K) & K\alpha\beta \rhd \alpha \\
(W) & W\alpha\beta \rhd \alpha\beta\beta \\
(\rho) & \alpha \rhd \alpha \\
\end{array}
\]

�ؖ��}�͌�����t�Ƃ���؏�̐}�`�ł�. �ؖ��}����邽�߂̋K����
{\bf ���_�K��\index{������񂫂���@���_�K��}(rule of inference)}�Ƃ����܂�. 
 �̌n CLw �̐��_�K���͎��� 3 �ł�:
\[
\infer[(\mu)]{\alpha\beta \rhd \alpha\gamma}{\beta \rhd \gamma},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{\alpha\gamma \rhd \beta\gamma}{\alpha \rhd \beta},
\]
\[
\infer[(\tau)]{\alpha \rhd \gamma}{\alpha \rhd \beta & \beta \rhd \gamma}.
\]
\\[1cm]

{\bf �ÓT����_��} HK �̌����^�͎��� 6 �ł��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 \\
(L3) & ((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \alpha \\
(N) & \bot \to \alpha
\end{array}
\]

\end{document}
