\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}  ���� 2}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2010 �N 11 �� 02 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
%\vspace{2mm}
\item ���ώ�`�q��_���̑̌n NJ �ɂ���, �����������_�}���������B
\begin{enumerate}
\item \ $\forall x(\neg px\to q),\neg\forall x\neg\neg px\vdash_{NJ} \neg\neg q$ , \
\item \ $\forall x(\neg pxx\to pxy),\forall x(pxy\to\neg pxx)\vdash_{NJ}\bot$ .
\end{enumerate}
\vspace{5mm}
% 2
\item �ÓT�q��_���̑̌n LK �ɂ���, ���̐������̏ؖ��}���������B
\begin{enumerate}
\item $\forall x(px\to q),\neg\forall x\neg px\rightarrow q$ ,
\item $\forall x ((px \to r) \to q),\neg q\rightarrow\forall x\,px$ ,
\item $\forall x(\neg px\to q),\neg\forall x\, px\rightarrow q$ ,
\item $\forall x((px\to q)\to q),\forall x \, px\to q\rightarrow q$ .
\end{enumerate}
\vspace{5mm}
% 3
\item ���ώ�`�q��_���̑̌n LJ �� NJ �ɂ���, ���� (a) ���� (b) ��������邱�Ƃ��ؖ�����B
\begin{enumerate}
\item \ $\Gamma\rightarrow\gamma$ �� LJ �ŏؖ��\�ł���,
\item \ $\Gamma\vdash_{NJ}\gamma$\ .
\end{enumerate}
%\vspace{5mm}
\end{enumerate}
%\vspace{5mm}
\newpage
\noindent
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B\\
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B
{\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} \]
\\
�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}

�Q���c�F�����̒��ώ�`�q��_�� LJ �̑̌n�� LK �ɂ�����, �������̌㌏����̘_�����ɐ����������̂ł���B
\end{document}
