\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof2}
\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}}
\def\ra{\rightarrow}
\title{��񐔊w\Romannumeral{1}  ���� 6}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2004 �N 7 �� 20 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ $(((q \to p)\to\neg q)\to r) \ra r$
 \ �� �ÓT�_���̑̌n LK �ŏؖ��ł���Ȃ�Ώؖ��}������, �ؖ��ł��Ȃ��Ȃ�΂��̂��Ƃ��Ƃ������B
% 2
\item �_���� \ \ $\forall x ((px \to q) \to q)\to\neg q\to\forall x\ \neg\neg px$
 \ \ �̏q��_���̑̌n NJ �̏ؖ��}���������B
%\vspace{5mm}
% 3
%\vspace{2mm}
\item �_���� \ $\forall y(\forall x(\neg pxx\to pxy)\to\forall x(pxy\to\neg pxx)\to pyy)$
 \ �̏q��_���̑̌n NJ �̏ؖ��}��������.
% 4
\item ���̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[\infer{\gamma}{
\infer{\alpha\to\gamma}{
	\infer[2]{\beta\to\alpha\to\gamma}{
		\infer[1]{\alpha\to\gamma}{
			\infer{\gamma}{
				\infer{\beta\to\gamma}{\deduce{\alpha\to\beta\to\gamma}{3} & \deduce{\alpha}{1}} &
				\deduce{\beta}{2}}}}	&
	\infer{\beta}{\deduce{\alpha\to\beta}{2} & \deduce{\alpha}{1}}}	&
	\deduce{\alpha}{4}}
\]
%\vspace{5mm}
% 5
\item
�q��_�� HJ �̉�㈒藝 �u$\alpha,\Gamma \vdash_{HJ} \beta$ \ \ �Ȃ�� \ \ 
$\Gamma \vdash_{HJ} \alpha \to \beta$ \ \ �ł���v���ؖ�����B������,
$\vdash_{HJ} (\alpha \to \gamma \to \beta) \to (\alpha \to \gamma) \to
\alpha \to \beta$ �ł��邱�Ƃ͗p���Ă悢�B
%\vspace{5mm}
\end{enumerate}
\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă��邱�Ƃ�����B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\bf ���ώ�`�q��_�� HJ} �̌����^�͎��� 7 �ł��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 \\
(N) & \bot \to \alpha \\
(F1) & \forall x \alpha \to [t/x]\alpha \\
(F2) & \forall x (\alpha \to \beta) \to \alpha \to \forall x \beta \\
\end{array}
\]

{\bf ���ώ�`�q��_�� HJ} �̐��_�K���͎��� MP �ƕ��Չ��K���ł��B 
\[
\infer{\beta}{\alpha \to \beta & \alpha},
\ \ \ \ \ 
\infer[\ \ \ ����������ɂ͕ϐ� x �����R�Ɍ���Ȃ�]{\forall x \alpha}{\alpha}.
\]

{\bf ���ώ�`�q��_�� NJ} �̐��_�K���͎��� 5 �ł��B
\[ \infer[\mbox{($\to$-E)}]{\beta}{\deduce{\alpha\to \beta}{\Pi_1}  & \deduce{\alpha}{\Pi_2}},
\hspace{7mm} \infer[k\mbox{($\to$-I)}]{\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}}
\]
\[
\infer[\mbox{($\bot$-E)}]{\alpha}{\deduce{\bot}{\Pi}}, \hspace{7mm}
\infer[\mbox{($\forall$-I)}]{\forall x \alpha}{\deduce{\alpha}{\Pi}}, \hspace{7mm}
\infer[\mbox{($\forall$-E)}]{[t/x]\alpha}{\deduce{\forall x \alpha}{\Pi}}
\]

{\bf �ÓT����_�� LK} �̌����^�͎��̂Q�ł��B
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \Theta 
\end{array} \]

{\bf �ÓT����_�� LK} �̐��_�K���͎��� 9 ����܂���, ���̂���
�_���L���Ɋւ��鐄�_�K���͎��� 2 �ł��B
\[
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \Theta, \Lambda}
	{\Gamma \rightarrow \Theta, \alpha &
	\beta, \Delta \rightarrow \Lambda}, \hspace{7mm}
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \Theta, \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \Theta, \beta}
\]
\end{document}
