\documentclass[amstex]{jarticle}
%\documentclass{jarticle}
\usepackage{latexsym,amsmath,amsthm,proof}
%\usepackage{proof}

\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
 \pagestyle{plain}
\def\ra{\rightarrow}
\def\Ra{\Rightarrow}

\newtheorem{definition}{��` }[section]
\newtheorem{theorem}[definition]{�藝 }
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{expectation}[definition]{�\�z}

%\title{}
%\author{��t��w��w�@�@���w�����ȁ@���w��񐔗��w�R�[�X�@�I�O}
%\date{2009�N3��}
\begin{document}
\thispagestyle{empty}
\vspace*{1cm}
\begin{center}
{\large\gt ��t��w��w�@�@���w�����ȁ@\\[3cm]�C�m�_��}
\end{center}
\vspace*{1cm}
\begin{center}
{\huge\bf �q��_���̑̌n�ɂ�����$\forall$ �̓����K���ɂ���}
\end{center}
\vspace*{1cm}
\begin{center}
{\large\gt ���w��񐔗��w�R�[�X}
\end{center}
\vspace*{5mm}
\begin{center}
{\large\gt �I�O}
\end{center}

\setcounter{page}{0}

\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%�ڎ�
\tableofcontents

\newpage

%\maketitle
%\documentclass[titlepage]{jsarticle}
\section{�T�v}
�q��_���̑̌n�ɂ�����, {$\forall$} �̓����K���� {$\alpha$} ���� {$\forall x\alpha$} �𓱂���
�̂�, {$[y/x]\alpha$} ($\alpha$ �̎��R�Ɍ���� $x$ �� $y$ ������������)����
{$\forall x\alpha$} �𓱂����̂�����.  ��҂ɂ�����, $y\equiv x$ �Ƃ���ƑO�҂��������̂�,
��҂̋K���̂ق����������Ƃ͖��炩�ł���.  ���͑O�҂����҂�������邩�ǂ����ł���.  �����
�ؖ����邽�߂̑O�i�K�Ƃ���, ���ώ�`�q��_���̑̌n LJ\_ (LJ �� $[y/x]\alpha$ ����
$\forall x\alpha$ �𓱂��� $\alpha$ ���� $\forall x\alpha$ �𓱂��ɕς�������) ��
$\Gamma \rightarrow  \gamma$  �� cut �Ȃ��ŏؖ��\�Ȃ��, $[y/x]\Gamma \rightarrow
[y/x]\gamma$ ���̌n LJ\_ �� cut �Ȃ��ŏؖ��\�ł���Ƃ������Ƃ��ؖ����悤�Ǝ��݂�.  ������, ����͏ؖ�
�ł���, ���Ⴊ��������.  ���̔��Ⴊ������ $\forall x(qy\supset qx),qy\rightarrow \forall zqz$
�ł���.  ���̐������� LJ\_ �� cut �Ȃ��ŏؖ��ł��邪, ���̐������̎��R�� $y$ �� $z$ �������ē�
���� $\forall x(qz\supset qx),qz\rightarrow \forall zqz$ �� LJ\_ ��
cut �Ȃ��ŏؖ��ł��Ȃ�.  �܂�, $\forall x(qz\supset qx),qz\rightarrow \forall yqy$ ��
$\forall yqy\rightarrow \forall zqz$
�͂Ƃ��� LJ\_ �� cut �Ȃ��ŏؖ��ł���̂�, ���̐������� LJ\_ �� cut ���g���Əؖ��ł���.
���Ȃ킿, LJ\_ �ł� cut �����藝���������Ă��Ȃ�.  �����悤��, NJ\_ (NJ �� $[y/x]\alpha$ ����
$\forall x\alpha$ �𓱂��� $\alpha$ ���� $\forall x\alpha$ �𓱂��ɕς�������)
�ł�, $\forall x(qz\supset qx),qz\vdash _{NJ\_}\forall zqz$ ���������K�łȂ��ؖ��}�͂��邪,
���K�� NJ\_ �̏ؖ��}����邱�Ƃ��ł��Ȃ�.  �̂�, NJ\_ �ł͐��K���藝���������Ă��Ȃ�.

���O�ɏq�ׂ���� LJ �ł� cut �Ȃ��ŏؖ��ł�, NJ �ł͐��K�ȏؖ��}�����݂���.  ������, LJ �� NJ ��
�{���� cut �����藝�␳�K���藝���_������ $\alpha$-�ϊ��������̂𓯈ꎋ�����ɐ������邩��
���Ƃ��Ďc����.  �悭�m���Ă��鐳�K���藝�Ȃǂ̏ؖ��͈Öق̂����� $\alpha$-�ϊ������_������
���Ƃ̘_�����Ɠ��ꎋ���Ă��镔��������.  ���̒藝����萳�m�ɏq�ׂ�Ǝ��̂悤�ɂȂ��Ă���.

�Q���c�F�����̌n LJ �Ő����� $\Gamma \rightarrow \gamma$ ���ŏؖ��ł����,
$\Gamma, \gamma$ �� $\alpha$-�ϊ����ē����� $\Gamma^*, \gamma^*$ �����݂���,
$\Gamma ^*\rightarrow \gamma  ^*$ �� LJ �� cut �Ȃ��ŏؖ��\�ł���.

���R��㈑̌n NJ �ɂ���, $\Gamma \vdash_{NJ} \gamma $ �Ȃ��,
$\Gamma, \gamma$ �� $\alpha$-�ϊ����ē����� $\Gamma^*, \gamma^*$ �����݂���,
$\Gamma^*\vdash_{NJ} \gamma^*$ ������ NJ �̐��K�ȏؖ��}������.

�����̒藝�͐��������̌n�ł��� LJ\_ �� NJ\_ �ł����藧���Ă���.

$\alpha$-�ϊ��������̂𓯈ꎋ���Ȃ��Ă�, LJ �� cut �Ȃ��̏ؖ��}���� NJ �̐��K�Ȑ��_�}�͂悭
�m��ꂽ���@�ō�邱���ł���. ���l��, $\alpha$-�ϊ��������̂𓯈ꎋ���Ȃ��Ă�, NJ �̐��K��
���_�}���� LJ �� cut �Ȃ��̏ؖ��}����邱�Ƃ��ł���.

LJ\_ �� NJ\_ �ɂ��Ă�, NJ\_ ���K�Ȑ��_�}���� LJ\_ �� cut �Ȃ��̏ؖ��}����邱�Ƃ��ł��邪
LJ\_ �� cut �Ȃ��̏ؖ��}���� NJ\_ �̐��K�Ȑ��_�}����邱�Ƃ͂ł��Ȃ�.
���̗Ⴊ������ $qx\supset r,qx,\forall x(r\supset px)\rightarrow\forall xpx$ �ł���.
���̐������� LJ\_ �� cut �Ȃ��ŏؖ��ł��邪, $qx\supset r,qx,\forall x(r\supset px)\vdash_{NJ\_}
\forall xpx$ ������ NJ\_ �̐��K�Ȑ��_�}�͑��݂��Ȃ�.

�ŏ��ɏq�ׂ���u$\Gamma \rightarrow  \gamma$  �� LJ\_ �� cut �Ȃ��ŏؖ��\�Ȃ��,
$[y/x]\Gamma \rightarrow [y/x]\gamma$ ���̌n LJ\_ �� cut �Ȃ��ŏؖ��\�ł���v�Ƃ����͔̂��Ⴊ
������, ���̔���͑���̒�`�Ɉˑ����Ȃ����̂ɂȂ��Ă���.  ������, ���̂悤�ȑ���Ɋւ��
�藝�ɂ��Ă�, ����̒�`�Ɉˑ����Đ��藧���Ă����肢�Ȃ������肷��\��������.
���̔����, ��������܂���`����Ώؖ��ł���ƍl���Ă��낢��Ȓ�`�ŏؖ������݂����ʌ�������
���̂ł���.

�Ō��, ���̘_���͌ÐX�搶���ڍׂȕ��j��^�����, �����̌���, ���؂͛I�O���s�������̂ł���.
�܂�, �����ŏq�ׂ�����͂��ׂČÐX�搶�����������̂ł��邪, �I�ɂ��ؖ������܂������Ȃ��ꍇ��
���������̔����ɑ傫����^���Ă���.
%
\section{�q��_���̑̌n�̒�`}
�ÓT�q��_���ƒ��ώ�`�q��_���Ƃł͓����c�_���ł��邪, ���̘_���ł� $\forall$ �̓����K���̈Ⴂ
�𒲂ׂ邱�Ƃ��ړI�ł���̂�, �����ł͒��ώ�`�q��_�������ŋc�_����.
%\bigskip
\subsection{LJ��LJ\_�̒�`}
�܂��������̒�`����͂��߂�.
\begin{definition}[������]\label{4}\em
       $\alpha_1,...,\alpha_m,\beta$ ��_�����Ƃ���Ƃ�,
       \[\alpha_1,...,\alpha_m \rightarrow \beta\]
       �̌`�̕\����{\bf ������\index{�������񂵂�@������}(sequent)}�Ƃ���. ���̂Ƃ�, �_�����̗�
       $\alpha_1,...,\alpha_m$
       �����̐�������{\bf �O��\index{���񂯂�@�O��}(antecedent)}�Ƃ���,
       �_����$\beta$ �����̐�������
       {\bf �㌏\index{��������@�㌏}(succedent)}�Ƃ���.
\end{definition}

������ $\alpha_1,...,\alpha_m \rightarrow \beta$ �͘_����
$(\alpha_1 \wedge ... \wedge \alpha_m) \to \beta$
�Ɠ����Ӗ���\�킵�Ă���. �����O�����S���Ȃ��ꍇ(���Ȃ킿,
$m = 0$ �̂Ƃ�)�� �_���� $\beta$ �Ɠ����Ӗ��ɂȂ�.
$m$ ��� $\alpha_1,...,\alpha_m$ ��
{\bf ����\index{�Ȃ���@����}(length)}�Ƃ���.

���ώ�`�_���̑̌n LJ �͕��ʘ_���L���Ƃ���$\supset ,\vee ,\wedge  ,\wedge ,\bot ,\forall ,\exists $���܂�.
�����ł�$\supset ,\forall$ ��������Ȃ�, �̌nLJ��${\{\supset ,\forall\}}$ -�f�Ђ�LJ�ƌĂԂ��Ƃɂ���.
\begin{definition}[FV��V�̒�`]\label{2}\em \
�_����$\alpha$ �Ɋ܂܂��ϐ��̏W��$V(\alpha )$�Ǝ��R�ϐ��̏W��$FV(\alpha )$
�����̂悤�ɋA�[�I�ɒ�`����.
       \begin{enumerate}
                       \item$FV((\alpha\supset \beta)) = FV(\alpha)\cup FV(\beta)$, \ 
$V((\alpha\supset \beta)) = V(\alpha)\cup FV(\beta)$.
                        \item$FV(\forall x \alpha) = FV(\alpha)-\{x\}$, \ 
$V(\forall x \alpha) = V(\alpha)\cup \{x\}$.
       \end{enumerate}
$\Gamma$ ��_�����̏W���Ƃ���Ƃ�.\\
       $FV(\Gamma )=\bigcup\{FV(\alpha ) \mid \alpha \in \Gamma\}$,
   $V(\Gamma )=\bigcup \{V(\alpha ) \mid \alpha \in \Gamma\}$
�ƒ�`����.
\end{definition}
%\subsubsection{LJ��LJ\_�̒�`}\label{z:LJ}
�������̌n�ł���Q���c�F�����̒��ώ�`�q��_���̌n LJ �̌����^�Ɛ��_�K�����ȉ��ɏq�ׂ�.

�q��_���̌n LJ �̌����^�͈ȉ��ł���.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha
%(N) & \bot   & \rightarrow & \alpha
\end{array} \]

�q��_���̌n LJ �̐��_�K���͑S���� 8 �ł���. �\���Ɋւ���
���̂� 4 ��, �_���L���Ɋւ�����̂� 4 �ł���.

\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\
\begin{description}
\item[����(weakening)]
\
\infer[(w \rightarrow)]
       {\alpha, \Gamma \rightarrow \gamma}
       {\Gamma \rightarrow \gamma}
\
\item[�k��(contraction)]
\
\infer[(c \rightarrow)]
       {\alpha, \Gamma \rightarrow \gamma}
       {\alpha, \alpha, \Gamma \rightarrow \gamma}
\
\item[����(exchanging)]
\
\infer[(e \rightarrow)]
       {\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
       {\Delta, \alpha, \beta, \Gamma \rightarrow \gamma}
\
\item[�ؒf(cut)]
\
\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
       {\Gamma \rightarrow \alpha &
       \alpha, \Delta \rightarrow \gamma}
\
\end{description}
\item[�_���L���Ɋւ��鐄�_�K��]\
\begin{description}
\item[$\supset $ �Ɋւ���K��]
\
\infer[(\supset  \rightarrow)]
       {\alpha \supset  \beta, \Gamma, \Delta \rightarrow \gamma}
       {\Gamma \rightarrow \alpha &
       \beta, \Delta \rightarrow \gamma}
\ \ \ \ \ \ \ \ \ \
\infer[(\rightarrow \supset )]
       {\Gamma \rightarrow \alpha \supset  \beta}
       {\alpha, \Gamma \rightarrow \beta}
\
       \item[$\forall$ �Ɋւ���K��]
       \
       \infer[(\forall \rightarrow)]
               {\forall x \alpha, \Gamma \rightarrow \gamma}
               {[t/x]\alpha, \Gamma \rightarrow \gamma}
       \ \ \ \ \ \ \ \ \ \
       \infer[(\rightarrow \forall)]
               {\Gamma \rightarrow \forall x \alpha}
               {\Gamma \rightarrow [y/x]\alpha}
       \
\end{description}
\end{description}
%�����S�Ă̐��_�K���ɂ����� $\Theta$ �͈�̘_��������Ȃ邩��񂩂ł���.
���_�K��{$(\rightarrow  \forall)$}  �ɂ����Ă�,  �ϐ� $y$ ��
$y\not\in FV(\Gamma) \cup  FV(\forall x\alpha )$ �𖞂����Ă��Ȃ���΂Ȃ�Ȃ�.

���ώ�`�q��_���̑̌n LJ\_ ��LJ���ア�ő̌n �ł���.
�̌n LJ\_ �̌����^�Ɛ��_�K���� $(\rightarrow \forall )$�ȊO�� LJ �Ƃ܂����������ł���.\\
�̌n LJ\_ �� $(\rightarrow \forall )$ �K��:
%\begin{center}
%\begin{description}
\[      \infer[(\rightarrow \forall)]
               {\Gamma \rightarrow \forall x \alpha}
               {\Gamma \rightarrow \alpha}.
\]
%\end{center}
���̐��_�K���ɂ�����, �ϐ� $x$ �� $x\not\in FV(\Gamma)$ �𖞂����Ă��Ȃ���΂Ȃ�Ȃ�.

�̌n LJ (LJ\_) �Ő����� $\Gamma\rightarrow\gamma$ ���ؖ��\�ł��邱�Ƃ�
$\Gamma\vdash_{LJ}\gamma$ ($\Gamma\vdash_{LJ\_}\gamma$) �Ə������Ƃɂ���.

\subsection{NJ��NJ\_�̒�`}
%�܂��̎��R��㈑̌n�̒�`����͂��߂�.
%\begin{definition}[���R��㈑̌n]\em
%�̌n�r�ɂ�����, $\alpha ,\Gamma \vdash _{S}\beta $�Ȃ��,
%$\Gamma \vdash _{S}\alpha \supset \beta $�Ə���, �r��{\bf ���R��㈑̌n\index{�����񂦂񂦂���������@���R��㈑̌n}}�Ƃ���.
%\end{definition}
%\subsubsection{NJ�̒�`}
���ώ�`�q��_���̎��R��㈑̌n�ł��� NJ �� NJ\_ ���`����.
\begin{definition}[NJ �̐��_�}]\ \em
\begin{enumerate}
\item �C�ӂ̐��� $k$ �Ƙ_���� $\alpha$ �ɑ΂���, �ȉ��̐}�`�͐��_�}�ł���:
\[
 \deduce{\alpha}{k}
\]
\item
���_�} $\Pi_1$ �̈�ԉ��Ɍ����_������ $\alpha \supset  \beta$ �� ���_
�} $\Pi_2$ �̈�ԉ��Ɍ����_������ $\alpha$ �̂Ƃ�,
       ���̐}�`�͐��_�}�ł���:
\[
\infer{\beta}{\Pi_1 & \Pi_2}.
\]
���̂Ƃ�, �g��ꂽ���_�K���� $\supset$-E �ł���Ƃ���, ���_�K����
\[ \infer{\beta}{\alpha \supset  \beta & \alpha} \]
�Ƃ������.
\item ���_�} $\Pi$ �̂Ȃ��̗����Ă��Ȃ�����̂����� $k$ �̉��ɂ���_������ $\alpha$ ��
       ���Ƃ���(��ɂ��鐔�� $k$ �͌���Ȃ��Ă��悢). �܂�, $\Pi$ �̈�ԉ��Ɍ���鎮�� $\beta$ �ł����
       ����. ���̂Ƃ����̐}�`�͐��_�}�ł���:
\[
\infer[k]{ \alpha \supset  \beta}{\Pi}\ \ .
\]
���̂Ƃ�, �g��ꂽ���_�K���� $\supset$-I �ł���Ƃ���, ���_�K����
\[ \infer[k]{\alpha \supset  \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}} \]
�Ƃ������. ���̐��_�K�����g���܂ł͗����Ă��Ȃ��������� $\alpha$ ��(��������ΑS��),
���̐��_�K�����g��������, {\bf ������\index{������@������}(discharged)}�Ƃ���.
\item ���_�} $\Pi$ �̈�ԉ��Ɍ���鎮�� $[y/x] \alpha$ �ł����
       ����. �܂�, $\Pi$ �̗����Ă��Ȃ������ $\forall x \alpha$ �ɂ͕ϐ� $y$ �͎��R�Ɍ����
       �����̂Ƃ���. ���̂Ƃ����̐}�`�͐��_�}�ł���:
\[
\infer{ \forall x \alpha}{\Pi}.
\]
���̂Ƃ�, �g��ꂽ���_�K���� $\forall$-I �ł���Ƃ���, ���_�K����
\[ \infer{ \forall x \alpha}{[y/x]\alpha} \]
�Ƃ������.
\item ���_�} $\Pi$ �̈�ԉ��Ɍ����_������ $\forall x \alpha$ �ł����
       ����.  ���̂Ƃ����̐}�`�͐��_�}�ł���:
\[
\infer{ [t/x]\alpha}{\Pi}.
\]
���̂Ƃ�, �g��ꂽ���_�K���� $\forall$-E �ł���Ƃ���, ���_�K����
\[ \infer {[t/x]\alpha}{ \forall x \alpha} \]
�Ƃ������.
\end{enumerate}
\end{definition}

���_�K�� $\supset$-E,
����� $\forall$-E ��{\bf �����K��\index{���傤���傫����@�����K��}
(elimination rule)}�ł���. �܂�, ���_�K�� $\supset$-I �� $\forall$-I ��
{\bf �����K��\index{�ǂ��ɂイ������@�����K��}(introduction rule)}�ł���.
���_�K�� $\supset$-E �̓�̑O�� $\alpha \supset  \beta$ �� $\alpha$ �ɂ��Ă�,
$\alpha \supset  \beta$ ��{\bf ��O��\index{���ズ��Ă�@��O��}(major premiss)}
�Ƃ�΂�, $\alpha$ ��{\bf ���O��\index{�ӂ�����Ă�@���O��}(minor premiss)}��
��΂��. �܂�, �O�񂪈�����Ȃ����_�K���ɂ��Ă����̑O�����O��Ƃ���
���Ƃɂ���.

�S�Ẳ��肪�����Ă��� NJ �̐��_�}�� NJ ��{\bf �ؖ��}}
\index{���傤�߂���@�ؖ��}}�Ƃ���.
�_���� $ \alpha$ �Ɏ���ؖ��}�����݂���Ƃ�, $ \alpha$ ��
{\bf �ؖ��\\index{���傤�߂����̂�@�ؖ��\}(provable)} �ł���, �Ƃ���.

���ώ�`�_���̑̌n NJ\_ �� NJ ���ア�ő̌n �ł���.
�̌n NJ\_ �̐��_�K���� $\forall$-I �ȊO�� LJ �Ƃ܂����������ł���.\\
�̌n NJ\_ ��$\forall$-I �K��:
%\bigskip
���_�} $\Pi$ �̈�ԉ��Ɍ���鎮�� $ \alpha$ �ł����
       ����. �܂�, $\Pi$ �̗����Ă��Ȃ�����ɂ͕ϐ� $x$ �͎��R�Ɍ����
       �����̂Ƃ���. ���̂Ƃ����̐}�`�͐��_�}�ł���:

\[
\infer{ \forall x \alpha}{\Pi}.
\]
���̂Ƃ�, �g��ꂽ���_�K���� $\forall$-I �ł���Ƃ���, ���_�K����
\[ \infer{ \forall x \alpha}{\alpha} \]
�Ƃ������.

$\Gamma$ ��_�����̗�Ƃ��܂�. �_���� $\alpha$ �Ɏ��� NJ (NJ\_) �̐��_�}������, ��
�̗����Ă��Ȃ����肪���ׂ� $\Gamma$ �Ɋ܂܂���Ƃ�,
\[ \Gamma \vdash_{NJ} \alpha \ \ \ \ (\Gamma \vdash_{NJ\_} \alpha)\]
�Ə���, NJ (NJ\_) �ŉ��� \ $\Gamma$ ���� $\alpha$ ���ł�Ƃ����܂�.
�܂�, ���̐��_�}�� $\Gamma$ ���� $\alpha$ �Ɏ��鐄�_�}�Ƃ����܂�. 
%
%\end{enumerate}
%\end{definition}
\section{4 �̑̌n LJ\_ , NJ\_ , LJ, NJ �̊֌W}
\subsection{LJ\_ �ɂ�����cut�����藝�� NJ\_ �ɂ����鐳�K���藝}
%\subsubsection{LJ\_ �ɂ�����cut�����藝}
\begin{theorem}
\rm{LJ\_} �ɂ�����, cut�����藝�͐������Ȃ�.
\end{theorem}
\begin{proof}
������ $\forall x(qz\supset qx),qz\rightarrow \forall zqz$ ��
LJ \_ �� cut �g���Ώؖ��ł��邪, cut �Ȃ��ł͏ؖ��ł��Ȃ�.

�܂� cut ���g���ďؖ��ł��邱�Ƃ�����.

\[
\infer{\forall x(qz \supset qx),qz \rightarrow \forall zqz }
{\infer{\forall x(qz \supset qx),qz \rightarrow \forall yqy} 
 {\infer{\forall x(qz \supset qx),qz \rightarrow qy }{\infer{qz \supset qy,  qz \rightarrow qy}
{qz \rightarrow qz &  qy \rightarrow qy}}}
& \infer{\forall yqy \rightarrow  \forall zqz}{\infer{\forall yqy \rightarrow qz}
{qz \rightarrow qz}}}
\]

cut �Ȃ��ł͏ؖ��ł��Ȃ����Ƃ�����. 

cut �Ȃ��ŏؖ��ł���Ƃ����,  $(e\rightarrow )$ �K���𖳎�����, $(w\rightarrow )$ �K���͉����������Ă��܂��̂�, 
�Ō�Ɏg���Ă���K���� $(\forall \rightarrow )$ �� $(c\rightarrow )$ �ł���.
% $\forall x(qz\supset qx),qz\rightarrow \forall zqz$ \\
%NJ �̏ؖ��}\\
%\[            \infer[(\forall i)]{\forall zqz} {\infer{qx}{\infer{qz\supset qx}{\forall x(qz\supset qx)}�@&qz}}
 %\]
%\bigskip
�䂦��, �Ō�̕����͈ȉ��̂悤�ɂȂ�:
 \[       \infer=[���񂩂�(\forall \rightarrow),(c\rightarrow  )]{qz,\forall x(qz\supset qx)\rightarrow \forall zqz }
        {qz,qz\supset qz,qz\supset qx,\forall x(qz \supset  qx)\rightarrow \forall zqz}.
 \]
���ꂪ cut �Ȃ��ŏؖ��ł��邽�߂ɂ�, �ȉ��̐������� cut �Ȃ��ŏؖ��ł��Ȃ���΂Ȃ�Ȃ�:
%bigskip
\[
      qz,qz\supset qz,qz \supset  qx\rightarrow \forall zqz.
\]
�Ƃ��낪, ���̐������� cut ���g���Ă� LJ\_ �ŏؖ��ł��Ȃ�.

%���ɐ����� $\forall x(qz\supset qx),qz\rightarrow \forall zqz$ ��
%LJ\_ �� cut ���g����,�ؖ��ł��邱�Ƃ�����.
%���̗�ł�NJ�ŏؖ��ł��邪, $LJ\_cut$�Ȃ��ŏؖ��ł��Ȃ�.
\end{proof}
%
���R��㈑̌n NJ\_ �ɂ��Ă͂܂��������l�� $\forall x(qz\supset qx),qz\vdash_{NJ\_}\forall zqz$
���������K�ȏؖ��}���Ȃ��̂�, NJ\_ �ɂ����鐳�K���藝�������Ȃ�.
%\subsubsection{NJ\_ �ɂ����鐳�K���藝}

%\begin{definition}
%$\Gamma \vdash \gamma $�Ɏ���NJ\_ ���_�}�����݂����,
%$\Gamma$ �ɂ���_������$\alpha$ �ϊ����ē�����_������$\Gamma ^*$
%��$\gamma $��$\alpha$ �ϊ����ē�����_����$\gamma  ^*$�����݂���,
%$\Gamma ^*\vdash\gamma  ^* $���������K�Ȑ��_�}�����݂���.
%\end{definition}
%\begin{theorem}
%\rm{NJ\_} �ɂ�����,���K���藝�͐������Ȃ�.
%\end{theorem}
\subsection{4 �̑̌n�̊֌W�̌���}
 %$\diamond LJ\Rightarrow NJ$\\
\vspace{5mm}
\begin{theorem}
$\Gamma \rightarrow \gamma$ ��LJ��cut�Ȃ��ŏؖ��ł���Ȃ��,
$\Gamma \vdash_{NJ}  \gamma$���������K�ȏؖ��}������.
%$\vdash_{\rm{LJ\_}}\Gamma \Longrightarrow  \gamma  \longrightarrow \Gamma \vdash_{NJ}  \gamma $\\
\end{theorem}
%\vspace{5mm}
\begin{proof}
%{\bf �ؖ� :}
\ \ \ \ LJ �� cut �Ȃ��̏ؖ��}�̒����Ɋւ���A�[�@�Ŏ���.\\
%\vspace{5mm}
{\bf 1.}\ \ �����̂Ƃ�
%      $\alpha \rightarrow \alpha$
     �͖��炩�ł���.\\
%\vspace{5mm}
{\bf 2.}\ \ ��ԍŌ�Ɏg��ꂽ�K�����\���Ɋւ���K���̂Ƃ��͖��炩�ł���.\\
{\bf 3.}\ \ ��ԍŌ�Ɏg��ꂽ�K���� $(\supset\rightarrow)$ �̂Ƃ��͏ؖ��}�̍Ō�̕�����
�ȉ��̂悤�ɂȂ��Ă���:
%\begin{center}
\[\infer
       {\alpha \supset  \beta, \Gamma, \Delta \rightarrow \gamma}
       {\Gamma \rightarrow \alpha &
       \beta, \Delta \rightarrow \gamma}.
\]
%\end{center}
�A�[�@�̉���ɂ��
$\Gamma \vdash_{NJ}\alpha$\ \ ��\ \ $\beta ,\Delta \vdash _{NJ}\gamma$
������ NJ �̐��K�ȏؖ��} $\Pi_1$\ \ �� \ \ $\Pi_2$ �Ƃ����݂���.
���̐��K�Ȑ��_�}�� $\alpha\supset\beta,\Gamma,\Delta\vdash_{NJ}\gamma$ �������Ă���:
\[
\infer{\deduce{\deduce{\gamma }{\Pi _2'}}
{\beta}}{\alpha\to\beta & \deduce{\alpha}{\Pi_1}},
\]
������ $\Pi _2'$ �� $\Pi _1$ �� $\Pi _2$ �Ɍ���Ȃ��ϐ���, $\Pi _2$ �� eigenvariable ��u������
�ē����鐄�_�}�ł���.\\
%\vspace{5mm}
{\bf 4.}\ \ ��ԍŌ�Ɏg��ꂽ�K���� $(\rightarrow\supset)$ �̂Ƃ���
�ȒP�Ȃ̂ŏȗ�����.\\
%\vspace{5mm}
%\begin{flushleft}
{\bf 5.}\ \ ��ԍŌ�Ɏg��ꂽ�K���� $(\forall\rightarrow)$ �̂Ƃ��͏ؖ��}�̍Ō�̕�����
�ȉ��̂悤�ɂȂ��Ă���:
%\end{flushleft}
%\begin{center}
\[\infer[(\forall \rightarrow)]
               {\forall x \alpha, \Gamma \rightarrow \gamma}
               {[t/x]\alpha, \Gamma \rightarrow \gamma}.
\]
%\end{center}
�A�[�@�̉���ɂ��
$[t/x]\alpha, \Gamma\vdash_{NJ}\gamma$
������ NJ �̐��K�ȏؖ��} $\Pi$ �����݂���.
���̐��K�Ȑ��_�}�� $\forall x\alpha,\Gamma\vdash_{NJ}\gamma$ �������Ă���:
%\begin{center}
\[\deduce{\gamma }{\deduce{\Pi}{\infer{[t/x]\alpha}{\forall x\alpha}}}.
\]
%\end{center}
%\begin{flushleft}
{\bf 6.}\ \ ��ԍŌ�Ɏg��ꂽ�K���� $(\rightarrow\forall)$ �̂Ƃ��͏ؖ��}�̍Ō�̕�����
�ȉ��̂悤�ɂȂ��Ă���:
%\end{flushleft}
%\begin{center}
\[\infer[(\rightarrow \forall)]
               {\Gamma \rightarrow \forall x \alpha}
               {\Gamma \rightarrow [y/x]\alpha}.
\]
%\end{center}
�A�[�@�̉���ɂ��
%\vspace{5mm}
$\Gamma\vdash_{NJ} [y/x]\alpha$ ���������K�Ȑ��_�} $\Pi$ �����݂���.
%\vspace{5mm}
���̐��K�Ȑ��_�}�� $\Gamma\vdash_{NJ}\forall x\alpha$ �������Ă���:
\[\deduce{\infer{\forall x\alpha}{[y/x]\alpha}}{\Pi}.
\]
\end{proof}
%
%\begin{flushleft}$\diamond NJ\Rightarrow LJ$\\
\begin{theorem}
$\Gamma \vdash_{NJ}  \gamma$ ������ \rm{NJ} �̐��K�ȏؖ��}�������,
 $\Gamma \rightarrow \gamma$������ LJ �� cut �Ȃ��̏ؖ��}������.
%$\Gamma \vdash_{NJ}  \gamma  \Longrightarrow \vdash_{LJ}\Gamma \rightarrow \gamma $\\
\end{theorem}
\begin{proof}
\rm{NJ} �̐��K�Ȑ��_�}�̒����Ɋւ���A�[�@�ŏؖ�����.
%\end{flushleft}

{\bf 1.      } ���_�}�̒����� 1 �̂Ƃ�.       \ \ ���_�}�͎��̌`�����Ă���:
\[
 \deduce{\gamma}{k}
\]
���ꂪ $\Gamma \vdash_{NJ} \gamma$ �������Ă��邱�Ƃ��,
 $\gamma$ �� $\Gamma$ �Ɋ܂܂�Ă���.
�����,   ���� $\gamma \ra \gamma$ ����o�����Đ��_�K�� $(w \ra)$ �� $(e \ra)$ ��
�g����,   $\Gamma \ra \gamma$ �� LJ �� cut �Ȃ��ŏؖ��ł���,

{\bf 2.      } ���_�}�̒����� 1 ����̂Ƃ��� 3�̏ꍇ�ɕ������.      

{\bf 2.1.      } �Ō�Ɏg��ꂽ���_�K���� $\supset$-I �̂Ƃ�.       \ \ ���_�}�͎��̌`����
�Ă��� ($\gamma \equiv \alpha \supset  \beta$ �ł���):
\[
\infer[k]{\alpha \supset  \beta}
       {\deduce{\beta}{\deduce{\Pi}{
 \deduce{\alpha}{k}
}}}.
\]
���_�}
\[
\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}
}}
\]
�ɂ��ċA�[�@�̉��肪�g����,   $\alpha,   \Gamma \ra \beta$ �� cut �Ȃ���
LJ �ŏؖ��ł���.       �����,   LJ �̐��_�K�� $(\ra \supset )$ �ɂ��
 $\Gamma \ra \alpha \supset  \beta$ �� LJ �� cut �Ȃ��ŏؖ��ł���.      

{\bf 2.2.      } �Ō�Ɏg��ꂽ���_�K���� $\forall$-I �̂Ƃ�.       \ \ \ \ ���_�}�͎��̌`��
���Ă���:
%9
\[
\infer{ \forall x\alpha}
    {\deduce{[y/x] \alpha}{\Pi}}.
\]
�A�[�@�̉�����g����,   ������ $\Gamma \ra [y/x]\alpha$ �� \rm{LJ} �� cut �Ȃ��ŏؖ���
����.       �����,   LJ �̐��_�K�� $(\ra \forall)$ �ɂ��,   ������ $\Gamma \ra
 \forall x \alpha$ �� LJ �� cut �Ȃ��ŏؖ��ł���.      

{\bf 2.3.      } �Ō�Ɏg��ꂽ���_�K���������K���̂Ƃ�.       \ \ \ \ ���_�}�̌��_ $\gamma$
���獶�ɒH���čs���Ĉ�ԍ��ɂ����[�̘_�����ɂ܂ŒB����
�o�H��{\bf ��o�H\index{���ク����@��o�H}(main branch)}�Ƃ���.
% ��o�H�Ɍ����_�����i�̏o��)�͐��_�K�� $\to$-E �̕��O��ɂ͂Ȃ��Ă��܂���.
���_�}�����K�ł��邱�ƂƍŌ�Ɏg��ꂽ���_�K���������K���ł��邱�Ƃ���,   ��o�H�Ɍ����
�_�����i�̏o��)�͓����K���̌��_�ɂ͂Ȃ��Ă��Ȃ�.       �Ȃ��Ȃ��,   �������̂悤��
�_�����i�̏o��)���������Ȃ��,   ���̒��ōł����ɂ�����̂��ɑ�_������
�Ȃ��Ă��܂�����ł���.       �����Ő��_�}�̍ł������̏�[���ɒ��ڂ����,
���_�}�͎��� 2 �̂ǂꂩ�̌`�����Ă���:
% 3
% 4
% 5
\[
%\hfil
\deduce{\Pi}{\infer{\beta}{\deduce{\alpha\to\beta}{k} &
                                 \deduce{\alpha}{\Pi_1}}},
\hspace{25mm}
%\infer*{}{\infer{\beta}{\deduce{\bot}{k}}},
%********* 5 ************************************
\deduce{\Pi}{\infer{ [t/z]\alpha}{\deduce{\forall z \alpha}{k}}}.
%\hfil
\]
% �ǂ̏ꍇ�� $l$ �͐��_�} $\Pi$ �̈�ԍ����̏�[�ɂ�������鐔����,
%���̉��ɂ͘_���� $\beta$ �� $[t/x]\alpha$ ������܂�.
������,   ���� $k$ �̉��̉���͗����Ă��Ȃ�.     

1�Ԗڂ̏ꍇ��,   ���_�} $\Pi_1$ �̗����Ă��Ȃ��������ׂ����̂� $\Delta$
 �Ƃ��A�[�@�̉����K�p�����,   ������
 $\Delta \ra \alpha$ �� LJ �� cut �Ȃ��ŏؖ��ł���.       ���_�} $\Pi$ ��
 $\beta$ �ȊO�̗����Ă��Ȃ��������ׂ����̂� $\Sigma$ �Ƃ�
�A�[�@�̉����K�p�����,   ������ $\beta,   \Sigma \ra \gamma$ �� LJ �� cut
 �Ȃ��ŏؖ��ł���.       ������,   �� $\Delta$ �� $\Sigma$ �Ɍ����_�����͑S��
�� $\Gamma$ �Ɍ���Ă���.       �����,   LJ �̐��_�K�� $(\supset  \ra)$ �ɂ��
 $\alpha \supset  \beta,   \Delta,   \Sigma \ra \gamma$ �� LJ �� cut �Ȃ��ŏؖ�
�ł���.       �_���� $\alpha \supset  \beta$ �͗� $\Gamma$ �Ɋ܂܂�邩��,
LJ �̐��_�K�� $(e \ra)$,   $(c \ra)$,   $(w \ra)$ �����񂩎g���ΐ�����
 $\Gamma \ra \gamma$ �� LJ �� cut �Ȃ��ŏؖ��ł��邱�Ƃ�������.      
%\vspace{5mm}

2�Ԗڂ̏ꍇ��,   ���_�} $\Pi$ �ɋA�[�@�̉����K�p�����,   ����
�� $[t/x]\alpha,   \Delta \ra \gamma$ �� LJ �� cut
 �Ȃ��ŏؖ��ł���.       ������,   �� $\Delta$ �Ɍ����_�����͑S��
�� $\Gamma$ �Ɍ���Ă���.       �����,   LJ �̐��_�K�� $(\forall \ra)$ �ɂ��
 $\forall x \alpha,   \Delta \ra \gamma$ �� LJ �� cut �Ȃ��ŏؖ�
�ł���.       �_���� $\forall x \alpha$ �͗� $\Gamma$ �Ɋ܂܂�܂�����,
LJ �̐��_�K�� $(e \ra)$,   $(c \ra)$,   $(w \ra)$ �����񂩎g���ΐ�����
 $\Gamma \ra \gamma$ �� LJ �� cut �Ȃ��ŏؖ��ł��邱�Ƃ�������.      

\end{proof}
%\begin{flushleft}
\begin{theorem}
$\Gamma \vdash_{\rm{NJ\_}}  \gamma $ ���������K�ȏؖ��}�������,
 $\Gamma \rightarrow \gamma $ �� \rm{LJ\_} �� cut �Ȃ��ŏؖ��ł���.
%$\Gamma \vdash_{NJ\_}  \gamma  \Longrightarrow \vdash_{LJ\_}\Gamma \rightarrow \gamma $\\
\end{theorem}
\begin{proof}
\ \ \ \ NJ\_ �̐��K�Ȑ��_�}�̒����Ɋւ���A�[�@�ŏؖ�����.      

�藝 3.3 �Ƃ܂����������Ȃ̂�,  �ȗ�����.
%\bigskip
\end{proof}
%\end{flushleft}
\begin{definition}\em
���������邢�͎��R��㈂̑̌n S, T �ɂ�����, �u �C�ӂ̘_�����̗� $\Gamma$ �ƔC�ӂ̘_���� $\gamma$ �ɑ΂���,
$\Gamma\vdash_S\gamma$ �Ȃ�� $\Gamma\vdash_T\gamma$ �v����������Ƃ�, T �� S ��苭���̌n�Ƃ�����,
$\rm{S}\leq \rm{T}$ �Ə���. �܂�, $\rm{S}\leq \rm{T}$ �ł��� $\rm{T}\leq \rm{S}$ �łȂ��Ƃ�
$\rm{S} < \rm{T}$ �Ə���.
\end{definition}
\begin{theorem}
�u$\Gamma \rightarrow \gamma$�@�Ɏ��� \rm{LJ\_} �� cut �Ȃ��̏ؖ��}�������,
$\Gamma\vdash_{NJ\_}\gamma$ ������ \rm{NJ\_} �̐��K�ȏؖ��}������v���������Ȃ�.     
\end{theorem}
\begin{proof}
������ $qx\supset r,  qx,  \forall x(r\supset px)\rightarrow \forall xpx$��
LJ\_ �� cut �Ȃ��ŏؖ��ł���.

LJ\_ �̏ؖ��}
\[
\infer{qx\supset r,  qx,  \forall x(r\supset px)\rightarrow \forall xpx}
       {qx\rightarrow qx
        &
      \infer{r,  \forall x(r\supset px)\rightarrow \forall xpx}
            {\infer={r,  \forall x(r\supset px)\rightarrow px}{\infer{r\supset px,  r\rightarrow px}
      {r\rightarrow r &  px\rightarrow px}}
           }}
\]
%NJ\_ �̏ؖ��}\\
%\[            \infer[(\forall i)]{\forall xpx} {\infer{px}{\infer{r\supset px}{\forall x(r\supset px)} & \infer{r}{qx\supset r�@qx}}}
%\]
$qx\supset r,  qx,  \forall x(r\supset px)\rightarrow \forall xpx$ ���������K�ȏؖ��}�̒���
���o�ė���_�����͗������Ă��Ȃ�����̕����_���������_�̕����_�����ł���.
$qx\supset r,  qx,  \forall x(r\supset px)\rightarrow \forall xpx$ ���������K�ȏؖ��}�̍Ō�
�Ɏg���Ă���K���� 4 �����Ȃ�,  ������ $\supset$ �̓����K���ł͂��蓾�Ȃ��̂�,
�\���Ƃ��Ă͎c��� 3 �ł���.      $\forall$ �̓����K���łȂ����Ƃ�������.      ������,  �\����
����̂�,  $\supset$ �̏����� $\forall$ �̏����ł���.

\[  \infer{\forall xpx}{\forall z\forall xpx}�@�@�@�Ɓ@\infer{\forall xpx}{\alpha \supset \forall xpx�@\alpha}
\]   �������肦�Ȃ�.    

$\forall z\forall xpx$ �� $\alpha \supset \forall xpx$ �͕����_�����ł͂Ȃ��̂�,   ���̗��NJ\_�Ő��K�ȏؖ��}���Ȃ�.
\end{proof}

LJ, NJ, LJ\_, NJ\_ �͏ؖ��\�͂Ƃ����_�ł͓����ł���. ������, Section 3 �ŏq�ׂ��悤�� LJ\_ �� NJ\_
�ł� cut �����藝�␳�K���藝�����藧���Ă��Ȃ�. ������, ������ 4 �̑̌n�� cut �Ȃ��̑̌n,
���K�Ȑ��_�}�݂̂�F�߂�̌n�Ŕ�r���Ă݂邱�Ƃɂ���B�Ȍ�� LJ �� LJ\_ �� cut �Ȃ��̑̌n, NJ �� NJ\_ ��
���K�Ȑ��_�}�݂̂𐄘_�}�Ƃ��ĔF�߂�̌n�Ƃ���. ���̂Ƃ�, �藝3.4 �� �藝3.6 �� $\rm{NJ\_} < \rm{LJ\_}$ ������
�Ă���.

\begin{theorem}
�u$\Gamma\vdash_{NJ}\gamma$ ������ \rm{NJ} �̐��K�ȏؖ��}�������,
$\Gamma \rightarrow \gamma$ �Ɏ��� \rm{LJ\_} �� cut �Ȃ��̏ؖ��}������v���������Ȃ�.      \\
\end{theorem}
\begin{proof}
������ $\forall x(qz\supset qx),  qz \vdash _{\rm{NJ}} \forall zqz$ ���������K�ȏؖ��}
���ȉ��ł���.

\[\infer[(\forall i)]{\forall zqz} {\infer{qx}{\infer{qz\supset qx}{\forall x(qz\supset qx)}�@&qz}}
 \]

������ $\forall x(qz\supset qx),  qz\rightarrow \forall zqz$ ��
LJ\_ �� cut �g���Ώؖ��ł��邪,  cut �Ȃ��ł͏ؖ��ł��Ȃ�.

�܂� cut ���g���Ώؖ��ł��邱�Ƃ�����. 

cut �t�̏ؖ��}�͈ȉ��ł���:
\[
\infer{ \forall x(qz \supset qx),qz \rightarrow \forall zqz}
{\infer{\forall x(qz \supset qx),qz \rightarrow \forall yqy} 
 {\infer{\forall x(qz \supset qx),qz \rightarrow qy }{\infer{qz \supset qy,  qz \rightarrow qy}
{qz \rightarrow qz &  qy \rightarrow qy}}}
& \infer{\forall yqy \rightarrow  \forall zqz}{\infer{\forall yqy \rightarrow qz}
{qz \rightarrow qz}}}
\]

cut �Ȃ��ł͏ؖ��ł��Ȃ����Ƃ�����. cut �Ȃ��ŏؖ��ł���Ƃ����,
�Ō�Ɏg���Ă���K���� $(\forall \rightarrow )$ �� $(c\rightarrow )$ �ł���.
% $\forall x(qz\supset qx),  qz\rightarrow \forall zqz$ \\
%NJ �̏ؖ��}\\
%\[\infer[(\forall i)]{\forall zqz} {\infer{qx}{\infer{qz\supset qx}{\forall x(qz\supset qx)}�@&qz}}
 %\]
%\bigskip
�䂦��,   �Ō�̕����͈ȉ��̂悤�ɂȂ�:
 \[\infer=[���񂩂�(\forall \rightarrow),  (c\rightarrow  )]{qz,  \forall x(qz\supset qx)\rightarrow \forall zqz }
       {qz,  qz\supset qz,  qz\supset qx,  \forall x(qz \supset  qx)\rightarrow \forall zqz}.
 \]
���ꂪ cut �Ȃ��ŏؖ��ł��邽�߂ɂ�,   �ȉ��̐������� cut �Ȃ��ŏؖ��ł��Ȃ���΂Ȃ�Ȃ�:
%bigskip
\[
     qz,  qz\supset qz,  qz \supset  qx\rightarrow \forall zqz.
\]
�Ƃ��낪,   ���̐������� cut ���g���Ă� LJ\_ �ŏؖ��ł��Ȃ�,

���̗�ł� NJ �Ő��K�ȏؖ��}�����邪,   LJ\_ cut �Ȃ��ŏؖ��ł��Ȃ�.
\end{proof}

�藝3.2 �� �藝3.7 �� $\rm{LJ}\_ < \rm{NJ}$ �������Ă���.
���ǂ��̎l�̑̌n�̊֌W�� $\rm{NJ}\_ < \rm{LJ}\_ < \rm{NJ} = \rm{LJ}$ �ɂȂ��Ă���.    
%
\section{$\forall$ �����K���Ɋւ���ؖ��̎���}
%
���� Section �̕⏕�藝4.3 �͔��Ⴊ�������Ă���̂ŕ⏕�藝�ł͂Ȃ�.
�ؖ����r���ōs���l���Ă���. ���̕⏕�藝���ǂ����ؖ����悤�Ƃ��ĐF�X�Ȕ��Ⴊ��������
�̂�, �s���l�����ؖ��ł��邪�������߂Ă���.
%
\begin{definition}[�ϐ��̕ϐ��ւ̑��]\ \em
\begin{flushleft}
$[y/x]\forall z\alpha$  �̒�`�͈ȉ��Ƃ���.
\end{flushleft}
\begin{enumerate}
 \item $[y/x] \forall z\alpha  \equiv  \forall z \alpha$ \ \ (if $x\not\in FV(\forall z\alpha))$,
 \item $[y/x]\forall z\alpha  \equiv \forall z[y/x]\alpha$\ \ (if $z\not\equiv y)$,
 \item $[y/x]\forall z\alpha  \equiv \forall x[x/u][y/x][u/y]\alpha$\ \ 
    ($u$ �� $V(\alpha )\cup \{x, y\}$ �̌��łȂ��ŏ��̕ϐ�).
\end{enumerate}
���̑���̒�`�͏ォ�珇�ɓK�p����.      
\end{definition}
\begin{definition}
������$\Gamma \rightarrow \Delta $ �̒���$n$ �� \rm{LJ\_} �̏ؖ��}�����݂���Ƃ�$
\Gamma \stackrel{n}  \vdash_{\rm{LJ\_}} \Delta$ �Ə���.
\end{definition}
%
\begin{lemma}\em \
$\Gamma  \stackrel{n}\vdash_{ \rm{LJ\_}} \Delta  \Rightarrow[y/x]\Gamma  \stackrel{n} \vdash_{\rm{LJ\_}} [y/x]\Delta$
\end{lemma}
\begin{proof}
{\bf �ؖ� :}\ \ \ \ n�@�Ɋւ���A�[�@�Ŏ���.     

{\bf I }�����̂Ƃ�

$\alpha \rightarrow\alpha�@�@ [y/x]\alpha\rightarrow[y/x]\alpha�@�@$  �������Ȃ̂�,   ���Ȃ�.       

{\bf II} �Ō�Ɏg��ꂽ�K���� $(w\rightarrow )$ �̂Ƃ�

\[\begin{array}{cc}
\infer[(w \rightarrow)]
              {\alpha,   \Gamma \rightarrow \Theta}
              {\Gamma \rightarrow \Theta}&\\
\end{array}\]
�A�[�@�̉�����

\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\Theta \]
%\end{array}\]
$(w\rightarrow )$�K����K�p����
\[\begin{array}{cc}
\stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\alpha ,  [y/x]\Gamma \rightarrow [y/x]\Theta 
\end{array}\]
{\bf III} �Ō�Ɏg��ꂽ�K����$(\rightarrow w)$�̂Ƃ�
\[\begin{array}{cc}
\infer[(\rightarrow w)]
              {\Gamma \rightarrow \Theta,   \alpha}
              {\Gamma \rightarrow \Theta}

\end{array}
\]
\[ (w\rightarrow )  �̏ꍇ�Ɠ��l.      \]
{\bf IV}�Ō�Ɏg��ꂽ�K���� $(\supset \rightarrow )$ �̂Ƃ�

\[\begin{array}{cc}
\infer[(\supset  \rightarrow)]
              {\alpha \supset  \beta,   \Gamma,   \Delta \rightarrow  \Lambda}
              {\Gamma \rightarrow  \alpha &
              \beta,   \Delta \rightarrow \Lambda}
\end{array}\]
�A�[�@�̉�����
\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\alpha\]
\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\beta ,   [y/x]\Delta  \rightarrow [y/x]\Lambda\]
$(\supset \rightarrow )$ �K����K�p���� 

\[\stackrel{n} \vdash_{\rm{LJ\_}} [y/x]\alpha \supset[y/x] \beta ,  [y/x]\Gamma,    [y/x]\Delta  \rightarrow [y/x]\Lambda\]
\[[y/x](\alpha \supset \beta)\equiv[y/x]\alpha \supset [y/x]\beta   ���\]
%\[\begin{array}{cc}
%\end{array}\]
\[\stackrel{n}\vdash_{\rm{LJ\_}} [y/x](\alpha \supset \beta ),  [y/x]\Gamma ,  [y/x]\Delta \rightarrow [y/x]\Lambda \]
%\begin{flushleft}
%\newpage
{\bf V} �Ō�Ɏg��ꂽ�K����$(\rightarrow \supset )$ �̂Ƃ�

\[\begin{array}{cc}
\infer[(\rightarrow \supset )]
              {\Gamma \rightarrow \alpha\supset \beta}
              {\alpha,   \Gamma \rightarrow \beta}

\end{array}\]
�A�[�@�̉�����

\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\beta \]
$(\rightarrow \supset )$ �K����K�p����
\[\stackrel{n}  \vdash_{\rm{LJ\_}}  [y/x]\Gamma   \rightarrow [y/x]\alpha \supset [y/x]\beta\]
\[ [y/x] (\alpha \supset \beta)\equiv[y/x]\alpha \supset [y/x]\beta   ��� \]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}}  [y/x]\Gamma   \rightarrow [y/x](\alpha \supset \beta) \]
{\bf VI} �Ō�Ɏg��ꂽ�K����$(\forall \rightarrow  )$ �̂Ƃ�

%\end{flushleft}
\[\begin{array}{cc}
\
      \infer[(\forall \rightarrow)]
              {\forall z \alpha,   \Gamma \rightarrow \Theta}
              {[s/z]\alpha,   \Gamma \rightarrow \Theta}
\end{array}\]
%\begin{flushleft}
$    $�A�[�@�̉�����
%\begin{center}
 \[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x][s/z]\alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
{\bf (1)}$  z\not\equiv  y $�̂Ƃ� 

{\bf (1.      1)} $z\not\equiv x $ �̂Ƃ� 

\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x][s/z]\alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta  ���� \]
$(\forall \rightarrow )$ �K����K�p����
�@\[\stackrel{n}  \vdash_{\rm{LJ\_}}\forall z [y/x]\alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
$y\not\equiv z$ ���@�@�@\[\forall z[y/x]\alpha \equiv [y/x]\forall z\alpha \]
\[\stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\forall z \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
{\bf (1.      2)}$z\equiv x$ �̂Ƃ� 

\[ [y/x][s/z]\alpha \equiv [[y/z]s/z]\alpha \]
 \[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [[y/z]s/z] \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
$(\forall \rightarrow )$ �K����K�p���ā@
\[ \stackrel{n}  \vdash_{\rm{LJ\_}}\forall z \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
%\vspace{5mm}
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\forall z \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta \]
%\end{center}
%\vspace{5mm}
{\bf (2)}$ z \equiv  y�̂Ƃ�$

\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [z/x][s/z] \alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta \]
{\bf (2.      1)}$z \equiv x�̂Ƃ�$ 

\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [[z/x]s/z] \alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta \]
$(\forall \rightarrow ) $�K����K�p����
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} \forall z \alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta \]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\forall z \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta  \]
{\bf (2.      2)}$z \not \equiv x$ �̂Ƃ� 

\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}}  [[z/x]s/z][z/x] \alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta \]
$x\not\in FV(\forall z\alpha ) $���   

\[ [z/x]\alpha \equiv \alpha \]
\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [[z/x]s/z]\alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta  \]
$(\forall \rightarrow )$ �K����K�p���ā@

\[ \stackrel{n}  \vdash_{\rm{LJ\_}} \forall z \alpha  ,   [z/x]\Gamma   \rightarrow [z/x]\Theta \]
$x\not\in FV(\forall z\alpha )$ ���

 \[[y/x]\forall z\alpha \equiv \forall z\alpha \]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\forall z \alpha  ,   [y/x]\Gamma   \rightarrow [y/x]\Theta  \]
{\bf VII} �Ō�Ɏg��ꂽ�K����$(\rightarrow \forall  )$ �̂Ƃ�

\[\begin{array}{cc}
\infer[(\rightarrow \forall)]
              {\Gamma \rightarrow \forall z \alpha}
              {\Gamma \rightarrow [y/z] \alpha}
      \end{array}\]
���_�K��{$(\rightarrow  \forall)$}  �ɂ����Ă�,    �ϐ� $y$ ��
$y\not\in FV(\Gamma) \cup  FV(\forall x\alpha )$ ,  �𖞂����Ă��Ȃ���΂Ȃ�Ȃ�.   

{\bf (1)}$ x\not\in FV(\forall z\alpha )�̂Ƃ�$

\[ [y/x]\forall z\alpha \equiv \forall z\alpha \]
{\bf (1.      1)}$ x\equiv z �̂Ƃ�$

x��$\Gamma$ �Ɍ���Ȃ��̂�
\[ [y/x]\Gamma  \equiv \Gamma�@\]
\[[y/x]\forall z\alpha\equiv \forall z\alpha �@\]
\[ [y/x]\Gamma \rightarrow [y/x]\forall z\alpha \equiv \Gamma \rightarrow \forall z\alpha \]
 \[ �Ȃ̂�,   [y/x]\Gamma \rightarrow [y/x]\forall z\alpha  �͏ؖ��ł���.      \]
{\bf (1.      2)}$x\not\equiv z �̂Ƃ�$

�A�[�@�̉�����  
\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\alpha \]
$x\not\in FV(\alpha )$ ���       
     \[[y/x]\alpha \equiv \alpha \]
\[ \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow \alpha \]
{\bf (1.      2.      1)}$z\not\equiv y$ �̂Ƃ� 

\[ z\not\in FV([y/x]\Gamma ) ���� (\rightarrow \forall ) ��K�p���� \]
\[\stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow  \forall z\alpha \]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\forall z\alpha \]
{\bf (1.      2.      2)}$z\equiv y$ �̂Ƃ� 

\[ �ؖ��͂ł��Ȃ�����. \]
{\bf (2)}$ z\not\equiv y �̂Ƃ�$

 \[[y/x]\forall z\alpha \equiv \forall z[y/x]\alpha \]
�A�[�@�̉�����         

 \[  \stackrel{n-1}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\alpha \]
$z\not\in FV([y/x]\Gamma ) $���� $(\rightarrow \forall )$ ��K�p���ā@ 

 \[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow \forall z[y/x]\alpha\]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow [y/x]\forall z\alpha \]
{\bf (3)}$ ����ȊO�̂Ƃ�$
\[ [y/x]\forall z\alpha \equiv \forall x[x/u][z/x][u/z]\alpha �@�@ (u�� V(\alpha )\cup {x,  y} �̌��o�Ȃ��ŏ��̕ϐ�) \]
$v��\Gamma ,   \alpha$ �Ɍ���Ȃ��ϐ��Ƃ���.      

�A�[�@�̉�����                

\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [x/v][z/x][v/z]\Gamma \rightarrow [x/v][z/x][v/z]\alpha \]
$z\not\in FV(\Gamma )$ ���� $[v/z]\Gamma \equiv \Gamma$ 

\[\stackrel{n-1}  \vdash_{\rm{LJ\_}} [x/v][z/x]\Gamma \rightarrow  [x/v][z/x][v/z]\alpha �ƂȂ�, \]
$[x/v][z/x]\Gamma \equiv[z/x]\Gamma $  ���g����,  

\[p\stackrel{n-1}  \vdash_{\rm{LJ\_}} [z/x]\Gamma \rightarrow  [x/v][z/x][v/z]\alpha \]
$x\not\in FV([z/x]\Gamma )$ �̂�,  $ (\rightarrow \forall )$ ��K�p���ā@ 

\[\stackrel{n}  \vdash_{\rm{LJ\_}} [z/x]\Gamma \rightarrow  \forall x[x/v][z/x][v/z]\alpha \]
\[ \stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow  \forall x[x/v][y/x][v/y]\alpha \]
$\forall x[x/v][y/x][v/y]\alpha \equiv \forall x[x/u][y/x][u/y]\alpha \equiv [y/x]\forall z\alpha$ �Ȃ̂�,   

\[\stackrel{n}  \vdash_{\rm{LJ\_}} [y/x]\Gamma \rightarrow  [y/x]\forall z\alpha \]
\end{proof}
�⏕�藝4.      3�͒��ώ�`�q��_���̑̌n LJ\_ ��
$\Gamma \rightarrow  \gamma$  �� cut �Ȃ��ŏؖ��\�Ȃ��, $[y/x]\Gamma \rightarrow
[y/x]\gamma$ ���̌n LJ\_ �� cut �Ȃ��ŏؖ��\�ł���Ƃ������Ƃ��ؖ����悤�Ǝ��݂�.������, ����͏ؖ�
�ł���, ���Ⴊ��������.���̔���͑���̒�`�Ɉˑ����Ȃ����̂ɂȂ��Ă���.  ������, ���̂悤�ȑ���Ɋւ��
�藝�ɂ��Ă�, ����̒�`�Ɉˑ����Đ��藧���Ă����肢�Ȃ������肷��\��������.
���̔����, ��������܂���`����Ώؖ��ł���ƍl���Ă��낢��Ȓ�`�ŏؖ������݂����ʌ�������
���̂ł���.
\newpage
\section{�ӎ�}

�{�_���̍쐬�ɂ�����,   �w�������̌ÐX�Y��搶,   �R�c�b�C����ɑ����
�����͂𒸂��܂������Ƃ�S���犴�ӂ������܂�.
\newpage
\nocite{matumoto3} \nocite{Komori07-4} \nocite{Gentzen} \nocite{Szabo} \nocite{Prawitz}
\bibliography{logic}
\bibliographystyle{jplain}
\end{document}
