\documentclass[a4j]{jarticle}
%\documentclass{jsarticle}
\usepackage{latexsym,amssymb,amsthm,proof}
\pagestyle{plain}
\renewcommand{\to}{\supset}
\newcommand{\mb}[1]{\mathbf{\mathsf{#1}}}
\newtheorem{df}{��`}[section]
\newtheorem{thm}[df]{�藝}
\newtheorem{cor}[df]{�n}
\newtheorem{prop}[df]{����}
\newtheorem{lem}[df]{���}
\newtheorem{exa}[df]{��}
\title{�ϐ�����ʂ��Ȃ��Ƃ��̎��R��㈑̌n NJ �̐��K�`�藝}       
\author{�ÐX�Y��(��t��w)}
%\date{}
\begin{document}
\maketitle
%% �ڎ�
\tableofcontents

\newpage

\section{���}

�{���_�� 2010 �N 3 ���C�������R�c�b�C�N�̏C�m�_������������(�ԈႢ�̏C�����s����),
��苭�����ʂ��ؖ��������̂ł���B�܂�, �ǂ݂₷�����邽�߂ɒ�`�Ȃǂɂ��ύX���Ă�
��B

Gentzen �� LJ, LK �̊�{�藝�� Prawitz �� NJ, NK �̐��K���藝���ؖ�����Ă����
�n�ł́C�_�����̒�`�͎��R�ϐ��Ƒ����ϐ�����ʂ���Ă���B���R�ϐ��Ƒ���
�ϐ�����ʂ��Ȃ��̌n�ł���{�藝�␳�K���藝����������Ƃ�����Ă��鏑��������B
$\alpha$ ���l�Ș_�����𓯈ꎋ����Εϐ��̋�ʂ����Ȃ��Ă���{�藝�␳�K���藝��
���藧���Ƃ�, ��ʂ����̌n�ł̏ؖ��Ɠ��l�ɏؖ��ł���B���������ꎋ���Ȃ���
���l�ȏؖ��͂��܂��s���Ȃ��B���R�ϐ��Ƒ����ϐ�����ʂ��� $\alpha$ ���l�Ș_������
���ꎋ���Ȃ��̌n�ł�, ��{�藝�␳�K���藝���u�^����ꂽ���_�}�� cut �����̐��_
�}�␳�K�`�̐��_�}�ɕό`�ł���v�Ƃ���Ɛ������Ă��Ȃ��B������
���u�^����ꂽ�_������ cut �����̐��_�}�␳�K�`�̐��_�}����
�݂���v�Ƃ���Ƃ����ア��{�藝�␳�K�`�藝�͐������Ă���B

�����ł� NJ �̐��K�`�藝���ؖ�����B�������̏������ԈႢ��Ƃ���
������Ȃ̂�, �T�d�ɏؖ����s���K�v������B���_�}�̕ό`���Ȃ�ׂ������ɒ�`��
�邽�߂�, �^�t�����_���𐄘_�}�Ƃ݂Ȃ����Ƃɂ���B�܂�, ��ʂ̌^�t�����_���ɂ�
���Ă͕ό`�����܂���`�ł��Ȃ��B���̂��߁C�܂��͋����^�t�����_�����`���C����
�����^�t�����_���ɂ��Ă̐��K���藝���ؖ�����B�����Ă��̌��ʂ��g���āC�ؖ���
����_�����ɂ��āC���K�ȏؖ��}������Ƃ������K�`�藝���ؖ�����B

�܂��_�����̒�`���s���B���̘_���ň������ώ�`�_���́C���m�ɂ͒��ώ�`�q��_
���� \{$\to, \bot, \forall \}$-�f�Ђł���B���̂��߁C�_���L���ɂ�$\vee, \wedge,
 \exists$ �͊܂܂�Ă��Ȃ��B

����, �[�^�t�����_�����`����B�[�^�t�����_���͌^���𖳎����č\�����ꂽ�^�t��
���_���̂悤�Ȃ��̂ł���B�[�^�t�����_���͌�Œ�`���鋷���^�t�����_����^�t����
�_�����܂񂾊T�O�ƂȂ��Ă���B

���̎��ɁC�����^�t�����_�����`��, ���� $\beta$-�ό`���`����B�����Đ��K���藝����
������B�ϐ����g�ɂ͎��R�ϐ��Ƒ����ϐ��̋�ʂ͂Ȃ��������^�t�����_���ł͎��R��
�ϐ��Ƒ����̕ϐ�����������Ă���B

�]���ł͖��炩���Ƃ��ďؖ���������Ă��鋷���^�t�����_���� $\beta$-�ό`�������ʂ�
�����^�t�����_���ɂȂ邱�Ƃ��ؖ�����B�܂� $\beta$-�ό`�ɂ��^���ω����Ȃ����Ƃ�
�����ɏؖ�����B���̂悤�Ȓi�K���o��, �����^�t�����_���ɂ��Ă̐��K���藝���ؖ�����B

���̋����^�t�����_���ɂ��Ă̐��K���藝�𗘗p���āC��ʂ̌^�t�����_���ɂ��Ă̐��K
�`�藝���ؖ�����B���̕��j�͈ȉ��̒ʂ�ł���D

�^�t�����_�� $M$ ���^����ꂽ���C$M$ �̌̕ϐ��̂����C���R�̕ϐ��Ƃ��Ă��C�����̕�
���Ƃ��Ă�����Ă���ϐ�������΁C��������Ă��镔���̂ݐV���ȕϐ��Œu�������Ăł���^�t
�����_���� $N$ �Ƃ���D���� $N$ �͋����^�t�����_���ɂȂ�̂ŁC���̐��K�` $N'$ �����܂�B
���� $N'$ ���� $M$ �̌��_($M$ �̌^)�Ɠ������_�������K�Ȑ��_�}(�^�t�����_��)�����߂�
�̂ł���B

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�_����}

��{�L���Ƃ��āC�̕ϐ��C�q��L���C�֐��L���C�_���L���C���̑��̋L����p�ӂ���B
\begin{itemize}
\item �̕ϐ�: \ ���Z�̕ϐ� `$u_{0}$', `$u_{1}$', `$u_{2}$',...
\item �q��L��: \ ���R��$n$�ɂ��āC$n$�ϐ��̏q��L��
\item �֐��L��: \ ���R��$n$�ɂ��āC$n$�ϐ��̏q��L��
\item �_���L��: \ `$\to$', `$\bot$', `$\forall$'
\item ���̑��̋L��: \ `$($', `$)$'
\end{itemize}

�̕ϐ���\�����^�ϐ��Ƃ��āC$u,v,w,a,b,c,...$���g�p��, �q��L����\�킷���^�ϐ�
�Ƃ��āC$p,q,r,...$���g�p��, �֐��L����\�킷���^�ϐ��Ƃ��āC$f,g,h,...$���g�p����B
%
\begin{df}[�̍�]\em \ �̍����ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item �̕ϐ� $u$ �͌̍��ł���,
\item $t_{1},...,t_{n}$ ���̍��ł���C$f$ �� $n$ �ϐ��̊֐��L���Ȃ�΁C$(ft_{1}...t_{n})$ �͌̍��ł���B
\end{enumerate}
\end{df}

\begin{df}[�_����]\em \ 
\label{sec: def_of_formula}
�_�������ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item �_���L�� $\bot$ �͘_�����ł���,
\item $p$ �� $n$ �ϐ��̏q��L���ŁC$t_{1},...t_{n}$ ���̍��̎��C$pt_{1}...t_{n}$ �͘_�����ł���,
\item $\alpha$ �� $\beta$ ���_�����Ȃ�΁C$(\alpha \to \beta)$ �͘_�����ł���,
\item $\alpha$ ���_�����ŁC$u$ ���̕ϐ��Ȃ�΁C$\forall u \alpha$ �͘_�����ł���B
\end{enumerate}
\end{df}

��`\ref{sec: def_of_formula}�ɂ����āC1 �܂��� 2 �̌`�̘_���������q�_����(atomic formula)�ƌĂԁB
�܂��C�_������\�킷���^�ϐ��Ƃ��āC$\alpha, \beta,\gamma ...$���g�p����B
��`�ʂ�ɘ_�����������ƁC���ʂ������Ȃ�C�ǂ݂ɂ����Ȃ�̂ŁC���ʂ�K���ɏȗ�
����B���̏ꍇ�C����Ȃ����ʂ́C�E����₤���Ƃɂ���B���Ƃ��΁C$\alpha \to
 \beta \to \gamma \to \delta$�́C$(\alpha \to (\beta \to (\gamma \to \delta)))$ ��\���Ă���D
%
\begin{df}[�̍��̎��R�ϐ�]\em \ 
�̍��ɂ��āC�̍��Ɍ���鎩�R�ϐ��̏W�� $V(t)$ ���ȉ��̂悤�ɒ�`����B
\begin{enumerate}
\item $V(u) = \{u\}$,
\item $V((ft_{1}..t_{n})) = V(t_{1}) \cup ... \cup V(t_{n})$.
\end{enumerate}
\end{df}
%
\begin{df}[�_�����̎��R�ϐ��Ƒ����ϐ�]\em \ 
�_���� $\alpha$ �Ɍ���鎩�R�ϐ��̏W�� $FV(\alpha)$, �����ϐ��̏W�� $BV(\alpha)$
 ���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $FV(\bot) = \phi$ ���� $BV(\bot) = \phi$,
\item $FV(pt_{1}...t_{n}) = V(t_{1}) \cup ... \cup V(t_{n})$ ���� $BV(pt_{1}...t_{n}) = \phi$,
\item $FV((\alpha \to \beta)) = FV(\alpha) \cup FV(\beta)$ ���� $BV(\alpha \to \beta) = BV(\alpha) \cup BV(\beta)$,
\item $FV(\forall u \alpha) = FV(\alpha) - \{u\}$ ���� $BV(\forall u \alpha) = BV(\alpha) \cup \{u\}$.
\end{enumerate}
\end{df}

�_����$\alpha$�ɑ΂��āC$V(\alpha) =FV(\alpha) \cup BV(\alpha)$ �ƒ�`����B

�_���� $\alpha$ �Ɍ���鎩�R�ϐ� $u$ �֌ő̍� $t$ ������������ $\{t/u\}\alpha$
 ���`���邪�C���̑���ł͑�����ɑ����ϐ��̒u��������������, ���R�� $u$ �ɂ�P�� $t$ ��
�u��������B
%
\begin{df}[�̍��̌ő̕ϐ��ւ̑��]\em \ 
�̍� $s$ �̌ő̕ϐ� $u$ �ւ̌̍� $t$ �̑��$\{t/u\}s$���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item $\{t/u\}u \equiv t$,
\item $\{t/u\}v \equiv v$,
\item $\{t/u\}(ft_{1}...t_{n}) \equiv (f\{t/u\}t_{1}...\{t/u\}t_{n})$.
\end{enumerate}
\end{df}
�A�[�I�ɒ�`�ɂ����Ă͓K�p�ł����`����ȏ゠��Ƃ��͔ԍ��̏��Ȃ��ق��̒�`
��K�p������̂Ƃ���B��̗�ł� $v \equiv u$ �̂Ƃ���, 2 �Ԗڂ̒�`�ł͂Ȃ� 1 
�Ԗڂ̒�`��K�p����B
%
\begin{df}[�_�����̎��R�ϐ��ւ̑��]\em \ 
�_���� $\alpha$ �̎��R�ϐ� $u$ �ւ̌̍� $t$ �̑�� $\{t/u\}\alpha$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item $\{t/u\} \bot \equiv \bot$,
\item $\{t/u\}(pt_{1}...t_{n}) \equiv (p\{t/u\}t_{1}...\{t/u\}t_{n})$,
\item $\{t/u\}(\alpha \to \beta) \equiv (\{t/u\}\alpha \to \{t/u\}\beta)$,
\item $\{t/u\}(\forall u \alpha) \equiv \forall u \alpha$,
\item $\{t/u\}(\forall v \alpha) \equiv \forall v \{ t/u \} \alpha$.
\end{enumerate}
\end{df}
%
\begin{df}[�_������ $\alpha$ ���l]\em \ 
�_���� $\beta$ �� $\gamma$ �� $\alpha$ ���l�ł���(���̂Ƃ��C$\beta
 \equiv_{\alpha} \gamma$�Ə���)���Ƃ��ȉ��̂悤�ɒ�`����B
\begin{enumerate}
\item $\beta \equiv \gamma$�Ȃ�΁C$\beta \equiv_{\alpha} \gamma$,
\item $\alpha \equiv_{\alpha} \gamma$ ���� $\beta \equiv_{\alpha} \delta$
      �Ȃ�΁C$(\alpha \to \beta) \equiv_{\alpha} (\gamma \to \delta)$,
\item $\{u/v\}\beta \equiv_{\alpha} \{u/w\}\gamma$ ���� $u\not\in V(\beta)\cup
      V(\gamma)$ �Ȃ�� $\forall v \beta \equiv_{\alpha} \forall w \gamma$.
\end{enumerate}
\end{df}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�[�^�t�����_��}
%
��{�L���Ƃ��āC�����_�ϐ��C�萔�L���C���̑��̋L����p�ӂ���D
\begin{itemize}
\item �����_�ϐ�: \ ���Z�̕ϐ�
\item �萔�L��: \ `$\mb{A}$', �e�̕ϐ� $u, v$ �ɂ������� `$\mb{J}^{u}_{v}$', �e�̍� $t$ �ɂ������� `$\mb{F}^{t}$'
\item ���̑��̋L��: \ `$.$', `$($', `$)$'
\end{itemize}
%
�����_�ϐ���\�����^�ϐ��Ƃ��āC$x,y,z...$��p���邱�Ƃɂ���B�e�����_�ϐ��͌^(Type)
�ƌĂ΂��_�����������Ă���B�ϐ� $x$ �̌^�� $\alpha$ �ł���Ƃ��C$Type(x) \equiv \alpha$�Ə����B
�܂��C�e�^�ɂ��āC���̌^�����悤�ȃ����_�ϐ����Z���݂��Ă��āC�����_�ϐ��͏��Ԃɕ���ł���,
�Ƃ���B$x$ ���^ $\alpha$ ��n�Ԗڂ̕ϐ��̎�, �^ $\beta$ �� $n$ �Ԗڂ̕ϐ����C$x^{\beta}$�Ƃ����B

�܂��C�ŏ��ɋ[�^�t�����_�����`����B�[�^�t�����_���͌^���𖳎����č\������
���^�t�����_���̂悤�Ȃ��̂ł���B��Œ�`���锼�����^�t�����_��, �����^�t�����_��, �^�t�����_��
�̂ǂ�����[�^�t�����_���ł���B
%
\begin{df}[�[�^�t�����_���̒�`]\em \ 
�[�^�t�����_�����ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item �����_�ϐ��͋[�^�t�����_���ł���D
\item $P$�@����с@$Q$�@���[�^�t�����_���Ȃ�΁C$(PQ)$�@�͋[�^�t�����_���ł���,
\item $M$ ���[�^�t�����_���� $x$ ���ϐ��Ȃ�΁C$(\lambda x.M)$ �͋[�^�t�����_���ł���,
\item $M$ ���[�^�t�����_���� $\alpha$ ���_�����Ȃ�΁C$(\mb{A}M)^{\alpha}$ �͋[�^�t�����_���ł���,
\item $M$ ���[�^�t�����_���Ȃ�΁C$(\mb{J}^{u}_{v}M)$�͋[�^�t�����_���ł���D
\item $M$���[�^�t�����_���Ȃ�΁C$(\mb{F}^{t}M)$�͋[�^�t�����_���ł���D
\end{enumerate}
\end{df}
%
�[�^�t�����_����\�킷���^�ϐ��Ƃ��āC$M,N,P,Q,R...$��p���邱�Ƃɂ���B
�܂��C��`�ʂ�ɋ[�^�t�����_���������Ɠǂ݂ɂ����Ȃ�̂�, ���ʂ�K���ɏȗ�����B
���̏ꍇ, ����Ȃ����ʂ͍�����₤���Ƃɂ���B�Ⴆ�΁C$MNPQ$ �� $(((MN)P)Q)$��\���B

�[�^�t�����_���Ɋ܂܂�Ă��郉���_�ϐ��̂����C���R�ϐ��ł�����̂����ׂďW�߂�
�����W�� $FV(M)$�C�����ϐ��ł�����̂����ׂďW�߂Ă����W�� $BV(M)$�C����у���
�_�ϐ������ׂďW�߂Ă����W�� $V(M)$ ���`����B
%
\begin{df}[�[�^�t�����_���̎��R�����_�ϐ�]\em \ 
�[�^�t�����_�� $M$ �ɂ��āC$M$ �̎��R�����_�ϐ��̏W�� $FV(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item $FV(x) = \{x\}$,
\item $FV((PQ)) = FV(P) \cup FV(Q)$,
\item $FV((\lambda x.P)) = FV(P) - \{x\}$,
\item $FV((\mb{A}P)^{\alpha}) = FV(P)$,
\item $FV((\mb{J}^{u}_{v}P)) = FV(P)$,
\item $FV((\mb{F}^{t}P)) = FV(P)$.
\end{enumerate}
\end{df}
%
\begin{df}[�[�^�t�����_���̑��������_�ϐ�]\em \ 
�[�^�t�����_�� $M$ �ɂ�������, $M$ �̑��������_�ϐ��̏W�� $BV(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item $BV(x) = \phi$,
\item $BV((PQ)) = BV(P) \cup BV(Q)$,
\item $BV((\lambda x.P)) = BV(P) \cup \{x\}$,
\item $BV((\mb{A}P)^{\alpha}) = BV(P)$,
\item $BV((\mb{J}^{u}_{v}P)) = BV(P)$,
\item $BV((\mb{F}^{t}P)) = BV(P)$.
\end{enumerate}
\end{df}
%
�[�^�t�����_�� $M$ �ɂ�����, $V(M) = FV(M) \cup BV(M)$�ƒ�`����B
%
\begin{df}[�ō������_�ϐ�]\em \ 
�[�^�t�����_�� $M$ �ɑ΂��C�ō������_�ϐ� $MLV(M)$ ���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $MLV(x) \equiv x$
\item $MLV((PQ))\equiv MLV(P)$
\item $MLV((\lambda x.P))\equiv MLV(P)$
\item $MLV((AP)^{\alpha})\equiv MLV(P)$
\item $MLV((\mb{J}^{u}_{v}P))\equiv MLV(P)$
\item $MLV((\mb{F}^{t}P))\equiv MLV(P)$
\end{enumerate}
\end{df}

���ɁC�[�^�t�����_���Ɋ܂܂�Ă���̕ϐ��̂���, ���R�ϐ��ł�����̂����ׂďW�߂�
�����W�� $FIV(M)$ ����сC�����ϐ��ł�����̂����ׂďW�߂Ă����W�� $BIV(M)$ ���`����B
%
\begin{df}[�[�^�t�����_���Ɍ���鎩�R�ő̕ϐ�]\em \ 
�[�^�t�����_�� $M$ �ɑ΂�, $M$ �Ɍ���鎩�R�ő̕ϐ��̏W��
$FIV(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item $FIV(x) = FV(Type(x))$,
\item $FIV((PQ)) = FIV(P) \cup FIV(Q)$,
\item $FIV((\lambda x.N)) = FIV(N) \cup FV(Type(x))$,
\item $FIV((\mb{A}N)^{\alpha}) = FIV(N) \cup FV(\alpha)$,
\item $FIV((\mb{J}^{u}_{v}N)) = FIV(N) \cup \{v \}$,
\item $FIV((\mb{F}^{t}N)) = FIV(N) \cup V(t)$.
\end{enumerate}
\end{df}
%
\begin{df}[�[�^�t�����_���Ɍ���鑩���ő̕ϐ�]\em \ 
�[�^�t�����_�� $M$ �ɑ΂��C$M$ �Ɍ���鑩���ő̕ϐ��̏W��
$BIV(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
\item $BIV(x) = BV(Type(x))$,
\item $BIV((PQ)) = BIV(P) \cup BIV(Q)$,
\item $BIV((\lambda x.N)) = BIV(N) \cup BV(Type(x))$,
\item $BIV((\mb{A}N)^{\alpha}) = BIV(N) \cup BV(\alpha)$,
\item $BIV((\mb{J}^{u}_{v}N)) = BIV(N) \cup \{u\}$,
\item $BIV((\mb{F}^{t}N)) = BIV(N)$.
\end{enumerate}
\end{df}
%
$IV(M) = FIV(M) \cup BIV(M)$�ƒ�`����D

�[�^�t�����_���ւ̑���́C�u�̍��̎��R�̕ϐ��ւ̑���v�Ɓu�^�t�����_���̎��R�����_�ϐ��ւ̑���v��
 2 ��ނ̑�����`����B
%
\begin{df}[��� $\{t/u, Var\}M$ �̒�`]\label{sec: def_of_dainyuu M}\em \ 
$t$ ���̍��C$u$ ���̕ϐ��C$Var$ ���̕ϐ��̏W���C$M$ ���[�^�t�����_���Ƃ���Ƃ��C
$\{ t/u, Var \} M$���ȉ��̂悤�ɋA�[�I�ɒ�`����B�܂��C�ȉ��ł�$\{ t/u, Var \}$��$\{ t/u \}$�Ɨ��L����B
\begin{enumerate}
\item $\{ t/u \} x \equiv x^{\{t/u\}Type(x)}$,
\item $\{ t/u \} (NR) \equiv (\{ t/u \} N\{ t/u \} R)$,
\item $\{ t/u \} (\lambda x.�m) \equiv (\lambda \{ t/u \} x.\{ t/u \} N)$,
\item $\{ t/u \} ((\mb{A}N)^{\alpha}) \equiv (\mb{A}\{ t/u \} N)^{\{ t/u \} \alpha}$,
\item $\{ t/u \} (\mb{F}^{s}N) \equiv (\mb{F}^{\{ t/u \} s}\{ t/u \} N)$,
\item $\{ t/u \} (\mb{J}^{u}_{v}N) \equiv (\mb{J}^{u}_{v}N)$,
\item $\{ t/u \} (\mb{J}^{w}_{v}N) \equiv (\mb{J}^{w}_{a}\{ t/u \} \{ a/v \} N)$ \ \ 
   (�������C$a$ �́C$a \not \in IV(N)\cup\{u,v,w\}\cup V(t)\cup Var$ �ƂȂ�ŏ��̌̕ϐ�).
\end{enumerate}
\end{df}
%
���̒�`�ł� $M$ ����Œ�`���鋷���^�t�����_���łȂ��Ƃ���, ���ʂ̈Ӗ��ł̑���ɂȂ��Ă��Ȃ��B
%
\begin{df}[�[�^�t�����_���̑��]\em \ 
$N, M$ ���[�^�t�����_���C$x$�������_�ϐ��C$Var$���̕ϐ��̏W���Ƃ���B$Type(N) \equiv Type(x)$�̎��C
$[N/x,Var]M$ ���ȉ��̂悤�ɒ�`����B�܂��C�ȉ��ł� $[N/x, Var]$ �� $[N/x]$ �Ɨ��L����B
\begin{enumerate}
\item $[N/x]x \equiv N$,
\item $[N/x]y \equiv y$,
\item $[N/x](PQ) \equiv ([N/x]P[N/x]Q)$,
\item $[N/x](\lambda x.P) \equiv (\lambda x.P)$,
\item $[N/x](\lambda y.P) \equiv (\lambda y.[N/x]P) \ \ (y \not \in FV(N) \ or \ x \not \in FV(P))$,
\item $[N/x](\lambda y.P) \equiv (\lambda z.[N/x][z/y]P)$ \ \ ($z$�́C$z \not \in V(xyNP)$��$Type(y) = Type(z)$�ƂȂ�悤�ȍŏ��̃����_�ϐ��Ƃ���),
\item $[N/x](\mb{A}P)^{\alpha} \equiv (A[N/x]P)^{\alpha}$,
\item $[N/x](\mb{J}^{u}_{v}P) \equiv (\mb{J}^{u}_{v}[N/x]P) \ \ (if \ v \not \in IV(N))$,
\item $[N/x](\mb{J}^{u}_{v}P) \equiv (\mb{J}^{u}_{w}[N/x] \{ w/v \} P)$ \ \ 
  ($w$ �́C$w \not \in IV(PNx) \cup \{u,v\}\cup Var$�ƂȂ�悤�ȍŏ��̌̕ϐ��Ƃ���),
\item $[N/x](\mb{F}^{t}P) \equiv (\mb{F}^{t}[N/x]P)$.
\end{enumerate}
\end{df}
%
��̒�`�̒��ł� $\{t/u, Var\}M$ �� $[N/x, Var]M$ �� $\{t/u\}M$ ����� $[N/x]M$ �Ɨ��L������,
����� $Var$ ����W���̂Ƃ�, $\{t/u, Var\}M$ �� $[N/x, Var]M$ �����ꂼ�� $\{t/u\}M$, $[N/x]M$ �Ə����B
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\section{�����^�t�����_��}
%
�����^�t�����_���̒�`�̑O�ɔ������^�t�����_�����`����B�[�^�t�����_���͌^�𖳎����č\��
���ꂽ��, �������^�t�����_���͌^�ɂ��������č\������K���^�����B
�������^�t�����_���̒�`���Ȍ��ɏq�ׂ邽�߂�, �ȉ��̕\����p����B
�u$M$ ���������^�t�����_������ $Type(M) \equiv \alpha$ �ł���v�Ƃ������Ƃ��C
\[M: \alpha\]
�Ɨ��L����B�܂�, �u$P_{1}$���C$P_{2}$����...����$P_{n}$�Ȃ�΁C$Q$�ł���v�Ƃ������Ƃ�
\[\infer{Q}{P_{1} & ... & P_{n}}\]
�Ɨ��L����B
�܂�, ���̔������^�t�����_���̒�`�� 5 �ł͎��̋L�@���p�����Ă���:
$Type(\{ x_{1}, \cdots, x_{n} \}) = \{ Type(x_{1}), ... , Type(x_{n}) \}$,\ \ 
$V(\{\alpha_1, \cdots, \alpha_n \}) = V(\alpha_1)\cup\cdots\cup V(\alpha_n)$�B
%
\begin{df}[�������^�t�����_��]\em \ 
\label{sec: def_of_lambda_term}
�������^�t�����_�� $M$ ����сC$M$ �̌^ $Type(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
	\begin{enumerate}
	\item  �����_�ϐ� $x$ �͔������^�t�����_���ł��̌^�� $Type(x)$ �ł���,
	\item  \[\infer{(MN):\beta}{M:(\alpha \to \beta) & N:\alpha} \ ,\]
	\item  \[\infer{(\lambda x.M):(\alpha \to \beta)}{M:\beta & x:\alpha} \ ,\]
	\item�@\[\infer{(\mb{A}M)^{\alpha}:\alpha}{M:\bot} \ ,\]
	\item  \[\infer{(\mb{J}^{u}_{v}M): \forall u \alpha}{M:\{v/u\}\alpha & v\not\in V(Type(FV(M))) \cup V(\forall u \alpha)} \ ,\]
	\item  \[\infer{(\mb{F}^{t}M): \{t/v\}\alpha}{M: \forall v \alpha} \ .\]
	\end{enumerate}
\end{df}
%
��̒�`�� 6 �ł͑�� $\{t/v\}$ ���p�����Ă��邪, ���̋����^�t�����_���ɂȂ邽�߂̏����𖞂�����
���Ȃ��ƕ��ʂ̈Ӗ��̑���ɂ͂Ȃ��Ă��Ȃ��B
%
\begin{df}[�����^�t�����_��]\em \ 
�������^�t�����_�� $M$ ���C�����^�t�����_���ł���Ƃ́C$BIV(M) \cap FIV(M) = \phi$ ���������Ă��邱�Ƃ������B
\end{df}

��`\ref{sec: def_of_reduction}�ŁC�����^�t�����_���� $\beta$-�ό`���`���邪�C�ό`�������ʂ������^�t��
���_���ɂȂ��Ă��邱�Ƃ��ؖ����邽�߂ɕK�v�Ȃ̂��C���̒藝\ref{sec: dainyuu2}��\ref{sec: dainyuu1}�ł���D
%
\begin{thm}
\label{sec: dainyuu2}
$M$�������^�t�����_���ŁC$V(t) \cap BIV(M) = \phi$�Ȃ��$ \{ t/a, Var \} M$�͋����^�t�����_���ŁC$Type(\{ t/a, Var \} M) \equiv \{ t/a, Var \}Type(M)$�ł���D�������C$Var$�͌̕ϐ��̗L���W���ŁC$BIV(M) \subseteq Var$�𖞂������̂Ƃ���D
\end{thm}

\begin{proof}
$M$�̒����ɂ��A�[�@�Ŏ����D\\
\begin{itemize}
\item ������1�̎��D\\
	$$ \{ t/a \} x \equiv x^{\{t/a\}Type(x)}$$
	$x^{\{t/a\}Type(x)}$ �������^�t�����_���ɂȂ�͎̂����ŁC�^�ɂ��Ă̏����������D\\
\item ������2�ȏ�̎��D

\begin{enumerate}
\item $M \equiv PQ$�̎��D
$$\{ t/a \} (PQ) \equiv \{ t/a \} P\{ t/a \} Q$$
$Type(P) \equiv \alpha \to \beta$, $Type(Q) = \alpha$�Ƃ���D�A�[�@�̉�����C$\{ t/a \} P$�͋����^�t�����_���ŁC$Type(\{ t/a \} P) \equiv \{ t/a \} Type(P) \equiv \{ t/a \} \alpha \to \{ t/a \} \beta$�������D���l�ɁC$\{ t/a \} Q$�͋����^�t�����_���ŁC$Type(\{ t/a \} Q) \equiv \{ t/a \} Type(Q) = \{ t/a \} \alpha$�������D
$$\infer{\{ t/a \} P\{ t/a \} Q: \{ t/a \}\beta}{\{ t/a \} P: \{ t/a \} \alpha \to \{ t/a \} \beta & \{ t/a \} Q: \{ t/a \} \alpha}$$
$\{ t/a \} P\{ t/a \} Q$�������^�t�����_���ɂȂ邽�߂ɂ́C
$$BIV(\{ t/a \} P\{ t/a \} Q) \cap FIV(\{ t/a \} P\{ t/a \} Q) = \phi$$
�ƂȂ�Ȃ���΁C�Ȃ�Ȃ��D$\{ t/a \} P$�ɂ����āC��`\ref{sec: def_of_dainyuu}�̋K��7���g����\�������邪�C���̎��ɐV�������������̕ϐ��́C$Var$�ɂ͌���Ȃ��̕ϐ��ł���D$Var \to BIV(PQ)$���C���̌̕ϐ���$BIV(\{ t/a \} P\{ t/a \} Q)$�ɂ͌���Ȃ��D$\{ t/a \}Q$�ɂ����Ă��C���l�̂��Ƃ���������̂ŁC
$$BIV(\{ t/a \} P\{ t/a \} Q) \cap FIV(\{ t/a \} P\{ t/a \} Q) = \phi$$
�͐�������D

\bigskip

\item $M \equiv \lambda x.P$�̎��D\\
$$\{ t/a \}  \lambda x.P \equiv \lambda \{ t/a \} x.\{ t/a \} P$$
$Type(x) \equiv \alpha$ , $Type(P) \equiv \beta$�Ƃ���D�A�[�@�̉�����C$\{ t/a \} x$�͋����^�t�����_���ŁC$Type(\{ t/a \} x) \equiv \{ t/a \}Type(x)$�������D�܂��C�������A�[�@�̉�����C$\{ t/a \} P$�͋����^�t�����_���ŁC$Type(\{ t/a \} P) \equiv \{ t/a \}Type(P)$�������D����āC
$$\infer{\lambda \{ t/a \} x.\{ t/a \} P : \{ t/a \} \alpha \to \{ t/a \} \beta}{\{ t/a \} P : \{ t/a \} \beta & \{ t/a \} x : \{ t/a \} \alpha}$$
�ɂ��C���̏ꍇ�͐����D

\bigskip

\item $M \equiv (AP)^\alpha$�̎��͏ȗ��D

\bigskip

\item $M \equiv \mb{J}^{u}_{v}P$�̎��D
$$
\{ t/a \}  \mb{J}^{u}_{v}P \equiv \mb{J}^{u}_{w}\{ t/a \} \{ w/v \} P
$$
�̏ꍇ�݂̂������D\\
$Type(P) \equiv \{ v/u \} \alpha$�Ƃ���D$P$�͋����^�t�����_���ł���̂ŁC�A�[�@�̉�����C$\{ w/v \} P$�͋����^�t�����_���ɂȂ�C$Type(\{ w/v \} P) \equiv \{ w/v \} Type(P) \equiv \{ w/v \} \{ v/u \} \alpha \equiv \{ w/u \}\alpha$�ƂȂ�D�X�ɁC$\{ w/v \} P$�ɋA�[�@�̉����K�p����ƁC$\{ t/a \} \{ w/v]P$�͋����^�t�����_���ɂȂ�C$Type(\{ t/a \} \{ w/v]P) \equiv \{ t/a \} \{ w/u \} \alpha$����������D�܂��C
\begin{eqnarray*}
\{ t/a \} \{ w/u \} \alpha 
&\equiv& \{ w/u \} \{ t/a \} \alpha \ \ (w��new�ŁCu \not \in V(t)���)
\end{eqnarray*}
�ƂȂ�D
$$
\infer{\mb{J}^{u}_{w}\{ t/a \} \{ w/v \} P: \forall u \{ t/a \} \alpha}{\{ t/a \} \{ w/v \} P: \{ w/u \} \{ t/a \} \alpha}
$$
���K�p�ł��邽�߂ɂ́C$w$�������Ă��Ȃ����肨���$\forall u \{ t/a \} \alpha$�Ɍ���Ȃ���΂悢�D���C$\mb{J}^{u}_{v}P$�������^�t�����_���ł���̂ŁC
$$
\infer{\mb{J}^{u}_{v}P: \forall u \alpha}{P: \{ v/u \} \alpha}
$$
�ɂ����āC$v$�͗����Ă��Ȃ�����Ɍ���Ă��Ȃ����C$\forall u \alpha$�ɂ�����Ă��Ȃ��D$w$��$P$�ɂ͌���Ȃ��ϐ��ł���̂ŁC$w$�́C$\{ w/v \} P$�̗����Ă��Ȃ�����Ɍ���Ȃ��D$w \not \in V(t)$�ł�����̂ŁC$\{ t/a \} \{ w/v \} P$�̗����Ă��Ȃ������$w$�͌���Ȃ��D����āC$\mb{J}^{u}_{w}\{ t/a \} \{ w/v \}P$�͋����^�t�����_���ɂȂ�D\\
�܂��C
\begin{eqnarray*}
\{ t/a \} Type(\mb{J}^{u}_{v}P)
&\equiv& \{ t/a \} \forall u \alpha \\
&\equiv& \forall u \{ t/a \} \alpha \ \  (a \not\equiv u ���) \\
&\equiv& Type(\{ t/a \} \mb{J}^{u}_{v}P)
\end{eqnarray*}
���C���̏ꍇ�������D

\bigskip

\item $M \equiv \mb{F}^{s}P$�̎��D\\
$$
\{ t/a \} \mb{F}^{s}P \equiv \mb{F}^{\{t/a\}s}\{ t/a \} P
$$
$Type(P) \equiv \forall u \alpha$����сC$Type(M) \equiv [ s/u ]\alpha $�Ƃ���D�A�[�@�̉�����C$\{ t/a \} P$�͋����^�t�����_���ŁC$Type(\{ t/a \} P) \equiv \{ t/a \} Type(P)$�������D�܂��C$u \not \in V(t)$���C$ \{ t/a \} \forall u \alpha \equiv \forall u \{ t/a \} \alpha$�������D
$$
\infer{\mb{F}^{\{t/a\}s}\{ t/a \} P: [ \{t/a\}s/u ]  \{ t/a \} \alpha}{\{ t/a \} P: \forall u \{ t/a \} \alpha}
$$
�܂��C
\begin{eqnarray*}
\{ t/a \} Type(\mb{F}^{s}P) 
&\equiv& \{ t/a \} [ s/u ] \alpha \\
&\equiv& \{ t/a \} \{ s/u \} \alpha \ \  (V(s) \cap BV(\alpha) = \phi ���)\\
&\equiv& \{ \{ t/a\} s/u \} \{ t/a \} \alpha \ \ (u \not \in V(t)���)\\
&\equiv& [ \{t/a\} s/u ]  \{ t/a \} \alpha \ \ (V( \{ t/a \} s) \cap BV( \{ t/a \} \alpha) = \phi ���)\\
&\equiv& Type(\{ t/a \} \mb{F}^{s}P)
\end{eqnarray*}
���C���̏ꍇ�������D

\end{enumerate}
\end{itemize}
�ȏ�ɂ��C�藝\ref{sec: dainyuu2}�͎����ꂽ�D\\
\end{proof}

\bigskip

\begin{thm}
\label{sec: dainyuu1}
$(\lambda x.M)N$�������^�t�����_���Ȃ��$[N/x, Var]M$�͋����^�t�����_���ł���, $Type([N/x,Var]M)\equiv Type(M)$ �ƂȂ�.�������C$Var$�͌̕ϐ��̗L���W���ŁC$BIV((\lambda x.M)N) \subseteq Var$�𖞂������̂Ƃ���D
\end{thm}

\begin{proof}
$M$�̒����ɂ��A�[�@�Ŏ����D
\begin{itemize}
\item ������1�̎��͏ȗ��D

\bigskip

\item ������2�ȏ�̎��D\\ 
\begin{enumerate}
\item $M \equiv PQ$�̎��D
$$[N/x]PQ \equiv [N/x]P[N/x]Q$$
�A�[�@�̉�����C$[N/x]P$�͋����^�t�����_���ŁC$Type(P) \equiv Type([N/x]P)$�������D���l�ɁC$[N/x]Q$�͋����^�t�����_���ŁC$Type(Q) \equiv Type([N/x]Q)$�������D
$[N/x]P[N/x]Q$�������^�t�����_���ɂȂ邽�߂ɂ́C$IBV([N/x]P) \cap IBV([N/x]Q) = \phi$���������Ȃ���΂Ȃ�Ȃ����C�藝\ref{sec: dainyuu2}�̏ؖ��̎��Ɠ��l�̗��R�Ő�������D

\bigskip

\item $M \equiv \lambda y.P$�̎��D\\
$[N/x] (\lambda y.P) \equiv \lambda z.[N/x][z/y]P$�̏ꍇ�̂ݎ����D\\
�A�[�@�̉�����C $[z/y]P$�͋����^�t�����_���ɂȂ�C$Type(P) \equiv Type([z/y]P)$�������D����ɂ�����x�A�[�@�̉����K�p�����$[N/x][z/y]P$�͋����^�t�����_���ɂȂ�C$Type(P) \equiv Type([N/x][z/y]P)$�������D$Type(y) \equiv Type(z)$���C$\lambda z.[N/x][z/y]P$�͋����^�t�����_���ɂȂ�C$Type(\lambda z.[N/x][z/y]P) \equiv Type(\lambda y.P)$�ƂȂ�D
\bigskip

\item $M \equiv (AN)^{\alpha}$�̎��͏ȗ��D

\bigskip

\item $M \equiv \mb{J}^{u}_{a}P$�̎��D\\
$[N/x](\mb{J}^{u}_{a}P) \equiv \mb{J}^{u}_{b}[N/x] \{ b/a \} P$�̏ꍇ�̂ݎ����D\\
$Type(M) \equiv \forall u \alpha$, $Type(P) \equiv \{ a/u \}\alpha$�Ƃ�����D�藝\ref{sec: dainyuu2}���C$ \{ b/a \} P$�͋����^�t�����_���ɂȂ�C
$$Type(\{ b/a \} P) \equiv \{ b/a \} Type(P) \equiv \{ b/u \} \alpha$$
�ƂȂ�D
%
%$Type(P) \equiv \{ a/u \}\alpha$�Ƃ�����D�藝\ref{sec: dainyuu2}���C$[b/a]P$�͋����^�t�����_���ɂȂ�C
%$$Type([b/a]P) \equiv \{ b/a \} Type(P) \equiv \{ b/u \} \alpha$$
%�ƂȂ�D
�A�[�@�̉�����C$[N/x] \{ b/a \} P$�͋����^�t�����_���ɂȂ�C$Type([N/x] \{ b/a \} P) \equiv Type(\{ b/a \} P)$�������D��`
$$\infer{\mb{J}^{u}_{b}[N/x] \{ b/a \} P: \forall u \alpha}{[N/x] \{ b/a \} P: \{ b/u \} \alpha}$$
���K�p�ł���̂́C$b$�������Ă��Ȃ�����Ɍ��ꂸ�C$\forall u \alpha$�Ɍ���Ă��Ȃ����ł���D$M \equiv \mb{J}^{u}_{a}P$�́C�����^�t�����_���ł���̂ŁC$a$��$P$�̗����Ă��Ȃ�����ɂ͌��ꂸ�C$\forall u\alpha$�ɂ͌���Ă��Ȃ��D����āC$\{ b/a \} P$�̗����Ă��Ȃ�����ɂ�$b$�͌���Ȃ��D$b$�̑I�ѕ�����C$b$��$N$�ɂ͌���Ȃ��ϐ��ł���̂ŁC$[N/x] \{ b/a \} P$�̗����Ă��Ȃ�����ɂ͌���Ȃ��D�܂��C���炩��$\forall u \alpha$�ɂ�$b$�͌���Ȃ��D����āC�K���͓K�p�\�ł���D�܂��C������ɐV���ɓ��������ϐ���new�ł���̂ŁC�̕ϐ��̑����ϐ��Ǝ��R�ϐ��͕�������Ă���D

\bigskip

\item $M \equiv \mb{F}^{t}P$�̎��͏ȗ��D
 
\end{enumerate}
\end{itemize}
�ȏ�ɂ��藝\ref{sec: dainyuu1}�͎����ꂽ�D
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�����^�t�����_���� $\beta$-�ό`}

\begin{df}[�����^�t�����_���̃��_�N�V����]\label{sec: def_of_reduction}\em \ 
$\beta$-�ό`�̑̌n $1\beta$ ���ȉ��̂悤�ɒ�`����B\\
{\bf (�����^)}
$$\begin{array}{ccc}
(\lambda x.M)N & \rhd_{1} & [N/x, BIV((\lambda x.M)N)]M,\\ \\

\mb{F}^{t}(\mb{J}^{u}_{v}M) & \rhd_{1} & \{t/u, BIV(M)\} M,\\ \\

(AM)^{\alpha \to \beta}N & \rhd_{1} & (AM)^{\beta}.
\end{array} $$
{\bf (���_�K��)}
\[
\infer{MN \rhd_{1} MR}{N \rhd_{1} R},
	\ \ \ \ \ \ \ \ \ \ 
\infer{MR \rhd_{1} NR}{M \rhd_{1} N},
	\ \ \ \ \ \ \ \ \ \ 
\infer{\lambda x.M \rhd_{1} \lambda x.N}{M \rhd_{1} N},
\]
\[
\infer{(\mb{A}M)^{\alpha} \rhd_{1} (\mb{A}N)^{\alpha}}{M \rhd_{1} N},
	\ \ \ \ \ \ \ \ \ \
\infer{\mb{J}^{u}_{v}M \rhd_{1} \mb{J}^{u}_{v}N}{M \rhd_{1} N},
	\ \ \ \ \ \ \ \ \ \
\infer{\mb{F}^{t}M \rhd_{1} \mb{F}^{t}N}{M \rhd_{1} N}.
\]
�̌n $1\beta$ �� $M \rhd_{1} N$ ���ؖ��ł���Ƃ��C$M \rhd_{1 \beta} N$ �Ƃ����B
\end{df}

$M$ ���� 0 ��ȏ�� $\beta$-�ό`���s���� $N$ �������鎞�C$M \rhd_\beta N$ �Ƃ����B
�܂��C$M \rhd_{1\beta}N$ �ƂȂ�悤�� $N$ �����݂��Ȃ����C$M$ �� ($\beta$)���K�`�ł���C�Ƃ����B
$M \rhd_\beta N$ ���C$N$ �����K�`�̎��C$N$ �� $M$ �̐��K�`�ł���C�Ƃ����B
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\begin{thm}
\label{sec: reduction1}
$M$�������^�t�����_����$M \rhd_{1 \beta} N$�Ȃ�΁C$N$�͋����^�t�����_���ł���B
\end{thm}

\begin{proof}
$M \rhd_{1\beta} N$�������ؖ��}�̒����ɂ��A�[�@�Ŏ����B
\begin{itemize}
\item ������1�C�܂�����̎��D
\begin{enumerate}
\item \[(AP)^{\alpha \to \beta}Q  \rhd_{1}  (AP)^{\beta}\] �̏ꍇ�͖��炩�B
\item \[(\lambda x.P)Q \rhd_{1} [Q/x, BIV((\lambda x.P)Q)]P\] �̏ꍇ�D
	�藝\ref{sec: dainyuu1} �ɂ��B
\item \[\mb{F}^{t}(\mb{J}^{u}_{v}P) \rhd_{1} \{t/v, BIV(P)\} P\] �̏ꍇ�D
	$\mb{F}^{t}(\mb{J}^{u}_{v}P)$ �������^�t�����_���Ȃ̂ŁC$P$�͋����^�t�����_���ł���B
�܂��C$V(t) \cap BIV(P) = \phi$����������B����āC�藝\ref{sec: dainyuu2}���C$\{t/v,BIV(P)\}P$
�͋����^�t�����_���ł���B
\end{enumerate}

\item ������2�ȏ�̎��D�ȒP�łȂ��̂�
$$
\infer{\mb{J}^{u}_{v}M \rhd_{1} \mb{J}^{u}_{v}N}{M \rhd_{1} N}
$$
�̏ꍇ�̂݁D�A�[�@�̉��肩��C$M$�������^�t�����_���ł���΁C$N$�͋����^�t�����_���ɂȂ�D��`
$$
\infer{\mb{J}^{u}_{v}N: \forall u \alpha}{N: \{ v/u \} \alpha}
$$
���K�p�ł��邽�߂̏�����$v$�������Ă��Ȃ�����Ɍ��ꂸ�C$\forall u \alpha$�Ɍ���Ă��Ȃ����Ƃł���D��,
$\mb{J}^{u}_{v}M$ �������^�t�����_���ł��邱�Ƃ����肵�Ă���̂ŁC��`
$$
\infer{\mb{J}^{u}_{v}M: \forall u \alpha}{M: \{ v/u \} \alpha}
$$
�͓K�p�ł��Ă���D����āC���̕�����ӂ͎������D
\end{itemize}
\begin{lem}
$M \rhd_{1\beta} N$ �Ȃ�΁C$FV(M) \supseteq FV(N)$.
\end{lem}
\end{proof}

\begin{df}[redex �� degree]\em \ 
�����^�t�����_���̂����C
$$(\lambda x.M)N,$$
$$\mb{F}^{t}(\mb{J}^{u}_{v}M),$$
$$(AM)^{\alpha \to \beta}N$$
�Ƃ����`�����Ă�����̂�redex�Ƃ����Dredex��degree�Ƃ́C����$Type(\lambda x.M)$�̒����C$Type(\mb{J}^{u}_{v}M)$�̒����C$\alpha \to \beta$�̒����C�̂��Ƃ������B
\end{df}
%
\begin{thm}[�����^�t�����_���̐��K���藝]\label{sec: normalization}
$M$ �������^�t�����_���Ȃ�� $M$ �̐��K�`�ɕό`�ł���B
\end{thm}
%
\begin{proof}
�^�t�����_���Ɋ܂܂��redex��degree�ōő�̂��̂�$l$�C���̂悤��redex�̌���$n$�Ƃ���D
$l$��$n$�Ɋւ���2�d�A�[�@�Ŏ����D

degree �� $l$ ��redex�ŁC$(AP)^{\alpha \to \beta}Q$��������$\mb{F}^{t}(\mb{J}^{u}_{a}P)$�Ƃ����`�̂��̂�����΁C��������_�N�V��������D����ƁCdegree��$l$��redex�̌���1����D

$(\lambda x.P)Q$�Ƃ����`�̂��̂ł���΁C$Q$�Ɋ܂܂��redex��degree���S��$l$�����ł���悤�Ȃ��̂�I�сC���_�N�V��������ƁCredex�̐���������\���͂��邪�Cdegree��$l$�̂��̂�1����D�Ȃ��C$n = 0$�ɂȂ�΁C$l$��1�ȏ㌸��D
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�^�t�����_���Ɛ��K�`�藝}
%
%��ʂ̌^�t�����_��$M$�ɂ��āC���̐��K�`�����݂��邱�Ƃ̏ؖ����s�����C���̑O�ɂ������̏���������D
%
%\bigskip
%
%\begin{df}($Hy(M)$�̒�`)\\
%�^�t�����_��$M$�ɂ��āC�_�����̏W��$Hy(M)$��	�C$Hy(M) = Type(FV(M))$�ƒ�`����D\\
%�������C$\Lambda = \{ x_{1}, ... , x_{n} \}$�̎��C$Type(\Lambda) = \{ Type(x_{1}), ... , Type(x_{n}) \}$�Ƃ���D
%\end{df}
%
�^�t�����_���̒�`���s���B
���̂��߂ɂ�, �܂��K�v�ȂƂ��͑����ϐ��̒u�����������镁�ʂ̑��
���`����K�v������B�����ł͕��ʂ̑���̒�`���Œ肵�Ȃ���, ��������𖞂����_����
�̏W������_�����̏W���ւ̎ʑ������ƌĂԂ��Ƃɂ���B�����Ă��̏�������������
��, ���̂悤�ȑ�����g���Ē�`���ꂽ�^�t�����_���ɑ΂��Đ��K�`�藝�����藧��
���������藝���ؖ�����B
%
%�����ł�, �^����ꂽ���_�}(�^�t�����_��) $M$ �ɂ�������, $M$ �̌��_($Type(M)$)�Ɠ������_������,
%���̑O��($FV(N)$)�� $M$ �̑O��Ɋ܂܂��悤�Ȑ��K�Ȑ��_�} $N$ �����݂��邱�Ƃ������B
%
\begin{df}[$\alpha$ �ϊ�������\���̂�����]\em \ 
$[t/u]$���C�_�����̏W������_�����̏W���ւ̎ʑ��ŁC�ȉ��̐����𖞂������̂ƒ�`����B
\begin{itemize}
\item $\alpha\equiv_\alpha\beta$ ���� $V(t)\cap BV(\beta) = \phi$ �Ȃ��, $[t/u]\alpha\equiv_\alpha \{t/u\}\beta$.
\end{itemize}
\end{df}

�^�t�����_���̒�`���Ȍ��ɏq�ׂ邽�߂�, �������^�t�����_���̒�`�̂Ƃ��Ɠ��l�ȕ\����p����B
�u$M$ ���^�t�����_������ $Type(M) \equiv \alpha$ �ł���v�Ƃ������Ƃ��C
\[M: \alpha\]
�Ɨ��L����B�܂�, �u$P_{1}$���C$P_{2}$����...����$P_{n}$�Ȃ�΁C$Q$�ł���v�Ƃ������Ƃ�
\[\infer{Q}{P_{1} & ... & P_{n}}\]
�Ɨ��L����B
�܂�, ���̌^�t�����_���̒�`�� 5 �ł͎��̋L�@���p�����Ă���:
$Type(\{ x_{1}, \cdots, x_{n} \}) = \{ Type(x_{1}), ... , Type(x_{n}) \}$,\ \ 
$V(\{\alpha_1, \cdots, \alpha_n \}) = V(\alpha_1)\cup\cdots\cup V(\alpha_n)$�B
%
\begin{df}[�^�t�����_��]\em \ 
\label{sec: def_of_lambda_term}
�^�t�����_�� $M$ ����сC$M$ �̌^ $Type(M)$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
	\begin{enumerate}
	\item  �����_�ϐ� $x$ �͌^�t�����_���ł��̌^�� $Type(x)$ �ł���,
	\item  \[\infer{(MN):\beta}{M:(\alpha \to \beta) & N:\alpha} \ ,\]
	\item  \[\infer{(\lambda x.M):(\alpha \to \beta)}{M:\beta & x:\alpha} \ ,\]
	\item�@\[\infer{(\mb{A}M)^{\alpha}:\alpha}{M:\bot} \ ,\]
	\item  \[\infer{(\mb{J}^{u}_{v}M): \forall u \alpha}{M:\{v/u\}\alpha & v\not\in V(Type(FV(M))) \cup V(\forall u \alpha)} \ ,\]
	\item  \[\infer{(\mb{F}^{t}M): [t/v]\alpha}{M: \forall v \alpha} \ .\]
	\end{enumerate}
\end{df}

�������^�t�����_���̒�`�ƈقȂ��Ă���̂�, �Ō�̍��ڂő�� $\{t/v\}$ ����� $[t/v]$ �ƂȂ��Ă��鏊��
���ł���B�܂�, ���̈Ⴂ�̂��߂ɋ����^�t�����_���������^�t�����_���Ƃ݂Ȃ����ꍇ�ƌ^�t�����_���Ƃ݂Ȃ���
�ꍇ�ł͌^���قȂ邱�Ƃ�����B�Ⴆ��, $Type(x)\equiv\forall u\forall v puv$ ����
$[a/u]\forall v puv\equiv\forall w paw$ �̂Ƃ����l���Ă݂�B 
�����^�t�����_�� $\mb{F}^{a}x$ �̌^�� $\forall v pav$ �ł��邪�^�t�����_�� $\mb{F}^{a}x$ �̌^��
$\forall w paw$ �ƂȂ�B 

���K�`�藝�͂قڌ^�t�����_���̑傫���ɂ��Ă̋A�[�@�ŏؖ�����̂ł��邪, �P���ȑ傫���ł͂��܂�������
���R�� $l(M)$ ���`��, $l(M)$ �ɂ��Ă̋A�[�@�ŏؖ�����B
%
\begin{df}[$l(\alpha)$ �̒�`]\em \ 
�_����$\alpha$�ɂ��āC���R��$l(\alpha)$���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $l(\alpha) = 1 \ \ (\alpha ��atomic�̎�)$,
\item $l(\alpha \to \beta) = l(\alpha) + l(\beta) + 1$,
\item $l(\forall u \alpha) = l(\alpha) + 1$.
\end{enumerate}
\end{df}
%
\begin{df}[$l(M)$ �̒�`]\em \ 
�^�t�����_��$M$�ɂ��āC����$l(M)$���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $l(x) = 2l(Type(x))$,
\item $l(PQ) = l(P) + l(Q) - 2l(Type(Q)) - 1$,
\item $l(\lambda x.P) = l(P) + l(Type(x)) + 1$,
\item $l((\mb{A}P)^{\alpha}) = l(P) + l(\alpha) - 1$,
\item $l(\mb{J}^{u}_{v}P) = l(P) + 1$,
\item $l(\mb{F}^{t}P) = l(P) - 1$.
\end{enumerate}
\end{df}

�Ȃ��C�C�ӂ̌^�t�����_�� $M$ �ɂ��āC$l(M)$ �͎��R���ɂȂ�B���̂��Ƃ������ɂ́C
\[l(M) \geq l(Type(M))\]
�������Ώ\���ł��邪�C�����$M$�̍\���ɂ��A�[�@�ŗe�ՂɎ�����B
%
\begin{thm}
\label{sec: existN}
$M$�𐳋K�ȋ����^�t�����_���Ƃ��C$FV(M) = \{ x_{1}, ... , x_{n} \} $�Ƃ���D$\alpha_{1} \equiv_{\alpha} Type(x_{1}), ... , \ \alpha_{n} \equiv_{\alpha} Type(x_{n})$����$\delta \equiv_{\alpha} Type(M)$�Ȃ�΁C$FV(N) = \{ x_{1}^{\alpha_{1}}, ... , x_{n}^{\alpha_{n}} \}$����$Type(N) \equiv \delta$�ƂȂ鐳�K�Ȍ^�t�����_��$N$�����݂���D
\end{thm}
%
\begin{proof}
$l(M)$�Ɋւ���A�[�@�Ŏ����D
\begin{itemize}
\item $Type(M)$��atomic�̎��D
	\begin{enumerate}
	\item $M$���ϐ�$x$�̎��D\\
		$N \equiv x$�ł悢�D
	\item $M$�������K���ɂ���ē���ꂽ��.
	  \begin{enumerate}
		\item �ϐ�$MLV(M)$��application�̋K�����K�p����Ă��鎞�D\\
		���̕����� $xR$ �ƂȂ��Ă���D$x$ �͗����Ă��Ȃ�����ł���D
		$Type(x) \equiv \alpha \to \beta$, $Type(R) \equiv \alpha$�Ƃ�����D\\
		�ϐ�$z$���C$xRM$�Ɍ��ꂸ�C$Type(z) \equiv \beta$�ƂȂ�悤�ȕϐ�$z$�Ƃ���D
		�^�t�����_��$C$���C$M \equiv [xR/z]C$�Ƃ����C$z\equiv MLV(C)$�ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$l(xR) = l(x) + l(R) - 2l(Type(R)) - 1 = 2l(\beta) + l(R) + 1$\\
		$l(z) = 2l(Type(z)) = 2l(\beta)$\\
		���C$l(xR) > l(z)$�ł���D���̂ق��̕����ł́C$M$��$C$�͓���ł���̂ŁC$l(M) > l(C)$ ����������.
        �܂��C$l(M) > l(R)$�ƂȂ�D����āC$C$����сC$R$�ɋA�[�@�̉��肪�K�p�\�ł���D\\
		$C$�ɋA�[�@�̉����K�p���ē���ꂽ����$N_{1}$, $R$�ɋA�[�@�̉����K�p���ē���ꂽ
		����$N_{2}$�Ƃ���D�܂��C$C$�Ɋ܂܂�Ă���$z$�́C$N_{1}$�ł�$z^{\beta '}$�ɒu���������
        �����Ƃ���D\\
		$N$�Ƃ��āC$[x^{\alpha '}N_{2}/z^{\beta '}]N_{1}$��I�ׂ΂悢�D�������C$\alpha '$��,
        $\{ \alpha_{1}, .. ,\alpha_{n} \}$�Ɋ܂܂�C$\alpha ' \equiv_{\alpha} Type(x)$�ł���悤
        �Ȃ��̂�I�ԁD
%
		\item �ϐ� $MLV(M)$ �� $\bot$ �̏����K�����g���Ă��鎞�D\\
		���̕����� $(\mb{A}x)^{\alpha}$ �ƂȂ��Ă���D\\
		$N\equiv (\mb{A}x)^\delta$ �Ƃ���΂悢.
%
		\item �ϐ� $MLV(M)$ �� $\forall$ �̏����K�����g���Ă��鎞�D\\
		���̕����� $\mb{F}^{t}x$ �ƂȂ��Ă���D$Type(x) \equiv \forall u \alpha$ �Ƃ�����D
		$\forall u\alpha$ �� $\alpha$ ���l�Ș_������ $\forall v\beta$ �Ƃ���. $w$ ��V�����̕ϐ���
        ����� $\{w/v\}\beta\equiv_\alpha\{w/u\}\alpha$ �ƂȂ��Ă���.
        �ϐ� $z$ ���C$xM$�Ɍ��ꂸ�C$Type(z) \equiv \{t/u\}\alpha$ �ł���V���������_�ϐ��Ƃ���D
		�^�t�����_�� $C$ ���C$M\equiv [\mb{F}^{t}x/z]C$ �ƂȂ�C$z\equiv MLV(C)$ �ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$l(\mb{F}^{t}x) = 2l(\forall u \alpha) - 1 = 2l(\alpha) + 1$\\
		$l(z) = 2l(\alpha)$\\
		�ł���D���̑��̕����ł́C$M$ �� $C$ �͓���ł���̂ŁC$l(M) > l(C)$ ����������D����āC$C$�ɋA�[
        �@�̉��肪�K�p�\�ł���D\\
		$C$ �ɋA�[�@�̉����K�p���ē���ꂽ���� $N_{1}$ �Ƃ���D�܂��C$C$ �Ɋ܂܂�Ă��� $z$ ��, $N_{1}$
        �ł� $z^{[t/v]\beta}$ �ɒu��������Ă���D\\
		$N$ �Ƃ��āC$[\mb{F}^{t}x^{\forall v\beta}/z^{[t/v]\beta}]N_{1}$ �Ƃ���΂悢.
	  \end{enumerate}
	\end{enumerate}
\item $Type(M)\equiv\alpha\to\beta$�̎��D\\
	$\delta\equiv\alpha'\to\beta'$�Ƃ����D
	\begin{enumerate}
	\item $\to$�̓����K���ɂ�蓾��ꂽ���D
		$M$ �� $\lambda x.P$ �Ƃ����`�����Ă���. $l(P) < l(\lambda x.P)$ ���C$P$ �ɋA�[�@�̉���
        ���K�p�ł���D$P$�ɋA�[�@�̉����K�p���� $Type(N_1)\equiv\beta'$ �ƂȂ鐳�K�Ȍ^�t�����_
        �� $N_{1}$ �𓾂�,\\
		$N\equiv\lambda x^{\alpha'}.N_{1}$ �Ƃ���΂悢�D
	\item �����K���ɂ�蓾��ꂽ�C�܂���$M$���ϐ��̎��D\\
		$x$ ���^ $\alpha$ �̐V���������_�ϐ��Ƃ���.
		$l(M) > l(Mx)$ ���C$Mx$�ɋA�[�@�̉��肪�K�p�\�ł���D
		$Mx$�ɋA�[�@�̉����K�p���� $Type(N_1)\equiv\beta'$ �ƂȂ鐳�K�Ȍ^�t�����_�� $N_{1}$ �𓾂�.\\
		$N\equiv\lambda x^{\alpha'}.N_{1}$ �Ƃ���΂悢�D
	\end{enumerate}
\item $Type(M)\equiv\forall u\alpha$�̎��D\\
	$\delta\equiv\forall w \beta$ �Ƃ���. $\alpha$ ���l�̒�`���, $a$ ��V�����̕ϐ��Ƃ����,
    $\{ a/u \} \alpha \equiv_{\alpha} \{ a/w \} \beta$ ����������.
	\begin{enumerate}
	\item $\forall$�̓����K���ɂ�蓾��ꂽ��.
		$M$ �� $\mb{J}^{u}_{v}P$ �Ƃ����`�����Ă���. $l(\mb{J}^{u}_{v}P) > l(\{a/u\}P)$���C$\{a/u\}P$
        �ɋA�[�@�̉��肪�K�p�ł���D
		$\{a/u\}P$�ɋA�[�@�̉����K�p���� $Type(N_1)\equiv\{a/w\}\beta$ �ƂȂ鐳�K�Ȍ^�t�����_���� $N_{1}$
        �𓾂�. $N\equiv\mb{J}^{w}_{a}N_{1}$�Ƃ���΂悢�D
	\item �����K���ɂ�蓾��ꂽ�C�܂��� $M$ ���ϐ��̎��D\\
		$a$ ��V�����̕ϐ��Ƃ���. $l(M) > l(\mb{F}^{a}M)$ ���C$\mb{F}^{a}M$ �ɋA�[�@�̉��肪�K�p�ł���.
		$\mb{F}^{a}M$ �ɋA�[�@�̉����K�p���� $Type(N_1)\equiv\{a/w\}\beta$ �ƂȂ鐳�K�Ȍ^�t�����_����
        $N_{1}$ �𓾂�.\\
		$N\equiv\mb{J}^{w}_{a}N_{1}$ �Ƃ���΂悢�D
	\end{enumerate}
\end{itemize}
\end{proof}
%
\begin{df}[�ϊ� $T(V,\alpha)$]\em \ 
�̕ϐ��̏W��$V$, ����ј_����$\alpha$�ɂ��āC�_����$(T(V,\alpha))$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item $T(V, pt_{1}...t_{n}) \equiv pt_{1}...t_{n}$,
\item $T(V,\bot) \equiv \bot$,
\item $T(V, \alpha \to \beta) \equiv T(V, \alpha) \to T(V, \beta)$,
\item $T(V, \forall u \alpha) \equiv \forall u T(V, \alpha)$ \ \ ($u \not \in V \cup FV(T(V, \alpha))$�̂Ƃ�),
\item $T(V, \forall u \alpha) \equiv \forall w \{ w/u \} T(V, \alpha)$.
\end{enumerate}
��`5�ɂ����āC$w$�́C$w\not\in V\cup FV(T(V,\alpha))$�ƂȂ�悤�ȍŏ��̕ϐ��Ƃ���D
\end{df} 
%
\begin{df}[�ϊ� $T(V,M)$]\em \ 
�̕ϐ��̏W�� $V$ ����ь^�t�����_��$M$�ɂ���, �^�t�����_�� $(T(V,M))$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item $T(V, x) \equiv x^{T(V, Type(x))}$,
\item $T(V,PQ) \equiv T(V,P) T(V,Q)$,
\item $T(V,\lambda x.P) \equiv \lambda x^{T(V, Type(x))} .T(V,P)$,
\item $T(V,\mb{A}P)^{\alpha}) \equiv (\mb{A}T(V,P))^{T(V,\alpha)}$,
\item $T(V,\mb{J}^{u}_{v}P) \equiv \mb{J}^{u}_{v}T(V,P)$ \ \  ($u \not \in V \cup FIV(T(V, P))$�̂Ƃ�),
\item $T(V,\mb{J}^{u}_{v}P) \equiv \mb{J}^{w}_{v}T \{ w/u \}T(V,P)$,
\item $T(V,\mb{F}^{t}P) \equiv \mb{F}^{t}T(V,P)$.
\end{enumerate}
��`6�ɂ����āC$w$�́C$w \not \in  (V \cup FIV(T(V, \alpha)))$�ƂȂ�悤�ȍŏ��̕ϐ��Ƃ���D
\end{df}

��`��薾�炩�ɁC�^�t�����_��$M$�ɂ��āC$V \cap BIV(T(V,M)) = \phi$����������D
%
\begin{thm}[���K�`�藝]
$M$���^�t�����_���Ȃ�΁C���̏����𖞂����^�t�����_��$N$�����݂���D
\begin{itemize}
\item $Type(M) \equiv Type(N)$.
\item $FV(M) \supset FV(N)$.
\item $N$�͐��K�`�ł���.
\end{itemize}
\end{thm}
%
\begin{proof}
�^����ꂽ�^�t�����_��$M$�ɂ��āC$FV(M) = \{ x_{1}, ... , x_{n} \}$�Ƃ���D\\
$M$�ɑ΂��C�^�t�����_��$P$���C$$P = T(FIV(M), M)$$
�ƒ�߂�ƁC$P$�́C�����^�t�����_���ɂȂ�C$Type(P) \equiv_{\alpha} Type(M)$����������D\\
�܂��C$FV(P) = \{ x_{1}^{T(FIV(M), Type(x_{1}))}, ... , x_{n}^{T(FIV(M), Type(x_{n}))} \}$�ƂȂ�D\\
�����ŁC$T(FIV(M), Type(x_{i})) \equiv_{\alpha} Type(x_{i})$���������Ă���D\\
$P$�͋����^�t�����_���Ȃ̂ŁC�藝\ref{sec: normalization}���C$P$�̐��K�`$P'$�����݂���D\\
$FV(P') \subset FV(P)$�ƂȂ�D$x_{i}^{T(FIV(M), Type(x_{i}))} \in FV(P')$�ɑ΂��āC$Type(x_{i}^{T(FIV(M), Type(x_{i}))}) \equiv_{\alpha} Type(x_{i})$�ƂȂ�D
����$P'$�ɒ藝\ref{sec: existN}��K�p����$\delta \equiv Type(M)$�Ƃ���΁C�ړI�Ƃ���$N$��������D
\end{proof}

%$FV(N) = \{ x_{i} \ | \ \exists y_{k} \ s.t. \ y_{k} \in FV(P') $����$Type(y_{k}) \equiv_{\alpha} Type(x_{i}) \} $
%% �Q�l����
\begin{thebibliography}{99}
\addcontentsline{toc}{section}{�Q�l����}

\bibitem{ko1} Yuichi Komori,
{\it $\lambda \rho$ calculas: A natural reduction for classical logic,}\
Bulletinl of the Section of  Logic Volume 31/2 (2002), pp.\ 65--70.

\bibitem{ko2} Yuichi Komori and Arato Cho,
{\it $\lambda \rho$-calculas,}\
preprint.

\bibitem{ge1} Gerhard Gentzen,
{\it Untersuchungen $\ddot{u}$ber das logische Schliessen. Mathematische
Zeitschrift,}\
 Vol. 39, pp. 176-210, 405-431, 1935. 

\bibitem{pr1} Dag Prawitz, {\it Natural deduction, Vol.3 of Stockholm Studies in Philosophy.}\
 Almqvist and Wilksell, Stockholm, 1965.

\end{thebibliography}
\end{document}
