\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}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 3}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2005 �N 11 �� 8 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ $((r \to p) \to p) \to (q \to r) \to (r \to q) \to r$
 \ �� �ÓT����_���̑̌n HK �ŏؖ��ł��Ȃ����Ƃ������B
% 2
\item ���ώ�`�q��_���̑̌n NJ �ɂ�����, \\
	�_���� \ $\forall x((px\to q)\to q)\to(\neg\neg\forall x\neg\neg px\to q)\to\neg\neg q$
 \ �̏ؖ��}��������.
%\vspace{5mm}
% 3
%\vspace{2mm}
\item ���ώ�`�q��_���̑̌n NJ �ɂ�����, \\
	�_���� \ $\forall y(\forall x(\neg pxx\to pxy)\to\forall x(pxy\to\neg pxx)\to pyy)$
 \ �̏ؖ��}���������B
% 4
\item ����(�ȗ��`��)���_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
\[
\infer{(\alpha\to\beta) \to \alpha\to\beta}
   {\infer[\lambda u]{\beta \to (\alpha\to\beta) \to \alpha\to\beta}
	       {\infer[\lambda z]{(\alpha\to\beta) \to \alpha\to\beta}
		   {\infer{\alpha\to\beta}
		       {\infer{\beta \to (\alpha\to\beta)}
		           {\infer[\lambda y]{(\alpha\to\beta) \to \beta \to
			    \alpha\to\beta}
	         {\infer[\lambda x]{\beta \to \alpha\to\beta}
		           {y:\alpha\to\beta}}
			&
			    z:\alpha\to\beta} &
			u:\beta}
           }} &
    z:\beta}
\]
%\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��_�� 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} \]

{\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 \forall x \alpha}
		{\Gamma \rightarrow \alpha}
\]
\end{description}

\end{document}
