\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}}
\title{��񐔊w\Romannumeral{1}  ���� 6}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2003 �N 7 �� 22 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ \ $\forall x ((px \to q) \to q) \to \forall x (q \to px) \to \forall x\ \neg\neg px$
 \ \ �̏q��_���̑̌n NJ �̏ؖ��}���������B
%\vspace{5mm}
% 2
%\vspace{2mm}
\item �_���� \ $\forall y(\forall x(\neg pxx\to pxy)\to\forall x(pxy\to\neg pxx)\to pyy)$
 \ �̏q��_���̑̌n NJ �̏ؖ��}��������.
% 3
\item ���̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\infer{\alpha\to\gamma}{
\infer[2]{((\beta\to\gamma)\to\gamma)\to\alpha\to\gamma}{
\infer[1]{\alpha\to\gamma}{
\infer{\gamma}{\deduce{(\beta\to\gamma)\to\gamma}{2} &
	\infer{\beta\to\gamma}{\deduce{\alpha\to\beta\to\gamma}{3} & \deduce{\alpha}{1}}}}}
&
\infer[3]{(\beta\to\gamma)\to\gamma}{\infer{\gamma}{\deduce{\beta\to\gamma}{3} & \deduce{\beta}{1}}}}
\]
% 4
\item �̌n NJ, HJ �͂Ƃ��ɏq��_���̑̌n�Ƃ���B$\Gamma \vdash_{NJ} \gamma$ �Ȃ��
$\Gamma \vdash_{HJ} \gamma$ �ł��邱�Ƃ��ؖ�����B(�q��_�� HJ �̉�㈒藝���g���Ă悢�B)
%\vspace{5mm}
% 5
\item �q��_���̑̌n LJ �̊�{�藝���q��_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
	(�̌n NJ �̐��K�ȏؖ��}�̒����Ɋւ���A�[�@�ɂ�邪, ������ 1 �̂Ƃ�, �Ō�Ɏg��ꂽ�K����
	�����K���̂Ƃ��͏ȗ����Ă悢�B�Ō�Ɏg���Ă���K���������K���̂Ƃ������������΂悢�B)
%\vspace{5mm}
\end{enumerate}
\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\bf ���ώ�`�q��_�� HJ} �̌����^�͎��� 7 �ł�.
\[
\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���� 2 �ł�. 
\[
\infer{\beta}{\alpha \to \beta & \alpha}, \hspace{7mm}
\infer{\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 ���ώ�`�q��_�� LJ} �̌����^�͎��̂Q�ł�.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]

{\bf ���ώ�`�q��_�� LJ} �̐��_�K���͎��� 8 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
\[
\infer[(w \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(c \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\alpha, \alpha, \Gamma \rightarrow \gamma}
\]
\[
\infer[(e \rightarrow)]
	{\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
	{\Delta, \alpha, \beta, \Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\alpha, \Delta \rightarrow \gamma}
\]
\item[�_���L���Ɋւ��鐄�_�K��]\ 
\[
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\beta, \Delta \rightarrow \gamma}, \hspace{7mm}
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \beta}
\]
\[
	\infer[(\forall \rightarrow)]
		{\forall x \alpha, \Gamma \rightarrow \gamma}
		{[t/x]\alpha, \Gamma \rightarrow \gamma}, \hspace{7mm}
	\infer[(\rightarrow \forall)]
		{\Gamma \rightarrow \Theta, \forall x \alpha}
		{\Gamma \rightarrow \Theta, \alpha}
\]
\end{description}

\end{document}
