\documentclass[a4r]{jarticle}
\usepackage{latexsym,amssymb,amsthm,proof}
%\pagestyle{plain}

% \input{define.tex}
\newtheorem{df}{���}[section]
\newtheorem{thm}[df]{����}
\newtheorem{cor}[df]{��}
\newtheorem{lemma}[df]{����}

\def\equivdef{\equiv_{def}}
\def\equalbe{\ \ =_{\beta \eta}\ \ }
\def\BCKbe{BCK\beta \eta}
\def\Eqbe{\beta \eta}
\def\verifyonnj{\ \ \vdash_{NJ}\ \ }
\def\verifyonbck{\ \ \vdash_{\beta \eta}\ \ }
\def\Lra{\ \ \Longrightarrow\ \ }
\def\Lla{\ \ \Longleftarrow\ \ }
\def\Llra{\ \ \Longleftrightarrow\ \ }
\def\fvsets#1#2#3{i#1_{#2}, \dots, i#1_{#3}}
\def\varsets#1#2#3{#1_{#2}, \dots, #1_{#3}}
\def\triquad{\qquad\qquad\qquad}
\def\circed#1{#1^{\circ}}

\begin{document}

\bibliographystyle{jplain}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\thispagestyle{empty}
\vspace*{1cm}
\begin{center}
{\Large ���������ر��������ʳظ����}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf ľ�Ѽ���Ҹ����������η� BCK$\beta\eta$ �ؤ�����������}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ʿ��16ǯ10��28��}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ���ء���������� �칶}
\end{center}

\vspace*{5mm}
\begin{center}
{\Large ��ƣ����}
\end{center}

\setcounter{page}{0}

\newpage


\section{�η� $\BCKbe$}

$\lambda$-term �� $\Xi$ ��ä����ηϤǤ��� $\BCKbe$ �ϰʲ��Τ褦���������롣 

\begin{df} ($\lambda$-term)
\[
\begin{array}{rl}
�� & �����ѿ�������� term �Ǥ��롣 \\
�� & \alpha, \beta �� term �ʤ�� (\alpha\beta) �� term �Ǥ��롣 \\
�� & \alpha �� term �ʤ�� (\lambda x.\alpha) �� term �Ǥ��롣 \\
\end{array}
\]
\end{df}

\begin{df} ($\beta \eta$-equality) 
\[
\begin{array}{rcll}
\alpha & \equalbe & \alpha \\
\lambda x.\alpha & \equalbe & \lambda y .[y/x]\alpha & (y �� \alpha �˼�ͳ�˸���ʤ�) \\ 
(\lambda x.\alpha)\beta & \equalbe & [\beta/x]\alpha \\
\lambda x.\alpha x & \equalbe & \alpha & (x �� \alpha �˼�ͳ�˸���ʤ�) \\
\alpha \equalbe \beta & \Lra & \gamma\alpha \equalbe \gamma\beta \\ 
\alpha \equalbe \beta & \Lra & \alpha\gamma \equalbe \beta\gamma \\ 
\alpha \equalbe \beta & \Lra & \lambda x.\alpha \equalbe \lambda x.\beta \\ 
\alpha \equalbe \beta, \qquad \beta \equalbe \gamma & \Lra & \alpha \equalbe \gamma \\
\alpha \equalbe \beta & \Lra & \beta \equalbe \alpha \\
\end{array}
\]
\end{df}

\bigskip

�η� $\BCKbe$ ���������� $\lambda$-term �Τ��ȤǤ��ꡢ
�Ļ��Ĥ������ޤ�, ������ˤϡ�$\Xi, i, c$�פ����롣
�η� $\BCKbe$ �ο�����§�ϼ��� 3 �ĤȤʤ롣
�ޤ������٤���Ȥ��벾��Ϲ⡹1�ĤǤ��롣 ���ʤ�������� $k$ �Ϲ⡹1����ˤ��������ʤ���

\bigskip

�� $\Xi$ introduction ($\Xi$i)
\nobreak
$$ \infer[k(\Xi i)]{\Xi \alpha\beta}{\deduce{\beta x}{\deduce{\displaystyle \Sigma}{\deduce{\alpha x}{k}}}} $$
\triquad $x$ �� $\alpha, \beta$ �ڤ�����Ƥ��ʤ�����˼�ͳ�˸���ʤ���

\bigskip

�� $\Xi$ elimination ($\Xi$e)
\nobreak
$$ \infer[(\Xi e)]{\beta \gamma}{\deduce{\Xi \alpha \beta}{\displaystyle \Sigma_1} & \deduce{\alpha \gamma}{\displaystyle \Sigma_2}} $$

�� $equality (\Eqbe)$
\nobreak
$$ \infer[(\Eqbe)]{\beta}{\deduce{\alpha}{\displaystyle \Sigma}} \qquad if \qquad \alpha =_{\Eqbe} \beta $$

\bigskip

��$\Xi\alpha\beta$ ��ľ��Ū�ʰ�̣��
$\forall x(\alpha x\supset \beta x)$ �Ǥ��롣
�� $ix$�ΰ�̣��
$x$ �ϸ��ΤǤ���, �� $\alpha = !\alpha$ �ΰ�̣�� $\alpha$ ��̿��Ǥ���
 �Ǥ��롣

\bigskip

���θ����ɽ���Ϥ�˭����
¿�������������Ҹ줬��ά����Ȥ�������Ǥ��롣�ʲ��ˤ�ɬ�פʤ�Τ�������󤹤�

\bigskip

\[
\begin{array}{rll}
\alpha\supset\beta & \equiv & \Xi(\mbox{\bf K}\alpha)(\mbox{\bf K}\beta), \mbox{\ where {\bf K}}\equiv\lambda xy.x ;\\
\top & \equiv & \Xi i i ;\\
\forall x\alpha & \equiv & \Xi (\mbox{\bf K}\top)(\lambda x.\alpha) ;\\
\bot & \equiv & \forall x x ;\\
\alpha = \beta & \equiv & \Xi (\lambda x. x\alpha)(\lambda x. x\beta) ;\\
!\alpha & \equiv & \top = \alpha .
\end{array}
\]

\bigskip

\begin{thm}
�嵭�ξ�ά������Ѥ��ưʲ��ο�����§��������롣

�� Implication introduction ($\supset$ i)
\nobreak
$$ \infer[k(\supset i)]{\alpha \supset \beta}{\deduce{\beta}{\deduce{\displaystyle \Sigma} {\deduce{\alpha}{k}}}} $$


�� Implication elimination ($\supset$ e)
\nobreak
$$ \infer[(\supset e)]{\beta}{\deduce{\alpha \supset \beta}{\displaystyle \Sigma_1} & \deduce{\alpha}{\displaystyle \Sigma_2}} $$

�� Universal quantifier introduction ($\forall$ i)
\nobreak
$$ \infer[(\forall i)]{\forall x\alpha}{\deduce{\alpha}{\displaystyle \Sigma}} $$
\nobreak 
\triquad $x$ ������Ƥ��ʤ�����˼�ͳ�˸���ʤ���

\bigskip

�� Universal quantifier elimination ($\forall$ e)
\nobreak
$$ \infer[(\forall e)]{(\lambda x.\alpha)\beta}{\deduce{\forall x\alpha}{\displaystyle \Sigma}} $$

�� Ex falso quodibet (q)
\nobreak
$$ \infer[(q)]{\alpha}{\bot} $$

\bigskip

\end{thm}

\bigskip

\begin{proof}
($\supset$ i) �ˤĤ��ƾ������롣

$$
\infer[k (\Xi i)]{\Xi (K\alpha)(K\beta)}{
  \infer[(\Eqbe)]{K\beta x}{\deduce{\beta}{\deduce{\displaystyle \Sigma}{
      \infer[(\Eqbe)]{\alpha}{\deduce{K\alpha x}{k}}
      }}}
  }
$$

\end{proof}



�ޤ���$\alpha = \beta$�פˤĤ��Ƥϼ��ο�����§��������롣
\[
\infer[k\mbox{($=\supset$i)}]{(\alpha = \beta)\supset \gamma}{\infer*{\gamma}{\deduce{\alpha = \beta}{k}}} .
\]
������, ($=\supset$i) �ˤ����Ʋ���Ϥ����ĤǤ���Ȥ��롣

\bigskip

\begin{thm}\label{exclamationdeduction} $!\alpha$ �ˤĤ��ưʲ��ο�����§��������롣

�� ! elimination
\nobreak
$$ \infer[(!e)]{\alpha}{!\alpha} $$

�� ! implication introduction
\nobreak
$$ \infer[k(!\supset i)]{!\alpha \supset \beta}{\deduce{\beta}{\deduce{\Sigma}{\deduce{!\alpha}{k}}}}$$

\begin{center}
$(!\supset i)$ �ˤ����Ʋ���Ϥ����ĤǤ���Ȥ��롣
\end{center}


\bigskip

\end{thm}

$\Gamma$ ������������Ȥ����Ȥ���
$\Gamma$ �˴ޤޤ��������������Ƥ��ʤ�����Ȥ� $\alpha$ �˻�� $\BCKbe$ �ο����ޤ�����Ȥ�
$$
\Gamma \verifyonbck \alpha
$$
�Ƚ񤯡� ����ˤʤ��������� $\Gamma$ �˴ޤޤ�Ƥ��Ƥ�褤�� 
������ $\BCKbe$ �Ǥϡ����̤� $contraction$ �������ʤ��Τǡ�
Ʊ������򣲲�ʾ�Ȥä����ϡ������������� $\Gamma$ ����˻Ȥä�ʬ�����ޤޤ�Ƥ��롣

\bigskip

�ޤ� $\alpha$ �˴ޤޤ�뼫ͳ�ѿ����Τν���� $FV(\alpha)$ �Ȥ��롣 





\section{$NJ$ �� $\BCKbe$ �ؤ�������}

$NJ$ ������������ $\BCKbe$ ���������ؤ��Ѵ���ͤ���
$NJ$ �Ǿ�������������� $\alpha$ �˴ؤ��ơ� $\alpha$ ���Ѵ�������Τ� $\BCKbe$ �Ǿ�����ǽ�Ȥʤ뤳�Ȥ���
ľ�Ѽ������ $NJ$ �� $\BCKbe$ ��������뤳�Ȥ򼨤���

\bigskip

�ޤ��ϡ�
\begin{itemize}
\item �ؿ����椬 2 �ѿ��ؿ����� f �Τ�
\item �Ҹ쵭�椬 2 �ѿ��Ҹ쵭�� p �Τ�
\end{itemize}
����ʤ� $NJ$ �ˤĤ��ƹͤ��롣 

\bigskip

\begin{df}
$\BCKbe$ �ˤ����ưʲ������������¤٤���� $\Delta$ �Ȥ��롣

$$ \bot = !(\bot) $$
$$ ic $$
$$!(\forall x (ix = !(ix)))$$
$$!(\forall x \forall y (i(fxy)))$$
$$!(\forall x \forall y (pxy = !(pxy)))$$
$$!(\forall x \forall y (\forall z (xz = !(xz)) \supset \forall z (yz = !(yz)) \supset (\Xi x y) = !(\Xi x y)))$$

\end{df}

\bigskip

\begin{df}
$NJ$ �������� $\alpha$ ���� $\BCKbe$ �������� $\circed{\alpha}$ ��ʲ��Τ褦��������롣
\[
\begin{array}{rll}
\circed{\alpha} & \equivdef & \alpha \qquad if \qquad \alpha \ is \ atom. \\
\circed{(\alpha \supset \beta)} & \equivdef & \circed{\alpha} \supset \circed{\beta} \\
\circed{(\forall x \alpha)} & \equivdef & \Xi i (\lambda x. \circed{\alpha}) (= \forall x
 (ix \supset \circed{\alpha})).
\\
\end{array}
\]
\end{df}

\bigskip

\begin{lemma}\label{fvsets}
$$ FV(\circed{\alpha}) = FV(\alpha) $$
$$ FV(!\alpha) = FV(\alpha) $$
\end{lemma}

\begin{proof}
$\alpha$ ��Ĺ���˴ؤ��뵢Ǽˡ��
\end{proof}

\bigskip

\begin{lemma}\label{contractionhypothesis} (contraction)
$$ !\alpha,!\alpha, \Gamma \verifyonbck \beta $$
�ΤȤ���
$$ !\alpha, \Gamma \verifyonbck \beta $$
\end{lemma}

\begin{proof}
$ (=\supset i)$ �ˤ�롣
\end{proof}

\bigskip


\begin{lemma}\label{forallstar}
$$
[t/x]\circed{\alpha} \equalbe \circed{([t/x]\alpha)}
$$
\end{lemma}

\begin{proof}

$\alpha$ ��Ĺ���˴ؤ��뵢Ǽˡ��

\bigskip

�� $\alpha$ �� atom �ΤȤ�

\[
\begin{array}{rll}
[t/x]\circed{\alpha} & \equalbe & [t/x]\alpha \\
\circed{([t/x]\alpha)} & \equalbe & [t/x]\alpha \\
\end{array}
\]

\bigskip

�� $\alpha$ �� $\beta \supset \gamma$ �ΤȤ�

��Ǽˡ�β�����
\[
\begin{array}{rll}
\ [t/x]\circed{\beta} & \equalbe & \circed{([t/x]\beta)} \\
\ [t/x]\circed{\gamma} & \equalbe & \circed{([t/x]\gamma)} \\
\end{array}
\]
������
\[
\begin{array}{rll}
[t/x]\circed{\alpha} & \equalbe & [t/x]\circed{\beta} \supset [t/x]\circed{\gamma} \\
\circed{([t/x]\alpha)} & \equalbe & \circed{([t/x]\beta \supset [t/x]\gamma)} \\
                & \equalbe & \circed{([t/x]\beta)} \supset \circed{([t/x]\gamma)} \\
\end{array}
\]
���
$$ [t/x]\circed{\alpha} \equalbe \circed{([t/x]\alpha)} $$

\bigskip

�� $\alpha$ �� $\forall x\beta$ �ΤȤ�

\[
\begin{array}{rll}
[t/x]\circed{\alpha} & \equalbe & [t/x]\circed{(\forall x\beta)} \\
                & \equalbe & \circed{(\forall x\beta)} \\
\circed{([t/x]\alpha)} & \equalbe & \circed{([t/x](\forall x\beta))} \\
                & \equalbe & \circed{(\forall x\beta)} \\
\end{array}
\]

\bigskip

�� $\alpha$ �� $\forall y\beta, (y \ne x) $ �ΤȤ�

��Ǽˡ�β��꤫��
\[
\begin{array}{rll}
\ [z/y]\circed{\beta} & \equalbe &  \circed{([z/y]\beta)}\\
\ [t/x]\circed{([z/y]\beta)} & \equalbe & \circed{([t/x][z/y]\beta)}\\
\end{array}
\]
������ z �� new-variable��\\
�Ĥޤ�
\[
\begin{array}{rllll}
\ [t/x][z/y]\circed{\beta} & \equalbe \circed{([t/x][z/y]\beta)} \\
\end{array}
\]

������
\[
\begin{array}{rll}
\ [t/x]\circed{\alpha} & \equalbe & [t/x](\Xi i(\lambda y.\circed{\alpha}))\\
                     & \equalbe & [t/x](\Xi i(\lambda z.[z/y]\circed{\beta}))\\
                     & \equalbe &\Xi i(\lambda z.[t/x][z/y]\circed{\beta})\\

\ \circed{([t/x]\alpha)} & \equalbe & \circed{([t/x](\forall z[z/y]\beta))}\\
                     & \equalbe & \circed{(\forall z[t/x][z/y]\beta)}\\
                     & \equalbe & \Xi i(\lambda z.\circed{([t/x][z/y]\beta)})\\
\end{array}
\]

���

$$ [t/x]\circed{\alpha} \equalbe \circed{([t/x]\alpha)} $$

\end{proof}

\bigskip




\begin{thm}\label{exclamation}
$NJ$ �������� $\alpha$ �˴ؤ��ơ�
$$ \Delta   \verifyonbck \circed{\alpha} = !(\circed{\alpha}) $$

\begin{proof}

$\alpha$ ��Ĺ���˴ؤ��뵢Ǽˡ��

\bigskip

�� $\alpha �� \bot$ �ΤȤ�

$\Delta$ �˴ޤޤ�Ƥ���Τǡ�������

\bigskip

�� $\alpha$ �� atom �ΤȤ�

$\alpha \ \ \equiv \ \ \circed{\alpha} \ \ \equiv \ \ pt_1t_2$ �Ȥʤ롣

���ΤȤ�
$$
\infer=[(!e)(\forall e)]{pt_1t_2=!(pt_1t_2)}{!(\forall x \forall y(pxy = !(pxy)))}
$$

�� $\alpha \ \ \equiv \ \ \beta \supset \gamma$ �ΤȤ�

��Ǽˡ�β�����

\[
\begin{array}{rll}
\Delta & \verifyonbck & \circed{\beta} = !(\circed{\beta}) \\
\Delta & \verifyonbck & \circed{\gamma} = !(\circed{\gamma}) \\
\end{array}
\]
�Ǥ��롣

��ä�

$$
\infer[(\Eqbe)]{\forall z(\circed{\beta} = !(\circed{\beta})) \supset \forall z(\circed{\gamma} = !(\circed{\gamma})) \supset (\circed{\beta} \supset \circed{\gamma}) = !(\circed{\beta} \supset \circed{\gamma})}{
  \infer[(!e)(\forall e)]{\forall z(K\circed{\beta}z = !(K\circed{\beta}z)) \supset \forall z(K\circed{\gamma}z = !(K\circed{\gamma}z)) \supset \Xi(K\circed{\beta})(K\circed{\gamma}) = !(\Xi(K\circed{\beta})(K\circed{\gamma}))}{
    !(\forall x \forall y (\forall z (xz = !(xz)) \supset \forall z (yz = !(yz)) \supset (\Xi x y) = !(\Xi x y)))}
  }
$$

����� $\Pi$ �Ȥ��롣

$$
\infer[(\supset e)]{\circed{\beta} \supset \circed{\gamma} = !(\circed{\beta}  \supset \circed{\gamma})}{
  \infer[(\supset e)]{\forall z(\circed{\gamma} = !(\circed{\gamma})) \supset (\circed{\beta} \supset \circed{\gamma}) = !(\circed{\beta} \supset \circed{\gamma})}{
    \deduce{\forall z(\circed{\beta} = !(\circed{\beta})) \supset \forall z(\circed{\gamma} = !(\circed{\gamma})) \supset  (\circed{\beta} \supset \circed{\gamma}) = !(\circed{\beta} \supset \circed{\gamma})}{\Pi} & {\forall z (\circed{\beta} = !(\circed{\beta}))}
    }
  & {\forall z (\circed{\gamma} = !(\circed{\gamma}))}
  }
$$

\bigskip

�� $\alpha \equiv \forall x \beta$ �ΤȤ�


��Ǽˡ�β�����

$$ \Delta  \verifyonbck  \circed{([u/x]\beta)} = !\circed{([u/x]\beta)} $$

�����ǡ�����\ref{forallstar}���


$$ [u/x]\circed{\beta} =_{\Eqbe} \circed{([u/x]\beta)} $$
$$ ![u/x]\circed{\beta} =_{\Eqbe} !\circed{([u/x]\beta)} $$


�Ǥ��롣

��ä�
$$
\infer[(\Eqbe)]{\forall z ([z/x]\circed{\beta} = !([z/x]\circed{\beta})) \supset (\circed{\forall x \beta}) = !(\circed{\forall x \beta})}{
  \infer[(\supset e)]{\forall z((\lambda x.\circed{\beta})z = !((\lambda x.\circed{\beta})z)) \supset \Xi i(\lambda x. \circed{\beta}) = !(\Xi i(\lambda x. \circed{\beta}))}{
    \infer[(!e)(\forall e)]{\forall z(iz = !(iz)) \supset \forall z((\lambda x.\circed{\beta})z = !((\lambda x.\circed{\beta})z)) \supset \Xi i(\lambda x. \circed{\beta}) = !(\Xi i(\lambda x. \circed{\beta}))}{
      !(\forall x \forall y (\forall z (xz = !(xz)) \supset \forall z (yz = !(yz)) \supset (\Xi x y) = !(\Xi x y)))}
    & {\forall z(iz = !(iz))}
    }
  }
$$

����� $\Pi$ �Ȥ��롣

$$
\infer[(\supset e)]{\circed{(\forall x\beta)} = !\circed{(\forall x\beta)}}{
  \deduce{\forall z([z/x]\circed{\beta} = !([z/x]\circed{\beta})) \supset \circed{(\forall x\beta)} = !\circed{(\forall x\beta)}}{\Pi}
  & \infer[(\forall i)]{\forall z([z/x]\circed{\beta} = !([z/x]\circed{\beta}))}{
      \infer[(\Eqbe)]{[z/x]\circed{\beta} = !([z/x]\circed{\beta})}{
	\circed{([z/x]\beta)} = !\circed{([z/x]\beta)}}
      }
  }
$$

\end{proof}

\end{thm}

\bigskip

����\ref{exclamation} ������ \ref{contractionhypothesis} ��
�Ѥ���Ȱʲ������꤬�����Ǥ��롣

\bigskip

\begin{lemma}\label{contractionhypothesis2} (contraction2)
$$ \Delta,\circed{\alpha},\circed{\alpha}, \Gamma \verifyonbck \beta $$
�ΤȤ���
$$ \Delta,\circed{\alpha}, \Gamma \verifyonbck \beta $$
\end{lemma}

\bigskip

\begin{thm}\label{njinbckeb}
$$ \Gamma \verifyonnj \alpha $$
�ΤȤ���$\varsets{x}{1}{n}$ ��Ŭ�����ѿ�����Ȥ����
$$ \Delta, \fvsets{x}{1}{n}, \circed{\Gamma} \verifyonbck \circed{\alpha} $$
������ $\circed{\Gamma}$ �� $\Gamma$ �˴ޤޤ�벾�� $\beta$ �˴ؤ��� $\circed{\beta}$ �Ȥ�����Ρ��ޤ��̾� $NJ$ �Ǥ�  $\Gamma$ �ˤϽ�ʣ�Ϥʤ��Τ�����
�����ǤϾ������ñ�ˤ��뤿�ᡢ$\Gamma$ �ˤϻȤä�ʬ�������꤬�ޤޤ�Ƥ����ΤȤ��롣
\end{thm}

\begin{proof}

$NJ$ �Ǥο����ޤ�Ĺ���˴ؤ��뵢Ǽˡ��

\bigskip

�� �����ޤ�Ĺ���� 1 �ΤȤ�

$\alpha$ �� $\Gamma$ �˴ޤޤ��Τ�
$$ \Gamma \verifyonnj \alpha $$
���
$$ \circed{\Gamma} \verifyonbck \circed{\alpha}$$

��ä�
$$ \Delta, \fvsets{x}{1}{n}, \circed{\Gamma} \verifyonbck \circed{\alpha} $$

\bigskip

�� NJ �ǺǸ�ο�����§�� $(\supset e)$ �ΤȤ�
$$
\infer[(\supset e)]{\alpha}{\beta \supset \alpha & \beta}
$$
�ȤʤäƤ��롣���ΤȤ���Ǽˡ�β�����
\[
\begin{array}{rll}
\Delta, \fvsets{x}{1}{m}, \circed{\Gamma_1} & \verifyonbck & \circed{(\beta \supset \alpha)} \\
\Delta, \fvsets{y}{1}{l}, \circed{\Gamma_2} & \verifyonbck & \circed{\beta} \\
\end{array}
\]
������ $\Gamma_1 , \Gamma_2$ ���¤٤���Τ� $\Gamma$ \\
�������ä�

\[
\begin{array}{rll}
\Delta, \fvsets{x}{1}{m}, \fvsets{y}{1}{l}, \circed{\Gamma_1}, \circed{\Gamma_2} & \verifyonbck & \circed{\alpha} \\
\end{array}
\]

\bigskip

�� NJ �ǺǸ�ο�����§�� $(\supset i)$ �ΤȤ�
$$
\infer[k(\supset i)]{\beta \supset \gamma}{
  \deduce{\gamma}{
    \deduce{\Pi}{
      \deduce{\beta}{k}
    }
  }
}
$$
�ȤʤäƤ��롣���ΤȤ���Ǽˡ�β�����
$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma},\circed{\beta}, \cdots ,\circed{\beta}  \verifyonbck \circed{\gamma} $$
��ä����� \ref{contractionhypothesis2} ���
$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma},\circed{\beta} \verifyonbck \circed{\gamma} $$
�������ä�
$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma} \verifyonbck \circed{\beta} \supset \circed{\gamma} $$

\bigskip

�� NJ �ǺǸ�ο�����§�� $(\forall i)$ �ΤȤ�
$$
\infer{\forall x\beta}{\beta}
$$
�ȤʤäƤ��롣 ($x$ ������Ƥ��ʤ�����˸���ʤ�)��\\
���ΤȤ���Ǽˡ�β�����
$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma} \verifyonbck \circed{\beta} $$
���� \ref{fvsets} ��� $\circed{\Gamma}$ �� $x$ �ϼ�ͳ�˸���ʤ��Τǡ�

$$
\infer[k (\Xi i)]{\Xi i(\lambda x.\circed{\beta})}{
  \infer[(\Eqbe)]{(\lambda x.\circed{\beta})x}{
    \deduce{\circed{\beta}}{\deduce{\Sigma}{\deduce{ix}{k}}}
    }
  }
$$

\bigskip

�� NJ �ǺǸ�ο�����§�� $(\forall e)$ �ΤȤ�
$$
\infer{[t/x]\beta}{\forall x\beta}
$$
�ȤʤäƤ��롣 ���ΤȤ���Ǽˡ�β�����

$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma} \verifyonbck \circed{(\forall x \beta)} $$
��ä�
$$
\infer[(\Eqbe)]{\circed{([t/x]\beta)}}{
  \infer[(\Eqbe)]{[t/x]\circed{\beta}}{
    \infer[(\Xi e)]{(\lambda x.\circed{\beta})t}{
      \Xi i(\lambda x.\circed{\beta}) & it}
    }
  }
$$

������ $t \equiv y$ ($y$ ���ѿ�)�ΤȤ��Ϻ��դ� $iy$ ��ä��Ƥ��Ф褤��\\
$ t \equiv ft_1t_2$ �ΤȤ���
$$
\infer=[(!e)(\forall e)]{i(ft_1t_2)}{
  !(\forall x \forall y(i(fxy)))}
$$
���
$$ \Delta \verifyonbck it$$
�������롣
��ä�
$$ \Delta, \fvsets{x}{1}{m},\circed{\Gamma} \verifyonbck \circed{([t/x]\beta)} $$

\bigskip

�� NJ �ǺǸ�ο�����§�� $(q)$ �ΤȤ�
$$
\infer{\alpha}{\bot}
$$
�ȤʤäƤ��롣 ���ΤȤ���Ǽˡ�β�����
$$ \Delta, \circed{\Gamma} \verifyonbck \bot $$
$(q)$ ��� 
$$ \Delta, \fvsets{x}{1}{n},\circed{\Gamma} \verifyonbck \circed{\alpha}$$

\end{proof}


\bibliography{logic}

\newpage

\section{����}

$http://www.math.s.chiba-u.ac.jp/~komori/papers/LogicSemi/$\\
�� komori6.dvi

$http://www.math.s.chiba-u.ac.jp/~komori/masters_thesis/2003/takayama/takayama.dvi
$

\end{document}
