\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}}
\newtheorem{definition}{��`}[section]
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 1}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2007 �N 10 �� 23 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���̐������Ɏ���ÓT����_���̑̌n LK �� cut �Ȃ��̏ؖ��}�������B
\begin{enumerate}
\item \ $(\alpha \to \beta) \to \alpha \rightarrow \alpha$ \
\item \ $\alpha\to\gamma, (\alpha \to \beta) \to \gamma \rightarrow \gamma$ \
\end{enumerate}
%\vspace{4mm}
%\vspace{5mm}
% 2
%\vspace{2mm}
\item ���ώ�`�q��_���̑̌n NJ �ɂ�����, ���̘_�����̏ؖ��}���������B
\begin{enumerate}
\item \ $\forall x px \to (\forall x \neg px) \to q$ \ 
\item \ $\forall y(\forall x(\neg pxx\to pxy)\to\forall x(pxy\to\neg pxx)\to pyy)$
\end{enumerate}
% 3
\item �ÓT�q��_���̑̌n LK �ɂ�����, \\
	������ \ $\forall x ((px \to r) \to q), \neg q\rightarrow\forall x\ px$
 \ �̏ؖ��}���������B
%\vspace{5mm}
% 5
\item
���ώ�`�q��_�� HJ �̉�㈒藝 �u$x:\alpha,\Gamma \vdash_{HJ} M:\beta$ \ \ ���� \ \ $\Gamma$ \ \ �̎�
���ɕϐ� $x$ ������Ȃ��Ȃ�� \ \ 
$\Gamma \vdash_{HJ} \lambda^* x.M:\alpha \to \beta$ \ \ �ł���v�� $\lambda^* x.M$ �̒�`�ɂ��A�[
�@�ŏؖ�����B
%\vspace{5mm}
\end{enumerate}
\vspace{5mm}
%\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\bf ���ώ�`�q��_�� HJ} �̌����^�͎��� 5 �ł�.
\[
\begin{array}{l}
\mathsb{K}: \alpha \to \beta \to \alpha \\
\mathsb{S}: (\alpha \to \beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma\\
\mathsb{A}: \bot \to \alpha \\
\mathsb{F}: \forall x \alpha \to [t/x]\alpha \\
\mathsb{G}: \forall x (\alpha \to \beta) \to \alpha \to \forall x \beta 
\end{array}
\]

{\bf ���ώ�`�q��_�� HJ} �̐��_�K���͎��� MP �ƕ��Չ��K���ł��B 
$$
\infer{(MN): \beta}{M: \alpha \to \beta & N: \alpha}.
$$
$$
\infer{\mathsb{J}M: \forall x \alpha}{M: \alpha}
$$

{\bf ���ώ�`�q��_�� NJ} �̐��_�K���͎��� 5 �ł��B
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha} \hspace{5mm}
 \infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}} \]
\[ \infer{\mathsb{A}M:\alpha}{M:\bot} \hspace{5mm}
 \infer{\mathsb{J}M: \forall x \alpha}{M: \alpha} \hspace{5mm}
 \infer{\mathsb{F}M: [t/x]\alpha}{M: \forall x \alpha} \]

\begin{definition}[����]\label{def-abstract}\em \ 
$M$ �� CL-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ��� $(\lambda^* x.M)$ ���ȉ��̂悤��
�A�[�I�ɒ�`����.
	\begin{enumerate}
		\item $(\lambda^* x.M) \equiv (\mathsb{K}M)$ \ \ ($x \notin FV(M)$ �̂Ƃ�),
		\item $(\lambda^* x.x) \equiv \mathsb{I}$ \ \ (������ $\mathsb{I} \equiv \mathsb{SKK}$),
		\item $(\lambda^* x. \mathsb{J}U) \equiv \mathsb{G(J}(\lambda^* x.U))$,
		\item $(\lambda^* x. UV) \equiv \mathsb{S}(\lambda^* x.U)(\lambda^* x.V)$ \ .
	\end{enumerate}
\end{definition}
�Q���c�F�����̌ÓT�q��_�� LK �̌����^�͎��� 2 �ł�.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \Theta
\end{array} \]
�Q���c�F�����̌ÓT�q��_�� LK �� cut �ȊO�̐��_�K���͎��� 10 �ł�.
\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}
	$$
	\item[$\forall$ �Ɋւ���K��]
	$$
	\infer[(\forall \rightarrow)]
		{\forall x \alpha, \Gamma \rightarrow \Theta}
		{[t/x]\alpha, \Gamma \rightarrow \Theta}
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow \forall)]
		{\Gamma \rightarrow \Theta, \forall x \alpha}
		{\Gamma \rightarrow \Theta, \alpha}
	$$
	\end{description}
\end{description}
\end{document}
