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

% \input{define.tex}
\newtheorem{df}{��`}[section]
\newtheorem{thm}[df]{�藝}
\newtheorem{cor}[df]{�n}
\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{j#1_{#2}, \dots, j#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\gt ��t��w��w�@�@���R�Ȋw�����ȁ@\\[3mm]�C�m�_��}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf ���ώ�`�_���� $\BCKbe$ �̋����̓������ɂ���}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����16�N2����o}
\end{center}

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

\vspace*{5mm}
\begin{center}
{\Large\gt ���R�}���F}
\end{center}

\setcounter{page}{0}

\newpage

%% �ڎ�
\tableofcontents

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�͂��߂�}

$\lambda$-term �� $\Xi$ ���������̌n�ł��� $\BCKbe$ �Ɋւ��āA
���ώ�`�_���ł��� $NJ$ �� $\BCKbe$ �̋����̓������ɂ��čl�@�����B

�ÓT�_�� $NK$ �ƒ��ώ�`�_�� $NJ$ �̋����̓������ɂ��ẮA
$NK$ �� $NJ$ �ɖ��ߍ��߂邱�Ƃ������Ă��� Glivenko �̒藝�A
�y�� $NJ$ �� $NK$ �ɖ��ߍ��߂邱�Ƃ����� Kripke �͌^��p���Ď������B

���ώ�`�_���� $\BCKbe$ �ɖ��ߍ��߂邱�Ƃɂ��āA
$NJ$ �̘_�������� $\BCKbe$ �̘_�����ւ̕ϊ� * ���l���A
$NJ$ �ŏؖ��o����_���� $\alpha$ �Ɋւ��āA $\alpha^*$ �� $\BCKbe$ �ŏؖ��ł��邱�Ƃ�
$NJ$ �̏ؖ��}�ɂ��Ă̋A�[�@�Ŏ����Ă���B

���̘_���͌ÐX�Y��搶�ɂ��ڍׂȕ��j��^���炦�A�����̌v�Z�E���؂����R���s�����B

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�̌n�̋���}

\begin{df}
�̌n $L_1, L_2$ �������� $L_1$ �� $L_2$ ��苭���Ƃ́A
$L_2$ ���� $L_1$ �ւ̌v�Z�ł���ϊ� * �������āA
$$L_2 �� \alpha ���ؖ��ł��� \Llra L_1 �� \alpha^* ���ؖ��ł��� $$
�����藧���Ƃ������B

���̂Ƃ� $L_1 \succ L_2$ �Ə����A $L_2$ �� $L_1$ �ɖ��ߍ��߂�Ƃ����B
\end{df}

\begin{thm}
$$ L_1 \succ L_2 \ ���� \  L_2 \succ L_3 \Lra L_1 \succ L_3 $$
\end{thm}

\begin{proof}
��`���B
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \input{be.tex}
\section{�̌n $\BCKbe$}

$\lambda$-term �� $\Xi$ ���������̌n�ł��� $\BCKbe$ �͈ȉ��̂悤�ɒ�`�����B 

\begin{df} ($\lambda$-term)
\[
\begin{array}{rl}
�E & �̕ϐ��A�萔�� term �ł���B \\
�E & \alpha, \beta �� term �Ȃ�� (\alpha\beta) �� term �ł���B \\
�E & \alpha �� term �Ȃ�� (\lambda x.\alpha) �� term �ł���B \\
\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 �Ɏ��R�Ɍ���Ȃ�) \\ 
(\lambda x.\alpha)\beta & \equalbe & [\beta/x]\alpha \\
\lambda x.\alpha x & \equalbe & \alpha & (x �� \alpha �Ɏ��R�Ɍ���Ȃ�) \\
\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

�̌n $\BCKbe$ �̘_������ $\lambda$-term �̂��Ƃł���A�萔�Ƃ��� $\Xi$ ���܂�(cf. \cite{Hindley} CH17)�B
�̌n $\BCKbe$ �̐��_�K���͎��� 3 �ƂȂ�B
�܂��A��x�ɗ��Ƃ��鉼��͍��X1�ł���B ���Ȃ킿�A���� $k$ �͍��X1�����ɂ��������Ȃ��B

\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$ �y�ї����Ă��Ȃ�����Ɏ��R�Ɍ���Ȃ��B

\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

\begin{df}
$\Xi$ ��p����ƈȉ��̂悤�ɘ_���L����q�ꂪ�ȗ��L���Ƃ��Ē�`�ł���(cf. \cite{Komori02})�B

\[
\begin{array}{rll}
K & \equivdef & \lambda xy.x \\
I & \equivdef & \lambda x.x \\
\alpha \supset \beta & \equivdef & \Xi (K\alpha)(K\beta) \\
\top & \equivdef & \Xi II \\
\forall x\alpha & \equivdef & \Xi (K\top)(\lambda x.\alpha) \\
\Pi \alpha & \equivdef & \Xi (K\top)\alpha \\
\alpha + \beta & \equivdef & \forall y((\alpha \supset y) \supset (\beta \supset y) \supset y) \\
\alpha \& \beta & \equivdef & \forall y((\alpha \supset \beta \supset y) \supset y) \\
\exists x\alpha & \equivdef & \forall y(\forall x (\alpha \supset y) \supset y) \\
\bot & \equivdef & \forall xx \\
\alpha \in \beta & \equivdef & \beta \alpha \\
\alpha \wedge \beta & \equivdef & \forall x(\forall y((y \supset \alpha) \supset (y \supset \beta) \supset y \supset x) \supset x) \\
\alpha \vee \beta & \equivdef & \forall y((\alpha \supset y) \supset ((\beta \supset y) \supset y)) \\
\end{array}
\]

$x, y$ �� $\alpha, \beta$ �ɂ͎��R�Ɍ���Ȃ��B 
\end{df}


\begin{thm}
��L�̏ȗ��L����p���Ĉȉ��̐��_�K�����������(cf. \cite{Hindley} CH17)�B 

�� 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$ �͗����Ă��Ȃ�����Ɏ��R�Ɍ���Ȃ��B

\bigskip

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

�� Universal quantifier introduction, second form ($\Pi$ i) 
\nobreak
$$ \infer[(\Pi i)]{\Pi \alpha}{\alpha x} $$
\nobreak
\triquad $x$ �� $\alpha$ �y�ї����Ă��Ȃ�����Ɏ��R�Ɍ���Ȃ��B

\bigskip

�� Universal quantifier elimination, second form ($\Pi$ e) 
\nobreak
$$ \infer[(\Pi e)]{\alpha\beta}{\Pi\alpha} $$ 

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

\bigskip

\end{thm}

\begin{proof}
($\forall$ i) �ɂ��ďؖ�����B 

$$
\infer[(\Eqbe)]{\forall x\alpha}{
  \infer[1 (\Xi i)]{\Xi (KT)(\lambda x.\alpha)}{
    \infer[(\Eqbe)]{(\lambda x.\alpha)x}{
      \infer[(\Xi e)]{I((\lambda x.\alpha)x)}{
        \infer[(\Eqbe)]{\Xi II}{
          \infer[(\Eqbe)]{T}{
            \deduce{(KT)x}{
              1
            }
          }
        }
        &
        \infer[(\Eqbe)]{I((\lambda x.\alpha)x)}{
          \infer[(\Eqbe)]{(\lambda x.\alpha)x}{
            \alpha
          }
        }
      }
    }
  }
}
$$
\end{proof}

�����ŁA���`�_���� ! (cf. \cite{Girard1987}) �ɗގ��������������L���� $\BCKbe$ �ɓ�������B 

\begin{df}

�ÐX \cite{Komori02} �ɂ� $!\alpha$ ���ȉ��̂悤�ɒ�`����ƒ藝 \ref{exclamationdeduction} ��������邱�Ƃ��q�ׂ��Ă���B  
$$! \alpha \equivdef \forall x (x\top \supset x \alpha) $$
������ $x$ �� $\alpha$ �ɂ͎��R�Ɍ���Ȃ�
\end{df}


\begin{thm}\label{exclamationdeduction} $!\alpha$ �ɂ��Ĉȉ��̐��_�K�����������B

�� ! 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)$ �ɂ����ĉ���͂����ł����Ƃ���B
\end{center}


\end{thm}

\begin{proof}
$(!e)$ �Ɋւ���

$$
\infer[(\supset e)]{\alpha}{
  \infer[(\Eqbe)]{\top \supset \alpha}{
    \infer[(\Eqbe)]{I\top \supset I\alpha}{\infer[(\forall e)]{(\lambda x . (x\top \supset x\alpha))I}{!\alpha}}
  }
  &
  \infer[(\Eqbe)]{\top}{\infer[1(\supset i)]{II \supset II}{\deduce{II}{1}}}
}
$$

\vspace*{10mm}

$(!\supset i)$ �Ɋւ���

�܂�
$$ \infer[\qquad \dots (*) ]{!\alpha \supset \beta}{!\alpha \supset !\alpha \supset \beta} $$
���ؖ��\�ł��邱�Ƃ������B


�����ňȉ��̂悤�ɒ�`����ƁA
\[
\begin{array}{rll}
X & = & \forall y ((!y \supset !\alpha) \supset (!y \supset !\alpha) \supset \beta) \\
Y & = & !\top \supset !\alpha \\
Z & = & !\alpha \supset !\alpha \\
\end{array}
\]
���̂悤�ɂ��� $!\top, Z$ ��������B

$$ \infer[(\forall i)]{\forall x (x\top \supset x\top)}{\infer[1(\supset i)]{x\top \supset x\top}{\deduce{x\top}{1}}}$$
$$ \infer[1(\supset i)]{!\alpha \supset !\alpha}{\deduce{!\alpha}{1}}$$

����Ĉȉ��ɂ�� (*) ���������B

$$
\infer[3(\supset i)]{!\alpha \supset \beta}{
  \infer[(\supset e)]{\beta}{
    \infer[(\supset e)]{Z \supset \beta}{
      \infer[(\supset e)]{Z \supset Z \supset \beta}{
        \infer[(\forall e)(\Eqbe)]{(Y \supset Y \supset \beta) \supset Z \supset Z \supset \beta}{
          \infer[(\Eqbe)]{(X\top) \supset (X\alpha)}{
            \infer[(\forall e)]{(\lambda x . (x\top \supset x\alpha))X}{
              \deduce{!\alpha}{3}}
            }
          }
        &
        \infer[2(\supset i)]{Y \supset Y \supset \beta}{
          \infer[1(\supset i)]{Y \supset \beta}{
            \infer[(\supset e)]{\beta}{
              \infer[(\supset e)]{!\alpha \supset \beta}{
                !\alpha \supset !\alpha \supset \beta & \infer[(\supset e)]{!\alpha}{\deduce{Y}{1} & !\top}
              }
              &
              \infer[(\supset e)]{!\alpha}{
                \deduce{Y}{2}
                &
                !\top
              }
            }
          }
        }
      }
      &
      Z
    }
    &
    Z
  }
}
$$

���āA$(!\supset i)$ �ɂĉ��肪 n �������Ƃ� $(\supset i)$ �� n ��p�����
$$ \infer=[k(\supset i)]{!\alpha \supset \dots \supset !\alpha \supset !\alpha \supset \beta}{\deduce{\beta}{\deduce{\Sigma}{\deduce{!\alpha}{k}}}}$$
�ƂȂ�A����� (*) ���
$$ \infer={!\alpha \supset \beta}{\infer=[k(\supset i)]{!\alpha \supset \dots \supset !\alpha \supset !\alpha \supset \beta}{\deduce{\beta}{\deduce{\Sigma}{\deduce{!\alpha}{k}}}}}$$
�ƂȂ�B 

\end{proof}

$\Gamma$ ��_�����̗�Ƃ����Ƃ��A
$\Gamma$ �Ɋ܂܂��_�����𗎂��Ă��Ȃ�����Ƃ� $\alpha$ �Ɏ��� $\BCKbe$ �̐��_�}������Ƃ�
$$
\Gamma \verifyonbck \alpha
$$
�Ə����B ����ɂȂ��_������ $\Gamma$ �Ɋ܂܂�Ă��Ă��悢�B 

\bigskip

�܂� $\alpha$ �Ɋ܂܂�鎩�R�ϐ��S�̂̏W���� $FV(\alpha)$ �Ƃ���B 

% \input{nj.tex}
\section{�̌n $NJ$}

�����ł� Gentzen \cite{Gentzen} (\cite{Szabo}) �ɂ�钼�ώ�`�_���̑̌n $NJ$ �� $\{\supset, \forall, \bot\}-fragment$(�f��)���l����B
�ȉ��ł� $NJ$ �� $\{\supset, \forall, \bot\}-fragment$ �� $NJ$ �Əȗ�����B 

$NJ$ �͈ȉ��̂悤�ɂ��Ē�`�����B 

\begin{df} (��)
\[
\begin{array}{rl}
�E & �̕ϐ��A�萔�͍��ł���B \\
�E & \varsets{t}{1}{n} �����ł���Af �� n �ϐ��̊֐��L���Ȃ�� (ft_1\dots t_n) �͍��ł���B \\
\end{array}
\]
\end{df}

\begin{df} (�_����)
\[
\begin{array}{rl}
�E & ����萔 \bot �͘_�����ł���B \\
�E & \varsets{t}{1}{n} �����ł���Ap �� n �ϐ��̏q��L���Ȃ�� pt_1\dots t_n �͘_�����ł���B \\
�E & \alpha, \beta ���_�����Ȃ�� (\alpha \supset \beta) �͘_�����ł���B \\
�E & \alpha ���_�����Ȃ�� \lambda x.\alpha �͘_�����ł���B \\
\end{array}
\]
$ \bot �� pt_1\dots t_n$ �̌`�̘_������ atom �ƌĂԁB 
�܂��A�_�����Ɋ܂܂�� $\supset$ �� $\forall$ �̌���_�����̒����Ƃ����B 
���̒����Ɋւ��āA�̕ϐ��E�萔�̒����� 1�A $(ft_1\dots t_n)$ �̒����� $L(t_1) + \dots + L(t_n) + 1$ �Ƃ���B
\end{df}

\bigskip

\begin{df}
 $NJ$ �̐��_�K���͎��� 5 �ł���B 

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

�� implication elimination $ (\supset e) $
\nobreak
$$ \infer[(\supset e)]{\beta}{\alpha \supset \beta & \alpha} $$

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

�� Universal quantifier introduction $(\forall i)$
\nobreak
$$ \infer[(\forall i)]{\forall x\alpha}{\alpha} $$
\nobreak
\triquad $x$ �͗����Ă��Ȃ�����Ɏ��R�Ɍ���Ȃ��B
\bigskip

�� Universal quantifier elimination $(\forall e)$
\nobreak
$$ \infer[(\forall e)]{[t/x]\alpha}{\forall x\alpha} $$
\nobreak
\triquad $t$ �͍��B
\end{df}

\bigskip

$\Gamma$ ��_�����̗�Ƃ����Ƃ��A
$\Gamma$ �Ɋ܂܂��_�����𗎂��Ă��Ȃ�����Ƃ� $\alpha$ �Ɏ��� $NJ$ �̐��_�}������Ƃ�
$$
\Gamma \verifyonnj \alpha
$$
�Ə����B ����ɂȂ��_������ $\Gamma$ �Ɋ܂܂�Ă��Ă��悢�B 
�_�����̗� $\Gamma$, $\Sigma$ ���W���Ƃ��ē������Ƃ� $\Gamma \verifyonnj \alpha$ �Ȃ�� $\Sigma \verifyonnj \alpha$ �ł���B 

\bigskip 

�܂� $\alpha$ �Ɋ܂܂�鎩�R�ϐ��S�̂̏W���� $FV(\alpha)$ �Ƃ���B 
% \input{nj-be.tex}
\section{$NJ$ �� $\BCKbe$ �ւ̖��ߍ���}

$NJ$ �̘_�������� $\BCKbe$ �̘_�����ւ̕ϊ� * ���l���A
$NJ$ �ŏؖ��o����_���� $\alpha$ �Ɋւ��āA $\alpha^*$ �� $\BCKbe$ �ŏؖ��\�ƂȂ邱�Ƃ���
���ώ�`�_�� $NJ$ �� $\BCKbe$ �ɖ��ߍ��߂邱�Ƃ������B

\bigskip

�܂��́A
\begin{itemize}
\item �֐��L���� 2 �ϐ��֐��L�� f �̂�
\item �q��L���� 2 �ϐ��q��L�� p �̂�
\end{itemize}
����Ȃ� $NJ$ �ɂ��čl����B 

\bigskip

������ $\BCKbe$ �ɂ����� $x$ ���̂ł��邱�Ƃ������q�� $i$ �𓱓�����B
�܂��ȗ��̂��� $!(ix)$ �� $jx$ ���L�����Ƃɂ���B
$$ jx \ \ \equiv \ \ !(ix) $$

\begin{df}
$\BCKbe$ �ɂ����Ĉȉ��̘_��������ׂ���� $\Delta$ �Ƃ���B

$$ jc $$
$$ !(\forall x (jx \supset !(jx))) $$
$$ !(\forall x \forall y ((x \supset !x) \supset (y \supset !y) \supset (x \supset y) \supset !(x \supset y))) $$
$$ !(\forall x (\forall y (jy \supset xy \supset !(xy)) \supset \Pi x \supset !(\Pi x))) $$
$$ !(\forall x (jx \supset jy \supset j(fxy))) $$
$$ !(\forall x \forall y (jx \supset jy \supset pxy \supset !(pxy))) $$
\end{df}

�e�_�����ɂ����Ė���������邽�߂� $i$ �𓱓����邱�Ƃ͌ÐX�搶�ɂ��B 
�܂��A���� $\Delta$ �Ɋ܂܂�Ă��Ȃ����� $!(\forall x (jx \supset !(jx)))$ �̓����͍��R�ɂ��B 

\begin{lemma}\label{contractionhypothesis} (contraction)
$$ jx, jx, \Gamma \verifyonbck \alpha $$
�̂Ƃ��A
$$ jx, \Gamma \verifyonbck \alpha $$
\end{lemma}

\begin{proof}
$ (!\supset i) $ �ɂ��B
\end{proof}

\begin{lemma}\label{termonbck}
$NJ$ �̍� $t$ �Ɋւ��āA$t$ �Ɍ�����̕ϐ��� $\varsets{x}{1}{n}$ �Ƃ����
$$ \fvsets{x}{1}{n} \verifyonbck jt $$
\end{lemma}

\begin{proof}
$t$ �̒����Ɋւ���A�[�@�B $t$ �� $ft_1t_2$ �̂Ƃ��Ɋւ��Ă̏ؖ�������B

�A�[�@�̉�����
$t_1$ �̌̕ϐ��� $\varsets{x}{1}{m}$�A $t_2$ �̌̕ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
\[
\begin{array}{rll}
\fvsets{x}{1}{m} & \verifyonbck & jt_1 \\
\fvsets{y}{1}{n} & \verifyonbck & jt_2 \\
\end{array}
\]
�ł���B ������
$$
\infer{j(ft_1t_2)}{
  \infer{jt_2 \supset j(ft_1t_2)}{
    \infer=[(!e) (\forall e)]{jt_1 \supset jt_2 \supset j(ft_1t_2)}{
      !(\forall x (jx \supset jy \supset j(fxy)))
    }
    &
     jt_1
  }
  &
  jt_2
}
$$
���
\[
\begin{array}{rll}
\fvsets{x}{1}{m}, \fvsets{y}{1}{n} & \verifyonbck & jt \\
\end{array}
\]
��� \ref{contractionhypothesis} ��� $ \varsets{x}{1}{m}, \varsets{y}{1}{n} $ ����d���𗎂Ƃ��� $t$ �̌̕ϐ��ƂȂ�B
\end{proof}


\begin{df}
$NJ$ �̘_���� $\alpha$ ���� $\BCKbe$ �̘_���� $\circed{\alpha}$ ���ȉ��̂悤�ɒ�`����B
\[
\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 & \forall x (jx \supset \circed{\alpha}) \\
\end{array}
\]
\end{df}

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

\begin{proof}
$\alpha$ �̒����Ɋւ���A�[�@�B
\end{proof}


\begin{thm}\label{exclamation}
$NJ$ �̘_���� $\alpha$ �Ɋւ��āA$\alpha$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{n}, \circed{\alpha} \verifyonbck !(\circed{\alpha}) $$
\end{thm}

\begin{proof}

$\alpha$ �̒����Ɋւ���A�[�@�B

\bigskip

�� $\alpha$ �� atom �̂Ƃ�

$\alpha \ \ \equiv \ \ \circed{\alpha} \ \ \equiv \ \ pt_1t_2$ �ƂȂ�B

���̂Ƃ� $t_1$ �Ɍ�����̕ϐ��� $\varsets{x}{1}{m}$�A$t_2$ �Ɍ�����̕ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
��� \ref{termonbck} ���
\[
\begin{array}{rll}
\fvsets{x}{1}{m} & \verifyonbck & jt_1 \\
\fvsets{y}{1}{n} & \verifyonbck & jt_2 \\
\end{array}
\]
���̂Ƃ�
$$
\infer{!(pt_1t_2)}{
  \infer{pt_1t_2 \supset !(pt_1t_2)}{
    \infer{jt_2 \supset pt_1t_2 \supset !(pt_1t_2)}{
      \infer=[(!e) (\forall e)]{jt_1 \supset jt_2 \supset pt_1t_2 \supset !(pt_1t_2)}{
        !(\forall x \forall y (jx \supset jy \supset pxy \supset !(pxy)))
      }
      &
      jt_1
    }
    &
    jt_2
  }
  &
  pt_1t_2
}
$$
���
$$ \Delta, \fvsets{x}{1}{m}, \fvsets{y}{1}{n}, \circed{\alpha} \verifyonbck !(\circed{\alpha}) $$
��� \ref{contractionhypothesis} ��� $ \varsets{x}{1}{m}, \varsets{y}{1}{n} $ ����d���𗎂Ƃ��� $\alpha$ �̎��R�ϐ��ƂȂ�B


\bigskip

�� $\alpha \ \ \equiv \ \ \beta \supset \gamma$ �̂Ƃ�

�A�[�@�̉�����
$\beta$ �̎��R�ϐ��� $\varsets{x}{1}{m}$�A $\gamma$ �̎��R�ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
\[
\begin{array}{rll}
\Delta, \fvsets{x}{1}{m}, \circed{\beta} & \verifyonbck & !(\circed{\beta}) \\
\Delta, \fvsets{y}{1}{n}, \circed{\gamma} & \verifyonbck & !(\circed{\gamma}) \\
\end{array}
\]
�ł���B �����
\[
\begin{array}{rll}
\Delta, \fvsets{x}{1}{m} & \verifyonbck & \circed{\beta} \supset !(\circed{\beta}) \\
\Delta, \fvsets{y}{1}{n} & \verifyonbck & \circed{\gamma} \supset !(\circed{\gamma}) \\
\end{array}
\]
������
$$
\infer{!(\circed{\beta} \supset \circed{\gamma})}{
  \infer{(\circed{\beta} \supset \circed{\gamma}) \supset !(\circed{\beta} \supset \circed{\gamma})}{
    \infer{(\circed{\gamma} \supset \circed{!\gamma}) \supset (\circed{\beta} \supset \circed{\gamma}) \supset !(\circed{\beta} \supset \circed{\gamma})}{
      \infer=[(!e) (\forall e)]{(\circed{\beta} \supset !(\circed{\beta})) \supset (\circed{\gamma} \supset !(\circed{\gamma})) \supset (\circed{\beta} \supset \circed{\gamma}) \supset !(\circed{\beta} \supset \circed{\gamma})}{
        !(\forall x \forall y ((x \supset !x) \supset (y \supset !y) \supset (x \supset y) \supset !(x \supset y)))
      }
      &
      \circed{\beta} \supset !(\circed{\beta})
    }
    &
    \circed{\gamma} \supset !(\circed{\gamma})
  }
  &
  \circed{\beta} \supset \circed{\gamma}
}
$$
����
$$ \Delta, \fvsets{x}{1}{m}, \fvsets{y}{1}{n}, \circed{\alpha} \verifyonbck !(\circed{\alpha}) $$
��� \ref{contractionhypothesis} ��� $ \varsets{x}{1}{m}, \varsets{y}{1}{n} $ ����d���𗎂Ƃ��� $\alpha$ �̎��R�ϐ��ƂȂ�B

\bigskip

�� $\alpha = \forall x \beta$ �̂Ƃ�

�A�[�@�̉����� $\beta$ �̎��R�ϐ��� $\varsets{x}{1}{m}$ �Ƃ���ƁA
$$ \Delta, \fvsets{x}{1}{m}, \circed{\beta} \verifyonbck !(\circed{\beta}) $$
�ł���B �����
$$ \Delta, \fvsets{x}{1}{m} \verifyonbck \circed{\beta} \supset !(\circed{\beta}) $$
������
$$
\infer{(\circed{\beta} \supset !(\circed{\beta} )) \supset (jx \supset \circed{\beta} ) \supset !(jx \supset \circed{\beta} )}{
  \infer=[(!e) (\forall e)]{(jx \supset !(jx)) \supset (\circed{\beta} \supset !(\circed{\beta} )) \supset (jx \supset \circed{\beta} ) \supset !(jx \supset \circed{\beta} )}{
    !(\forall x \forall y ((x \supset !x) \supset (y \supset !y) \supset (x \supset y) \supset !(x \supset y)))
  }
  &
  \infer=[(!e) (\forall e)]{jx \supset !(jx)}{
    !(\forall x(jx \supset !(jx)))
  }
}
$$
���
$$ \Delta, \fvsets{x}{1}{m} \verifyonbck (jx \supset \circed{\beta}) \supset !(jx \supset \circed{\beta}) $$
�䂦�� $\forall x \beta$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ����Ƃ�
$$ \Delta, \fvsets{x}{1}{n} \verifyonbck jx \supset (jx \supset \circed{\beta}) \supset !(jx \supset \circed{\beta}) $$
�ƂȂ�B
$$
\infer[(\Eqbe)]{(jx \supset (jx \supset \circed{\beta}) \supset !(jx \supset \circed{\beta})) \supset \circed{(\forall x\beta)} \supset !(\circed{(\forall x\beta)})}{
  \infer[(!e) (\forall e)]{(jx \supset (\lambda x.(jx \supset \circed{\beta}))x \supset !((\lambda x.(jx \supset \circed{\beta}))x)) \supset \Pi (\lambda x.(jx \supset \circed{\beta})) \supset !(\Pi (\lambda x.(jx \supset \circed{\beta})))}{
    !(\forall x (\forall y (jy \supset xy \supset !(xy)) \supset \Pi x \supset !(\Pi x)))
  }
}
$$
���
$$ \Delta, \fvsets{x}{1}{n} \verifyonbck \circed{(\forall x\beta)} \supset !(\circed{(\forall x\beta)}) $$
���Ȃ킿
$$ \Delta, \fvsets{x}{1}{n}, \circed{\alpha} \verifyonbck \supset !(\circed{\alpha}) $$

\end{proof}

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

\begin{proof}

$\alpha$ �̒����Ɋւ���A�[�@�B

\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$ �̂Ƃ�

�A�[�@�̉�����
\[
\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) $ �̂Ƃ�

�� $ y \notin FV(t) $ �̂Ƃ�

�A�[�@�̉�����
\[
\begin{array}{rll}
\ [t/x](\circed{\beta}) & \equalbe & \circed{([t/x]\beta)} \\
\end{array}
\]
������
\[
\begin{array}{rll}
[t/x](\circed{\alpha}) & \equalbe & [t/x](\forall y(jy \supset \circed{\beta})) \\
                & \equalbe & \forall y(jy \supset [t/x](\circed{\beta})) \\
\circed{([t/x]\alpha)} & \equalbe & \circed{(\forall y([t/x]\beta))} \\
                & \equalbe & \forall y(jy \supset \circed{([t/x]\beta)}) \\
\end{array}
\]
���
$$ [t/x](\circed{\alpha}) \equalbe \circed{([t/x]\alpha)} $$

�� $ y \in FV(t) $ �̂Ƃ�

�A�[�@�̉�����
\[
\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](\forall y(jy \supset \circed{\beta})) \\
                & \equalbe & \forall y(jy \supset [t/x][z/y](\circed{\beta})) \\
\circed{([t/x]\alpha)} & \equalbe & \circed{(\forall y([z/x]\beta))} \\
                & \equalbe & \forall y(jy \supset \circed{([t/x][z/y]\beta)}) \\
\end{array}
\]
���
$$ [t/x](\circed{\alpha}) \equalbe \circed{([t/x]\alpha)} $$

\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thm}\label{njinbckeb}
$$ \Gamma \verifyonnj \alpha $$
�̂Ƃ��A$\alpha$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{n}, !(\circed{\Gamma}) \verifyonbck \circed{\alpha} $$
������ $!(\circed{\Gamma})$ �� $\Gamma$ �Ɋ܂܂�鉼�� $\beta$ �Ɋւ��� $!(\circed{\beta})$ �Ƃ������́B
\end{thm}

\begin{proof}

$NJ$ �ł̐��_�}�̒����Ɋւ���A�[�@�B

\bigskip

�� ���_�}�̒����� 1 �̂Ƃ�

$\alpha$ �� $\Gamma$ �Ɋ܂܂��̂�
$$ \Gamma \verifyonnj \alpha $$
���
$$ !(\circed{\Gamma}) \verifyonbck !(\circed{\alpha})$$
����� $\alpha$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{n}, !(\circed{\Gamma}) \verifyonbck \circed{\alpha} $$

\bigskip

�� NJ �ōŌ�̐��_�K���� $(\supset e)$ �̂Ƃ�
$$
\infer[(\supset e)]{\alpha}{\beta \supset \alpha & \beta}
$$
�ƂȂ��Ă���B ���̂Ƃ��A�[�@�̉����� $\beta \supset \alpha$ �̎��R�ϐ��� $\varsets{x}{1}{m}$, $\beta$ �̎��R�ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
\[
\begin{array}{rll}
\Delta, \fvsets{x}{1}{m}, !(\circed{\Gamma}) & \verifyonbck & \circed{(\beta \supset \alpha)} \\
\Delta, \fvsets{y}{1}{n}, !(\circed{\Gamma}) & \verifyonbck & \circed{\beta} \\
\end{array}
\]
�ł���B ���̂Ƃ� $x \in FV(\beta)$ ���� $x \notin FV(\alpha)$ �ƂȂ� $\beta$ �̎��R�ϐ� $x$ �ɑ΂��� $c$ �����������̂� $\beta'$ �Ƃ��A
$\alpha$ �̎��R�ϐ��� $\varsets{z}{1}{l}$ �Ƃ����
\[
\begin{array}{rll}
\Delta, \fvsets{z}{1}{l}, !(\circed{\Gamma}) & \verifyonbck & \circed{(\beta' \supset \alpha)} \\
\Delta, \fvsets{z}{1}{l}, !(\circed{\Gamma}) & \verifyonbck & \circed{(\beta')} \\
\end{array}
\]
�ƂȂ�B �����
\[
\begin{array}{rll}
\Delta, \fvsets{z}{1}{l}, !(\circed{\Gamma}) & \verifyonbck & \circed{\alpha} \\
\end{array}
\]

\bigskip

�� NJ �ōŌ�̐��_�K���� $(\supset i)$ �̂Ƃ�
$$
\infer[k(\supset i)]{\beta \supset \gamma}{
  \deduce{\gamma}{
    \deduce{\Pi}{
      \deduce{\beta}{k}
    }
  }
}
$$
�ƂȂ��Ă���B ���̂Ƃ��A�[�@�̉����� $\gamma$ �̎��R�ϐ��� $\varsets{x}{1}{m}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{m}, !(\circed{\Gamma}), !(\circed{\beta}) \verifyonbck \circed{\gamma} $$
�ł���B �����Œ藝 \ref{exclamation} ��� $\circed{\beta}$ �̎��R�ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{y}{1}{n}, \circed{\beta} \verifyonbck !(\circed{\beta}) $$
�ƂȂ�̂�
$$ \Delta, \fvsets{x}{1}{m}, \fvsets{y}{1}{n}, !(\circed{\Gamma}), \circed{\beta} \verifyonbck \circed{\gamma} $$
��� \ref{contractionhypothesis} ��� $x_i, y_i$ ����d���������� $\beta \supset \gamma$ �̎��R�ϐ� $\varsets{z}{1}{l}$ �ƂȂ�B �����
$$ \Delta, \fvsets{z}{1}{l}, !(\circed{\Gamma}) \verifyonbck \circed{(\beta \supset \gamma)} $$

\bigskip

�� NJ �ōŌ�̐��_�K���� $(\forall i)$ �̂Ƃ�
$$
\infer{\forall x\beta}{\beta}
$$
�ƂȂ��Ă���B ($x$ �͗����Ă��Ȃ�����Ɍ���Ȃ�)�B
���̂Ƃ��A�[�@�̉����� $\beta$ �̎��R�ϐ��� $\varsets{x}{1}{m}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{m}, !(\circed{\Gamma}) \verifyonbck \circed{\beta} $$
�ł���B ���̂Ƃ� $\forall x\beta$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ���
$$ \Delta, \fvsets{x}{1}{n}, !(\circed{\Gamma}) \verifyonbck jx \supset \circed{\beta} $$
�ƂȂ�B ��� \ref{fvsets} ��� $!(\circed{\Gamma})$ �� $x$ �͎��R�Ɍ���Ȃ��̂ŁA$(\forall i)$ ���
$$ \Delta, \fvsets{x}{1}{n}, !(\circed{\Gamma}) \verifyonbck \circed{(\forall x \beta)} $$


\bigskip

�� NJ �ōŌ�̐��_�K���� $(\forall e)$ �̂Ƃ�
$$
\infer{[t/x]\beta}{\forall x\beta}
$$
�ƂȂ��Ă���B ���̂Ƃ��A�[�@�̉����� $\forall x\beta$ �̎��R�ϐ��� $\varsets{x}{1}{m}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{m}, !(\circed{\Gamma}) \verifyonbck \circed{(\forall x\beta)} $$
�ł���B ������

�� $x \notin FV(\beta)$ �̂Ƃ�

$$
\infer{\circed{([t/x]\beta)}}{
  \infer[(\forall e)]{jc \supset \circed{\beta}}{
    \infer[(\Eqbe)]{\forall x (jx \supset \circed{\beta})}{
      \circed{(\forall x \beta)}
    }
  }
  & jc
}
$$

�ƂȂ�A$[t/x]\beta$ �̎��R�ϐ��� $\varsets{x}{1}{m}$ �ɂȂ�̂�
$$ \Delta, \fvsets{x}{1}{m}, !(\circed{\Gamma}) \verifyonbck \circed{([t/x]\beta)} $$


�� $x \in FV(\beta)$ �̂Ƃ�

$$
\infer[(\Eqbe)]{\circed{([t/x]\beta)}}{
  \infer{[t/x](\circed{\beta})}{
    \infer[(\forall e)]{jt \supset [t/x](\circed{\beta})}{
      \infer[(\Eqbe)]{\forall x (jx \supset \circed{\beta})}{
        \circed{(\forall x \beta)}
      }
    }
    & jt
  }
}
$$
���
$$ \Delta, \fvsets{x}{1}{m}, jt, !(\circed{\Gamma}) \verifyonbck \circed{([t/x]\beta)} $$
�ƂȂ�B ��� \ref{termonbck} ��� $t$ �̎��R�ϐ��� $\varsets{y}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{m}, \fvsets{y}{1}{n}, !(\circed{\Gamma}) \verifyonbck \circed{([t/x]\beta)} $$
��� \ref{contractionhypothesis} ��� $ \varsets{x}{1}{m}, \varsets{y}{1}{n} $ ����d���𗎂Ƃ��� $[t/x]\beta$ �̎��R�ϐ��ƂȂ�B


\bigskip

�� NJ �ōŌ�̐��_�K���� $(q)$ �̂Ƃ�
$$
\infer{\alpha}{\bot}
$$
�ƂȂ��Ă���B ���̂Ƃ��A�[�@�̉�����
$$ \Delta, !(\circed{\Gamma}) \verifyonbck \bot $$
$(q)$ ��� $\alpha$ �̎��R�ϐ��� $\varsets{x}{1}{n}$ �Ƃ����
$$ \Delta, \fvsets{x}{1}{n}, !(\circed{\Gamma}) \verifyonbck \circed{\alpha} $$

\end{proof}


\begin{cor}\label{njinbckebcor}
$NJ$ �̏q��ϐ��E�֐��L���ɂ��Ă��ꂼ��
\begin{itemize}
\item NJ �� n �ϐ��֐��L�� $f_1$ ���܂ނƂ�
$$ !(\forall x_1 \cdots \forall x_n (jx_1 \supset \cdots \supset jx_n \supset j(f_1 x_1 \cdots x_n))) $$
\item NJ �� n �ϐ��q��L�� $p_1$ ���܂ނƂ� 
$$ !(\forall x_1 \cdots \forall x_n (jx_1 \supset \cdots \supset jx_n \supset p_1 x_1\cdots x_n \supset !(p_1 x_1\cdots x_n))) $$
\end{itemize}
�� $\Delta$ �ɉ�����ƒ藝 \ref{njinbckeb} �����藧�B 
\end{cor}

\begin{proof}
��� \ref{termonbck} �ƒ藝 \ref{exclamation} �� $f_1, p_1$ �Ɋւ��Ċg������Ηǂ��B 
\end{proof}

\bigskip 

������ $NJ$ �̘_���� $\alpha$ ���� $\BCKbe$ �̘_�����ւ̕ϊ� $\alpha^*$ ���l����B 
\[
\begin{array}{rll}
\alpha^* & \equivdef & \Delta \supset jx_1 \supset \cdots \supset jx_n \supset \circed{\alpha} 
\end{array}
\]
���̂Ƃ��A�n \ref{njinbckebcor} ����ʂ� $NJ$ �ɂ��āA
$\alpha$ �� $NJ$ �ŏؖ��o����Ƃ� $\alpha^*$ �� $\BCKbe$ �ŏؖ��o����B 






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�I����}

$\BCKbe$ �ŏؖ��o����_���� $\alpha^*$ �Ɋւ��� $\alpha$ �� $NJ$ �ŏؖ��o���邱�Ƃ�
$\BCKbe$ �̃��f�����l���邱�Ƃ�莦�����Ǝv����B

�܂� $\BCKbe$ �� $NJ$ �ւ̖��ߍ��݂Ɋւ��Ă�
$NK \succ \BCKbe$ �������A $NJ \succ NK$ ���� $NJ \succ \BCKbe$ ���������Ƃŏؖ��ł���ƍl������B


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage

\section{�ӎ�}

�{�_���쐬�ɂ�����A�w�������̌ÐX�搶�A�ÐX�������̊F�l��
����Ȃ����͂𒸂��܂������Ƃ�S���犴�ӂ������܂��B


\bibliography{logic}

\end{document}
