\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]{��}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% �\��
\thispagestyle{empty}


\vspace*{1cm}


\begin{center}
{\Large\gt ��t��w��w�@�@���w�����ȁ@\\[3mm]�C�m�_��}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf $\alpha$���l�Ș_�����𓯈ꎋ���Ȃ�����ł̒��ώ�`�q��_���̐��K���藝�̏ؖ�}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����22�N3��}
\end{center}

\vspace*{5.7cm}
\begin{center}
{\Large\gt ��՗��w ��U \\[2mm]���w��񐔗��w�R�[�X}
\end{center}

\vspace*{5mm}
\begin{center}
{\Large\gt �R�c�b�C}
\end{center}

\setcounter{page}{0}

\newpage

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

\newpage

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

\section{�͂��߂�}
�����_���ƒ��ώ�`�q��_���Ƃ̊Ԃ̊֌W�́C�J���[�E�n���[�h�̑Ή��Ƃ��Ă悭�m���Ă���D�܂��C���̑Ή��̌ÓT�_���ւ̊g���ɂ��Ă��CMichel Parigot �����\����$\lambda \mu$-calculas��C�ÐX�Y��ɂ��$\lambda \rho$-calculas \cite{ko1} \cite{ko2}�����݂���D���̘_���̖ړI�́C�J���[�E�n���[�h�̑Ή���p���Ē��ώ�`�q��_���̐��K���藝���ؖ����邱�Ƃł���D

�Ȃ��C���̘_���͌ÐX�Y��搶�ɂ��ڍׂȕ��j���^�����C�����̌����E���؂��R�c���s�����D
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{���}

�����̐��K���藝�̏ؖ��ł́C$\alpha$���l�Ș_�����𓯈ꎋ���邱�Ƃ��Öقɉ��肵�Ă��镔��������悤�Ɏv���邪�C���̘_���ł́C$\alpha$���l�Ș_�����𓯈ꎋ���Ȃ�����ł̌����ȏؖ����s���Ă���D���ꎋ���Ȃ����R�Ƃ��ẮC���ꎋ���Ȃ��Ă��ؖ��\�͕͂ς��Ȃ����C$cut$�̂Ȃ��ؖ��}���C$\alpha$�ϊ��𓯈ꎋ���Ȃ��Ă������Ă��܂�����ł���D

�Ȃ��C��ʂ̌^�t�����_���ɂ��Ă̓��_�N�V���������܂���`�ł��Ȃ��D���̂��߁C�܂��͋����^�t�����_�����`���C���̋����^�t�����_���ɂ��Ă̐��K���藝���ؖ�����D�����Ă��̌��ʂ��g���āC��ʂ̏ؖ��ł���_�����ɂ��āC���K�ȏؖ��}�����邱�Ƃ��ؖ�����D

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

�܂��C���̘_���̓����Ƃ��āC�_�����ւ̑���̒�`�Ƃ��ď�������Ȓ�`���̗p���Ă���D���̘_���Ŏ�ɗp�����Ă�����$\{ \ / \ \}$�ł́C������ɁC�����ϐ��̒u�������͈�؋N���炸�C���̂܂ܑ�����s���D�Ⴆ�΁C
$$\{ u/v \} \forall u (pu \to pv) \equiv \forall u (pu \to pu)$$
�ƂȂ�D���̑��$\{ \ / \ \}$��p���邱�Ƃɂ��C�����ϐ��̒u���������C�ɂ��邱�ƂȂ��c�_��i�߂邱�Ƃ��ł���悤�ɂȂ�D

���ɁC�^�t�����_���̒�`���s���Ă���D�^�t�����_���̒�`�́C��q����Ă���Ƃ���ł���D�ʏ�C�J���[�E�n���[�h�̑Ή��́C�u�ؖ��}�v�Ɓu�����_���v�̊Ԃ̊֌W�Ƃ��Ĉ����邪�C���̘_���ł́C�^�t�����_���𒼐ځC���ώ�`�q��_���̏ؖ��}���Ƃ݂Ȃ��Ă���D

�^�t�����_��$M$���C$FIV(M) \cap BIV(M) = \phi$�𖞂����Ă���Ƃ��C�܂�C���R�̕ϐ��Ƒ����̕ϐ�����������Ă���Ƃ�$M$�͋����^�t�����_���ł���C�ƒ�`����D

���_�N�V�����̒�`�́C�����^�t�����_���ɂ��čs���Ă���D�_���L���̓����K�����K�p����Ă����ɂ��̘_���L������������Ă���悤�Ȏ���3�̃P�[�X�ɂ��ă��_�N�V�������s���Ă���D
$$\begin{array}{ccc}
(\lambda x.M)N & \rhd_{1\beta} & [N/x]M,\\ \\

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

(AM)^{\alpha \to \beta}N & \rhd_{1\beta} & (AM)^{\beta}.
\end{array} $$

���̒�`�́C�����^�t�����_���ɂ��ẮC���܂������Ă��邪�C�ʏ�̌^�t�����_���ɑ΂��ẮC���܂���`�ł��Ă��Ȃ��D���̂悤�ȗ�Ƃ��āC���̂悤�Ȍ^�t�����_��$\mb{F}^{u}(\mb{J}^{v}_{a}(\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x))))$���l����D
$$\infer{\mb{F}^{u}(\mb{J}^{v}_{a}(\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x)))):  \forall w \ puw}{
	\infer{\mb{J}^{v}_{a}(\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x))): \forall v \forall u \ pvu}{
		\infer{\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x)): \forall u \ pau} {
			\infer{\mb{F}^{u}(\mb{F}^{a}x): pau}{
				\infer{\mb{F}^{a}x: \forall v \ pav}{x: \forall u \forall v \ puv}}}}}$$
���̌^�t�����_���͋����^�t�����_���ł͂Ȃ��D���̌^�t�����_�������_�N�V��������(�������C�_�����ւ̑���̒�`�́C$\{ \ / \ \}$�ł͂Ȃ��C�����ϐ��̒u���������N����悤�Ȉ�ʓI�ȑ���̒�`��p����)�ƁC
$$\infer{[u/a](\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x))): \forall c \ puc}{
	\infer{[u/a](\mb{F}^{u}(\mb{F}^{a}x)): puu}{
		\infer{[u/a](\mb{F}^{a}x): \forall v \ puv}{[u/a]x: \forall u \forall v \ puv}}}$$
$[v/a](\mb{J}^{u}_{u}(\mb{F}^{u}(\mb{F}^{a}x)))$�Ƀ��_�N�V��������邪�C����͌^�t�����_���ł͂Ȃ��Ȃ��Ă��܂��D

�܂��C�ʂ̌^�t�����_���Ƃ��āC
$$\infer{\mb{F}^{a}(\mb{J}^{b}_{v}(\mb{J}^{a}_{u}(\mb{F}^{v}(\mb{F}^{u}x)))):  \forall c \ pca}{
	\infer{\mb{J}^{b}_{v}(\mb{J}^{a}_{u}(\mb{F}^{v}(\mb{F}^{u}x))): \forall b \forall a \ pab}{
		\infer{\mb{J}^{a}_{u}(\mb{F}^{v}(\mb{F}^{u}x)): \forall a \ pav} {
			\infer{\mb{F}^{v}(\mb{F}^{u}x): puv}{
				\infer{\mb{F}^{u}x: \forall v \ puv}{x: \forall u \forall v \ puv}}}}}$$
$\mb{F}^{a}(\mb{J}^{b}_{v}(\mb{J}^{a}_{u}(\mb{F}^{v}(\mb{F}^{u}x))))$���l����D���̌^�t�����_�����C�����^�t�����_���ł͂Ȃ��D���̌^�t�����_�������_�N�V��������ƁC
$$\infer{[a/v](\mb{J}^{u}_{b}(\mb{F}^{b}(\mb{F}^{a}x))): \forall b \ pba}{
	\infer{[a/v](\mb{F}^{b}(\mb{F}^{u}x)): pua}{
		\infer{[a/v](\mb{F}^{u}x): \forall v \ puv}{[a/v]x: \forall u \forall v \ puv}}}$$
$[a/v](\mb{J}^{u}_{b}(\mb{F}^{b}(\mb{F}^{a}x)))$��������D���̏ꍇ�ł́C���_�N�V��������^�t�����_���ɂȂ��Ă͂��邪�C�^�͈قȂ��Ă���D
���̂悤�ɁC�ʏ�̌^�t�����_���ɂ��ẮC���_�N�V���������܂���`�ł��Ȃ��D

���_�N�V��������O�������^�t�����_���Ȃ�΁C���_�N�V������������^�t�����_���ɂȂ�C$Type$���ω����Ȃ����Ƃ��ؖ��ł���D�܂��C�����^�t�����_���ɂ��ẮC�^�t�����_�������_�N�V�������Ă������Ƃɂ���āC�����^�t�����_���ɂ��Ă̐��K���藝�𒼐ڏؖ����邱�Ƃ��ł���D

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

�^�t�����_��$M$���^����ꂽ���C$M$�̌̕ϐ��̂����C���R�̕ϐ��Ƃ��Ă��C�����̕ϐ��Ƃ��Ă�����Ă���ϐ�������΁C��������Ă��镔���̂ݐV���ȕϐ��Œu�������Ăł���^�t�����_����$N$�Ƃ���D����$N$�͋����^�t�����_���ɂȂ�̂ŁC���̐��K�`$N'$�����܂�D����$N'$�Ɏ��̒藝��K�p����ƁC$M$�̐��K�`�����߂邱�Ƃ��ł���D


{\bf �藝} $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

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

\section{�_����}

��{�L���Ƃ��āC�̕ϐ��C�q��L���C�֐��L���C�_���L���C���̑��̋L����p�ӂ���D
\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����D\\
�֐��L����\�킷���^�ϐ��Ƃ��āC$f,g,h,...$���g�p����D

\begin{df} (�̍��̒�`�j\\
�̍����ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item �̕ϐ�$u$�͍��ł���D
\item $t_{1},...,t_{n}$�����ł���C$f$��$n$�ϐ��̊֐��L���Ȃ�΁C$(ft_{1}...t_{n})$�͍��ł���D
\end{enumerate}
\end{df}

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

 \bigskip

��`\ref{sec: def_of_formula}�ɂ����āC1�܂���2�̌`�̘_���������q�_����(atomic formula)�ƌĂԁD

\bigskip

�q��L����\�킷���^�ϐ��Ƃ��āC$p,q,r...$���g�p����D�܂��C�_������\�킷���^�ϐ��Ƃ��āC$\alpha, \beta,\gamma ...$���g�p����D

\bigskip

��`�ʂ�ɘ_�����������ƁC���ʂ������Ȃ�C�ǂ݂ɂ����Ȃ�ꍇ������̂ŁC���ʂ�K���ɏȗ����邱�Ƃ�����D���̏ꍇ�C����Ȃ����ʂ́C�E����₤���Ƃɂ���D���Ƃ��΁C$\alpha \to \beta \to \gamma \to \delta$�́C$(\alpha \to (\beta \to (\gamma \to \delta)))$��\���Ă���D

\bigskip

\begin{df}(�̍��̎��R�ϐ�)\\
�̍��ɂ��āC�̍��Ɍ���鎩�R�ϐ��̏W��V(t)���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $V(u) = u$,
\item $V((ft_{1}..t_{n})) = V(t_{1}) \cup ... \cup V(t_{n})$.
\end{enumerate}
\end{df}

\bigskip

\begin{df}(�_�����̎��R�ϐ��Ƒ����ϐ�)\\
�_�����Ɍ���鎩�R�ϐ��̏W��$FV$, �����ϐ��̏W��$BV$���ȉ��̂悤�ɒ�`����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}

\bigskip

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

\bigskip

�܂��C������`���邪�C$\{ \ / \ \}$��$[ \ / \ ]$��2��ނ̑�����`����D

\bigskip

\begin{df} (�̍��ւ̑��)\\
�̍�$s$�̎��R�ϐ�$u$�ւ̌̍�$t$�̑��$\{t/u\}s$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item $\{t/u\}u \equiv t$,
\item $\{t/u\}u' \equiv u' \ \ (if \ u \not \equiv u')$,
\item $\{t/u\}(ft_{1}...t_{n}) \equiv (f\{t/u\}t_{1}...\{t/u\}t_{n})$.
\end{enumerate}
\end{df}

\bigskip

\begin{df} (�_�����ւ̑��)\\
�_����$\alpha$�̎��R�ϐ�$u$�ւ̌̍�$t$�̑��$\{t/u\}\alpha$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\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}

\bigskip

�A�[�I�Ȓ�`�ɂ����āC�����̒�`���K�p�\�ȏꍇ�́C�ԍ��̏������K����D�悵�ēK�p���邱�Ƃɂ���D�Ⴆ�΁C��̒�`�ɂ����ċK��4�ƋK��5�̗������K�p�\�ł���΁C�K��4���D�悳���D

\bigskip

���$\{ \ / \ \}$�ł́C������ɑ����ϐ��̒u�������͋N���炸�C���̂܂ܑ�����s���D

\bigskip

\begin{df} (�_������$\alpha$���l)\\
�_����$\beta$��$\gamma$��$\alpha$���l�ł���(���̂Ƃ��C$\beta \equiv_{\alpha} \gamma$�Ə���)���Ƃ��ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $\beta \equiv \gamma$�Ȃ�΁C$\beta \equiv_{\alpha} \gamma$,
\item $\beta \equiv_{\alpha} \beta '$���C$\gamma \equiv_{\alpha} \gamma '$�Ȃ�΁C$(\beta \to \gamma) 	\equiv_{\alpha} (\beta ' \to \gamma ')$,
\item $\{u/v\}\beta \equiv_{\alpha} \{u/w\}\gamma$���C$u \not \in V(\beta) \cup V(\gamma)$�Ȃ�΁C$\forall v \beta \equiv_{\alpha} \forall w \gamma$.
\end{enumerate}
�������C3�ɂ����āC$u$��$\beta$�����$\gamma$�ɂ͌���Ȃ��̕ϐ��Ƃ���D
\end{df}

\bigskip



\bigskip


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

\section{�^�t�����_��}

��{�L���Ƃ��āC�����_�ϐ��C�萔�L���C���̑��̋L����p�ӂ���D
\begin{itemize}
\item �����_�ϐ� \ ���Z�̕ϐ�
\item �萔�L�� \ $\mb{A},\mb{J}^{u}_{v},\mb{F}^{t}$
\item ���̑��̋L�� \ $.,(,)$
\end{itemize}

�����_�ϐ���\�����^�ϐ��Ƃ��āC$x,y,z...$��p���邱�Ƃɂ���D

�e�����_�ϐ��͌^(Type)�ƌĂ΂��_�����������Ă���D�ϐ�$x$�̌^��$\alpha$�ł���Ƃ��C$Type(x) \equiv \alpha$�Ə����D�܂��C�S�Ă̌^�ɂ��āC���̌^���������_�ϐ����Z���݂��邱�Ƃ����肷��D

\bigskip

�܂��C�ŏ��ɋ[�^�t�����_�����`����D

\begin{df}(�[�^�t�����_���̒�`)\\
�[�^�t�����_�����ȉ��̂悤�ɋA�[�I�ɒ�`����D
\begin{enumerate}
\item �����_�ϐ��͋[�^�t�����_���ł���D
\item $P$�����$Q$���[�^�t�����_���Ȃ�΁C$(PQ)$�͋[�^�t�����_���ł���D
\item $M$���[�^�t�����_���ŁC$x$���ϐ��Ȃ�΁C$(\lambda x.M)$�͋[�^�t�����_���ł���D
\item $M$���[�^�t�����_���Ȃ�΁C$(\mb{A}M)^{\alpha}$�͋[�^�t�����_���ł���D
\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}

\bigskip

�[�^�t�����_����\�킷���^�ϐ��Ƃ��āC$M,N,P,Q,R...$��p���邱�Ƃɂ���D

�܂��C��`�ʂ�Ɍ^�t�����_���������ƁC���ʂ������Ȃ�C�ǂ݂ɂ����Ȃ�ꍇ������̂ŁC���ʂ�K���ɏȗ����邱�Ƃ�����D���̏ꍇ�C����Ȃ����ʂ́C������₤���Ƃɂ���D�Ⴆ�΁C$MNPQ$�́C$(((MN)P)Q)$��\���D

\bigskip

�[�^�t�����_���Ɋ܂܂�Ă��郉���_�ϐ��̂����C���R�ϐ��ł�����̂����ׂďW�߂Ă����W��$FV(M)$�C�����ϐ��ł�����̂����ׂďW�߂Ă����W��$BV(M)$�C����у����_�ϐ������ׂďW�߂Ă����W��$V(M)$���`����D

\begin{df}(�[�^�t�����_���̎��R�����_�ϐ�)\\
�[�^�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�����_���̑��������_�ϐ�)\\
�[�^�t�����_��$M$�ɂ��āC$M$�̑��������_�ϐ��̏W��$BV(M)$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\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}

\bigskip

�[�^�t�����_��$M$�ɑ΂��C$V(M) = FV(M) \cup BV(M)$�ƒ�`����D

\bigskip

\begin{df}
�[�^�t�����_��$M$�ɑ΂��C�ϐ�$MLV(M)$���ȉ��̂悤�ɒ�`����D
\begin{enumerate}
\item $MLV(x) \equiv x$
\item $MLV((PQ)) = MLV(P)$
\item $MLV((\lambda x.P)) = MLV(P)$
\item $MLV((AP)^{\alpha}) = MLV(P)$
\item $MLV((\mb{J}^{u}_{v}P)) = MLV(P)$
\item $MLV((\mb{F}^{t}P)) = MLV(P)$
\end{enumerate}
\end{df}
\bigskip

�^�t�����_���̒�`�Ɉڂ�D

�Ȃ��C���ꂩ���`����^�t�����_���́C�[�^�t�����_���ł���C�[�^�t�����_���͌^�����Ƃ͌���Ȃ����C�^�t�����_���͕K���^�����D

�ȉ��C�u$M$���^�t�����_���ŁC$Type(M) \equiv \alpha$�ł���v�Ƃ������Ƃ��C
$$M: \alpha$$
�Ɨ��L����D�܂��C�u$P_{1}$���C$P_{2}$����...����$P_{n}$�Ȃ�΁C$Q$�ł���v�Ƃ������Ƃ�
$$\infer{Q}{P_{1} & ... & P_{n}}$$
�Ɨ��L����D

\bigskip

\begin{df}($[t/u]$�̒�`)\\
$[ \ / \ ]$���C�_�����̏W������_�����̏W���ւ̎ʑ��ŁC�ȉ��̐����𖞂������̂ƒ�`����D
\begin{enumerate}
\item $V(t) \cap BV(\alpha) = \phi$�Ȃ�΁C$[t/u]\alpha \equiv \{ t/u \} \alpha$
\item $\alpha \equiv_\alpha \beta$����$V(t) \cap BV(\beta) = \phi$�Ȃ�΁C$[t/u]\alpha \equiv_\alpha \{ t/u \} \beta$
\end{enumerate}
\end{df}
�Ȃ��C����1�́C�藝\ref{sec: dainyuu2}��C�藝\ref{sec: dainyuu1}�̏ؖ��ŗ��p����Ă���D
�܂��C����2�́C�藝\ref{sec: existN}�́C�ؖ��ŁC$M$�������K���ɂ�蓾��ꂽ���́C(c)�̃P�[�X�̏ꍇ�ɗp�����Ă���D

\bigskip

\begin{df}(�^�t�����_���̑̌n)\\
\label{sec: def_of_lambda_term}
�^�t�����_������сC�^�t�����_���̌^$Type$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
	\begin{enumerate}
	\item �^�C�v$\alpha$�̃����_�ϐ�$x$�́C�^�t�����_����$Type(x) \equiv \alpha $
	\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 Type(FV(M)) \cup V(\forall u \alpha)}$$
	\item  $$\infer{(\mb{F}^{t}M): [t/v]\alpha}{M: \forall v \alpha} $$
	\end{enumerate}
�ȏ�̋K���ɂ���č��ꂽ�����_�����^�t�����_���ƒ�`����D�������C$V = \{ x_{1}, ... , x_{n} \}$�̎��C$Type(V) = \{ Type(x_{1}), ... , Type(x_{n}) \}$ �ƒ�߂�D
\end{df}

\bigskip

���ɁC�^�t�����_���Ɋ܂܂�Ă���̕ϐ��̂����C���R�ϐ��ł�����̂����ׂďW�߂Ă����W��$FIV(M)$����сC�����ϐ��ł�����̂����ׂďW�߂Ă����W��$BIV(M)$���`����D

\bigskip

\begin{df}($FIV(M)$�̒�`) \\
�^�t�����_��$M$�ɑ΂��C$FIV(M)$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\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}($BIV(M)$�̒�`) \\
�^�t�����_��$M$�ɑ΂��C$BIV(M)$���ȉ��̂悤�ɋA�[�I�ɒ�`����D
\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}

\bigskip

$IV(M) = FIV(M) \cup BIV(M)$�ƒ�`����D

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

\section{�����^�t�����_��}

\begin{df}(�����^�t�����_��)\\
�^�t�����_��$M$���C�����^�t�����_���ł���Ƃ́C$BIV(M) \cap FIV(M) = \phi$���������Ă��邱�Ƃ������D
\end{df}

�����^�t�����_���ւ̑���́C�u�̍��̎��R�̕ϐ��ւ̑���v�Ɓu�^�t�����_���̎��R�����_�ϐ��ւ̑���v��2��ނ̑�����`����D

�e�^�ɂ��āC���̌^�����悤�ȃ����_�ϐ����Z���݂��Ă��āC�����_�ϐ��͏��Ԃɕ���ł���C�Ƃ���D$x$���^$\alpha$��n�Ԗڂ̕ϐ��̎��C�^$\beta$��$n$�Ԗڂ̕ϐ����C$x^{\beta}$�Ƃ����D

\bigskip

\begin{df}($\{ t/u, Var \} M$�̒�`)\\
\label{sec: def_of_dainyuu M}
$t$���̍��C$u$���̕ϐ��C$Var$���̕ϐ��̏W���C$M$���^�t�����_���Ƃ���Ƃ��C$\{ t/u, Var \} M$���ȉ��̂悤�ɋA�[�I�ɒ�`����D�܂��C�ȉ��ł�$\{ t/u, Var \}$��$\{ t/u \}$�Ɨ��L����D
\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 $\{ a/u \} (\mb{J}^{w}_{v}N) \equiv (\mb{J}^{w}_{v} \{ a/v \} N)$ \ \ ($t$���ϐ�$a$�ŁC$a \not \in \{ u,v,w \} \cup IV(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 Var \cup \{ u,v,w \}$�ƂȂ�ŏ��̌̕ϐ�).
\end{enumerate}
\end{df}

\begin{df}(�^�t�����_���̃����_�ϐ��ւ̑��$[N/x, Var]M$�̒�`)\\
$N,M$���^�t�����_���C$x$�������_�ϐ��C$Var$���̕ϐ��̏W���Ƃ���D$Type(N) \equiv Type(x)$�̎��C$[N/x,Var]M$���ȉ��̂悤�ɒ�`����D�܂��C�ȉ��ł�$[N/x, Var]$��$[N/x]$�Ɨ��L����D
\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 \}$�ƂȂ�悤�ȍŏ��̌̕ϐ��Ƃ���),
\item $[N/x](\mb{F}^{t}P) \equiv (\mb{F}^{t}[N/x]P)$.
\end{enumerate}
\end{df}

\bigskip

��`\ref{sec: def_of_reduction}�ŁC�����^�t�����_���̃��_�N�V�������`���邪�C���_�N�V�����������ʂ������^�t�����_���ɂȂ��Ă��邱�Ƃ��ؖ����邽�߂ɕK�v�Ȃ̂��C���̒藝\ref{sec: dainyuu2}��\ref{sec: dainyuu1}�ł���D

\bigskip

\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�����_���̃��_�N�V����}

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

\mb{F}^{t}(\mb{J}^{u}_{v}M) & \rhd_{1} & \{ t/u \} 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}.
$$
�������C$\mb{F}^{t}(\mb{J}^{u}_{v}M) \rhd_{1} \{ t/u \} M$�̎��C$Var$�͌̕ϐ��̗L���W���ŁC$BIV(M) \subseteq Var$�𖞂������̂�I�ԁD\\
�̌n�� $1\beta$ �� $M \rhd_{1} N$ ���ؖ��ł���Ƃ��C$M \rhd_{1 \beta} N$ �Ƃ����D
\end{df}

\bigskip

$M$����0��ȏ�̃��_�N�V�������s����$N$�������鎞�C$M \rhd_\beta N$�ƒ�`����D
�܂��C$M \rhd_{1\beta}N$ �ƂȂ�悤��$N$�����݂��Ȃ����C$M$�͐��K�`�ł���C�Ƃ����D
$M \rhd_\beta N$���C$N$�����K�`�̎��C$N$��$M$�̐��K�`�ł���C�Ƃ����D
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\bigskip

\begin{thm}
\label{sec: reduction1}
$M$�������^�t�����_����$M \rhd_{1 \beta} N$�Ȃ�΁C$N$�͋����^�t�����_���ł���D
\end{thm}

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

\bigskip

\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���C$\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} N$�Ȃ�΁C$FV(M) \supseteq FV(N)$
\end{lem}
\end{proof}

\begin{df}(redex��degree)\\
�^�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�̂��Ƃ������D
\end{df}

\bigskip

\begin{thm}(�����^�t�����_���̐��K���藝)
\label{sec: normalization}
$M$�������^�t�����_���Ȃ�΁C$M$�̐��K�`�����݂���D
\end{thm}

\bigskip

\begin{proof}
�^�t�����_���Ɋ܂܂��redex��degree�ōő�̂��̂�$l$�C���̂悤��redex�̌���$n$�Ƃ���D
$l$��$n$�Ɋւ���2�d�A�[�@�Ŏ����D

\bigskip

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

\bigskip

$(\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{���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}

\bigskip

\begin{df}($l(\alpha)$�̒�`)\\
�_����$\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}

\bigskip

\begin{df}($l(M)$�̒�`)\\
�^�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}

\bigskip

�Ȃ��C�^�t�����_��$M$�ɂ��āC$l(M)$�͎��R���ɂȂ�D���̂��Ƃ������ɂ́C
$$l(M) \geq l(Type(M))$$
�������Ώ\���ł��邪�C�����$M$�̍\���ɂ��A�[�@�ŗe�ՂɎ�����D

\bigskip

\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

\bigskip
	\item $M$�������K���ɂ���ē���ꂽ���D\\
		
	\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 = 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)$��		��������D�܂��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 '$�́C$\{ \alpha_{1}, .. ,\alpha_{n} \}$�Ɋ܂܂�C$\alpha ' \equiv_{\alpha} Type(x)$�ł���悤�Ȃ��̂�I�ԁD
	
\bigskip

		\item �ϐ�$MLV(M)$��$\bot$�̏����K�����g���Ă��鎞�D\\
		���̕�����$(\mb{A}x)^{\alpha}$�ƂȂ��Ă���Ƃ���D\\
		�ϐ�$z$���C$xM$�Ɍ��ꂸ�C$Type(z) \equiv \beta$�ƂȂ�悤�ȕϐ�$z$�Ƃ���D
		�^�t�����_��$C$���C$M \equiv [\mb{A}x/z]C$�Ƃ����C$z = MLV(C)$�ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$l((\mb{A}x)^{\alpha}) = l(x) + 2l(\alpha) - 1 = 2l(\alpha)+1$\\
		$l(z) = 2l(\alpha)$\\
		���C$l((\mb{A}x)^{\alpha}) > l(z)$�ł���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$�́C		$N_{1}$�ł�$z^{\alpha '}$�ɒu��������Ă����Ƃ���D\\
		$N$�Ƃ��āC$[(\mb{A}x)^{\alpha '}/z^{\alpha '}]N_{1}$��I�ׂ΂悢�D�������C$\alpha$�́C$N$���^�t�����_���ɂȂ�悤�Ȃ��̂�I��($FV(N)$�Ɉˑ����Ē�܂�)�D

\bigskip

		\item �ϐ�$MLV(M)$��$\forall$�̏����K�����g���Ă��鎞�D\\
		���̕�����$\mb{F}^{t}x$�ƂȂ��Ă���Ƃ���D$Type(x) \equiv \forall u \alpha$�Ƃ�����D
		�ϐ�$z$���C$xM$�Ɍ��ꂸ�C$Type(z) \equiv \beta$�ƂȂ�悤�ȕϐ�$z$�Ƃ���D
		�^�t�����_��$C$���C$M \equiv [\mb{F}^{t}x/z]C$�Ƃ����C$z = MLV(C)$�ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$l(\mb{F}^{t}x) = 2l(\forall u \alpha) - 1 = 2l(\alpha) + 1$\\
		$l(z) = 2l(\alpha)$\\
		�ł���D���̑��̕����ł́C$B$��$C$�͓���ł���̂ŁC$l(M) > l(C)$����������D����āC$C		$�ɋA�[�@�̉��肪�K�p�\�ł���D\\
		$C$�ɋA�[�@�̉����K�p���ē���ꂽ����$N_{1}$�Ƃ���D�܂��C$C$�Ɋ܂܂�Ă���$z$�́C		$N_{1}$�ł�$z^{[t/u]\beta}$�ɒu��������Ă���D\\
		$N$�Ƃ��āC$[\mb{F}^{t}x^{\beta}/z^{[t/u]\beta}]N_{1}$��I�ׂ΂悢�D�������C$\beta$��$\{ \alpha_{1}, .. ,\alpha_{n} \}$�Ɋ܂܂�C$\beta \equiv_{\alpha} Type(x)$�ł���悤�Ȃ��̂�I�ԁD

\bigskip
		
		\end{enumerate}
	\end{enumerate}

\bigskip

\bigskip

\item $Type(M) = \alpha \to \beta$�̎��D\\
	$\delta = \alpha ' \to \beta '$�Ƃ����D
	\begin{enumerate}
	\item $\to$�̓����K���ɂ�蓾��ꂽ���D
		$$\infer{\lambda x.P: \alpha \to \beta}{P: \beta}$$
		$l(P) < l(\lambda x.P)$���C$P$�ɋA�[�@�̉��肪�K�p�ł���D
		$P$�ɋA�[�@�̉����K�p���ē���ꂽ�����C$N_{1}$�Ƃ���D\\
		$\delta_{1}$�Ƃ��āC$\beta '$��I�сC$N = \lambda x^{\alpha '}.N_{1}$�Ƃ���΂悢�D

\bigskip

	\item �����K���ɂ�蓾��ꂽ�C�܂���$M$���ϐ��̎��D\\
		���̂悤�ȏؖ��}���l����D
		$$\infer{Mx: \beta}{\deduce{M: \alpha \to \beta}{\Pi} & x: \alpha}$$
		$l(M) > l(Mx)$���C$Mx$�ɋA�[�@�̉��肪�K�p�\�ł���D
		$Mx$�ɋA�[�@�̉����K�p���ē���ꂽ����$N_{1}$�Ƃ���D\\
		$delta_{1}$�Ƃ��āC$\beta '$��I�сC$N = \lambda x^{\alpha '}.N_{1}$�Ƃ���΂悢�D
	\end{enumerate}

\bigskip

\bigskip

\item $Type(M) = \forall u \alpha$�̎��D\\
	$\delta = \forall w \beta$�Ƃ����D$\alpha$���l�̒�`���C$\{ a/u \} \alpha \equiv_{\alpha} \{ a/w \} \beta$����������D�������C$a$��new�Ȍ̕ϐ��D
	\begin{enumerate}
	\item $\forall$�̓����K���ɂ�蓾��ꂽ���D
		$$\infer{\mb{J}^{u}_{v}P: \forall u \alpha}{P: \{ v/u \} \alpha}$$
		$l(\mb{J}^{u}_{v}P) > l(P)$���C$P$�ɋA�[�@�̉��肪�K�p�ł���D
		$P$�ɋA�[�@�̉����K�p���ē���ꂽ����$N_{1}$�Ƃ���D\\
		$\delta_{1}$�Ƃ��āC$ \{ a/w \} \beta$���Ƃ�C$N = \mb{J}^{w}_{a}N_{1}$�Ƃ���΂悢�D
		$$\infer{\mb{J}^{w}_{a}N_{1}: \forall w \beta}{N_{1}: \{ a/w \} \beta}$$	

\bigskip

	\item �����K���ɂ�蓾��ꂽ�C�܂���$M$���ϐ��̎��D\\
		���̂悤�ȏؖ��}���l����D
		$$\infer{\mb{F}^{a}P: [a/u]\alpha}{\deduce{P: \forall u \alpha}{\Pi}}$$
		$a$��new�Ȃ̂ŁC$[a/u]\alpha \equiv \{ a/u \}\alpha$�ł���D
		$l(P) > l(\mb{F}^{a}P)$���C$\mb{F}^{a}P$�ɋA�[�@�̉��肪�K�p�ł���D
		$\mb{F}^{a}P$�ɋA�[�@�̉����K�p���ē���ꂽ����$N_{1}$�Ƃ���D\\
		$\delta_{1}$�Ƃ��āC $ \{ a/w \} \beta$���Ƃ�C$N = \mb{J}^{w}_{a}N_{1}$�Ƃ���΂悢�D
		$$\infer{\mb{J}^{w}_{a}N_{1}: \forall w \beta}{N_{1}: \{ a/w \} \beta}$$
	\end{enumerate}
\end{itemize}
\end{proof}

\bigskip

\begin{df}(�ϊ�$T(V,\alpha)$)\\
�̕ϐ��̏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)$)\\
�̕ϐ��̏W��$V$,����ь^�t�����_��$M$�ɂ��āC�^�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}

\bigskip

��`��薾�炩�ɁC�^�t�����_��$M$�ɂ��āC$V \cap BIV(T(V,M)) = \phi$����������D

\bigskip

\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}) \} $
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{$LJ$��cut�����藝}
���K�`�藝�̗��p��Ƃ��āC�Q���c�F�����̒��ώ�`�q��_���̑̌n$LJ$��$cut$�����藝�������D\\
$LJ$�Ƃ��Ĉȉ��̑̌n���̗p����D�Ȃ��C$LJ$�͐��m�ɂ́C$LJ$��$\{ \to, \forall, \bot \} $-�f�Ђł���D

\begin{df}($LJ$�̒�`)

(�����^)
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot & \rightarrow & \alpha
\end{array} \]

\bigskip

(���_�K��)

\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 u \alpha, \Gamma \rightarrow \gamma}
		{[ t/u ] \alpha, \Gamma \rightarrow \gamma}
	\ \ \ \ \ \ \ \ \ \ 
	\infer[(\rightarrow \forall)]
		{\Gamma \rightarrow \forall u \alpha}
		{\Gamma \rightarrow [ v/u ] \alpha}
	$$
\end{description}
\end{description}
%�����S�Ă̐��_�K���ɂ����� $\Theta$ �͈�̘_��������Ȃ邩��񂩂ł���.
���_�K��{$(\rightarrow  \forall)$} �ɂ����ẮC �ϐ� $v$ �͐��_�K���̉����ɂ�
���R�Ɍ���Ȃ����̂Ƃ���D

\end{df}

\bigskip

\begin{thm}
$M$�����K�Ȍ^�t�����_���Ȃ�΁C$LJ$�ŁC$Type(FV(M)) \rightarrow Type(M)$��cut�Ȃ��ŏؖ��\�ł���D
\end{thm}

\begin{proof}
$M$�̒����Ɋւ���A�[�@�Ŏ����D\\
\begin{itemize}
\item ������1�̎��D\\
	$M$���ϐ�$x$�̎��́C$Type(FV(M)) = \{ Type(x) \}$�@���C����$(I)$����cut�Ȃ��ŏؖ��\�ł���D

\bigskip

\bigskip

\item ������2�ȏ�̎��D\\
\begin{enumerate}
\item �Ō�Ɏg��ꂽ�K����$\to$�̓����K���̎��D
	$$\infer{\lambda x.P: \alpha \to \beta}{P: \beta & x: \alpha}$$
	�A�[�@�̉�����C$LJ$�ŁC
	$$Type(FV(\lambda x.P)), \alpha \rightarrow \beta$$
	��cut�Ȃ��ŏؖ��\�ł���D����āC���_�K��$(\rightarrow \to)$��K�p�����
	$$Type(FV(\lambda x.P)) \rightarrow \alpha \to \beta$$
	��$LJ$��cut�Ȃ��ŏؖ��\�ł���D

\bigskip

\item �Ō�Ɏg��ꂽ�K����$\forall$�̓����K���̎��D
	$$\infer{\mb{J}^{u}_{v}P: \forall u \alpha}{P: \{ v/u \} \alpha}$$
	�A�[�@�̉�����C$LJ$�ŁC
	$$Type(FV(P)) \rightarrow \{ v/u \} \alpha$$
	��cut�Ȃ��ŏؖ��\�ł���D$Type(FV(P)) = Type(FV(\mb{J}^{u}_{v}P))$���C���_�K��$(\rightarrow \forall)$��K�p�����
	$$Type(FV(\mb{J}^{u}_{v}P)) \rightarrow \forall u \alpha$$
	��$LJ$��cut�Ȃ��ŏؖ��\�ł���D

\bigskip

\item �Ō�Ɏg��ꂽ�K���������K���̎��D
	\begin{enumerate}

	\item �ϐ�$MLV(M)$��Application�̋K�����g���Ă���ꍇ�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 = MLV(C)$�ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$R$�ɋA�[�@�̉����K�p����ƁC$LJ$�ŁC$Type(FV(R)) \rightarrow \alpha$��cut�Ȃ��ŏؖ��\�ł���D\\
�܂��C$C$�ɋA�[�@�̉����K�p����ƁC$LJ$�ŁC$\Sigma , \beta \rightarrow Type(M)$��cut�Ȃ��ŏؖ��\�ł���D�������C$\Sigma \cup \beta = Type(FV(C))$�Ƃ��Ă���D\\
�����ŁC$Type(FV(R))$�����$\Sigma$�Ɍ����_�����́C���ׂ�$Type(FV(M))$�Ɋ܂܂�Ă���D\\
����āC�K��$(\to \rightarrow)$�ɂ��C$LJ$�ŁC$\alpha \to \beta, \Sigma, Type(FV(R)) \rightarrow Type(FV(M))$��cut�Ȃ��ŏؖ��\�ł���D�_����$\alpha \to \beta$�́C$Type(FV(M))$�Ɋ܂܂��̂ŁC���_�K��$(e \rightarrow), (c \rightarrow), (w \rightarrow)$�����񂩎g���΁C$Type(FV(M)) \rightarrow Type(M)$��$LJ$��cut�Ȃ��ŏؖ��\�ł���D

\bigskip

	\item �ϐ�$MLV(M)$��$\bot$�̏����K�����g���Ă���ꍇ�D\\
		����(N)����C$\bot \rightarrow Type(M)$��$LJ$�ŏؖ��ł���D$\bot \in Type(FV(M))$���C���_�K��$(e \rightarrow), (w \rightarrow)$�����񂩎g���΁C$Type(FV(M)) \rightarrow Type(M)$��$LJ$��cut�Ȃ��ŏؖ��\�ł���D

\bigskip

	\item �ϐ�$MLV(M)$��$\forall$�̏����K�����g���Ă���ꍇ�D\\
		���̕�����$\mb{F}^{t}x$�ƂȂ��Ă���Ƃ���D$Type(x) = \forall u \beta$�Ƃ�����D\\
		�ϐ�$z$���C$xM$�Ɍ��ꂸ�C$Type(z) \equiv [t/u]\beta$�ƂȂ�悤�ȕϐ�$z$�Ƃ���D
		�^�t�����_��$C$���C$M \equiv [\mb{F}^{t}x/z]C$�Ƃ����C$z = MLV(C)$�ƂȂ�悤�Ȍ^�t�����_���Ƃ���D\\
		$C$�ɋA�[�@�̉����K�p����ƁC$\Sigma, [t/u]\beta \rightarrow Type(M)$��$LJ$��cut�Ȃ��ŏؖ��\�ł���D�����ŁC$\Sigma$ �Ɍ����_�����͂��ׂ�$Type(FV(M))$�Ɋ܂܂�Ă���D\\
����āC�K��$(\forall \rightarrow)$�ɂ��C$LJ$�ŁC$\forall u \beta, \Sigma \rightarrow Type(M)$���ؖ��\�ł���D�_����$\forall u \beta$�́C$Type(FV(M))$�Ɋ܂܂��̂ŁC���_�K��$(e \rightarrow), (w \rightarrow)$�����񂩎g���΁C$Type(FV(M)) \rightarrow Type(M)$��$LJ$��cut�Ȃ��ŏؖ��\�ł���D
\end{enumerate}

\end{enumerate}
\end{itemize}
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�ӎ�}
�{�_���̍쐬�ɂ�����C�w�������̌ÐX�搶�C�ÐX�������̊F�l�C��t��w��w�@���w�����Ȃ̍���M���搶�C���c �[�搶�C�V����w����w���̍��쓹�v�搶�C����ѓ����H�Ƒ�w��w�@��񗝍H�w�����Ȃ̎������搶�ɑ���Ȃ����͂𒸂��܂������Ƃ�S���犴�ӂ������܂��D

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

%% �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 Gerhard Gentzen. 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}
