%\documentclass[b5paper,twoside]{jsarticle}
%\documentclass[twoside]{jsarticle}
\documentclass[11pt]{jsarticle}
\usepackage{proof,color}
%\usepackage{proof}
%\setlength{\textwidth}{125truemm}
%\setlength{\textheight}{200truemm}
%\setlength{\oddsidemargin}{3truemm}
%\setlength{\evensidemargin}{3truemm}
%\setlength{\topmargin}{-5truemm}
%\setlength{\headsep}{5truemm}
%\setlength{\headheight}{5truemm}
%\setcounter{page}{43}
\newtheorem{definition}{��`}
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{problem}[definition]{���}
\newtheorem{conjecture}[definition]{�\�z}
\pagestyle{myheadings}
\renewcommand{\to}{\supset}
%\title{\textcolor{blue}{�ėp�V�X�e���Ƃ��Ắu�����_�v�Z + �_���v}}       
\title{�u�����_�v�Z + �_���v�̑̌n BCK$\beta$ �ł̏W���_�̃V�~�����[�V����}       
\author{��t��w �������f�B�A��ՃZ���^�[ �ÐX �Y�� (Yuichi Komori) \\
    komori@math.s.chiba-u.ac.jp}
\date{2007 �N 11 �� 30 ��}
%\date{}
\pagestyle{plain}
\begin{document}
\maketitle
\thispagestyle{plain}
\section{���_}
�ŋ�, �̌n BCK$\beta$ (���R, BCK$\beta\eta$ �ł�) �ɂ�����, ��W���̊O���������������
�o�邱�Ƃ����������B���̌���, ��W�����珇���K�v�ȏW��������Ă����Ƃ������@�� BCK$\beta$
�ŊO�������������W���_���V�~�����[�g���邱�Ƃ͂ł��Ȃ��B�F�X�Ȃ������ȋ���������N���X
�̒����琫���̂悢�N���X(������W���ƌĂڂ�)��I�яo��(�I�яo�����߂̏q�ꂪ $i$),
���̏����Ȑ��E�����ōl����ƊO���������藧���Ă���, �Ƃ̍l���ŃV�~�����[�g���Ă݂邱�Ƃ�
����B������, ���̏ؖ��͊������Ă��Ȃ��̂�, ���Ƃ��Ē�o�������B
%
\section{�u�����_�v�Z + �_���v�̑̌n BCK$\beta$}
%
�قڌÐX\cite{Komori89} �ɂ��������Đ�������B
�����_���͌^�Ȃ������_���̂��Ƃł���, �Z�̒萔���܂�, ���̒��ɂ́u{$\Xi, i$}�v������B
�̌n $BCK\beta$ �̘_�����̓����_���̂��Ƃł���B�̌n $BCK\beta$ �̐��_�K���͎��� 3 �ł���:
\[ \vcenter{\infer[\Xi e]{\beta\gamma}{\deduce{\Xi\alpha\beta}{\Pi_1}  & \deduce{\alpha\gamma}{\Pi_2}}},
\hspace{7mm} \vcenter{\infer[k (\Xi i)]{\Xi\alpha\beta}{\deduce{\beta x}{\deduce{\Pi}{\deduce{\alpha x}{k}}}}},
\hspace{7mm} \vcenter{\infer[\beta]{\beta}{\deduce{\alpha}{\Pi}}}\mbox{\ \ if \ \ }\alpha=_{\beta}\beta.
\]
������, �K�� ($\Xi$i) �ɂ����Ă͕ϐ� $x$ �� $\alpha$, $\beta$ ����ї����Ă��Ȃ�����Ɏ��R�Ɍ����Ȃ��B�܂�,
��x�ɗ��Ƃ��鉼��͍��X 1 �ł���, ���Ȃ킿 ���� $k$ �͍��X 1 �����ɂ��������Ȃ��B

�� {$\Xi\alpha\beta$} �̒��ϓI�ȈӖ��� {$\forall x(\alpha x\to \beta x)$} ��
����B�萔 $i$ �ɂ��Ă� $i$ ���ȉ��̒�`�Ŏg���Ă͂��邪, ����ɂ��Ă̐��_�K�����������Ȃ��̂�
���̂Ƃ�����ʂȈӖ��͂Ȃ��B���̌���͕\���͂��L����
�����̘_���L����q�ꂪ�ȗ��L���Ƃ��Ē�`�ł��邪�ȉ��ł͌�ŕK�v�Ȓ�`�������L��:
{\[
\begin{array}{rcl}
\alpha\to\beta & \equiv_{def} & \Xi(\mbox{\bf K}\alpha)(\mbox{\bf K}\beta), \mbox{\ where {\bf K}}\equiv_{def}\lambda xy.x ;\\
\top & \equiv_{def} & \Xi i i ;\\
\forall x\alpha & \equiv_{def} & \Xi (\mbox{\bf K}\top)(\lambda x.\alpha) ;\\
\bot & \equiv_{def} & \forall x x ;\\
\alpha = \beta & \equiv_{def} & \forall x(x\alpha\to x\beta) ;\\
!\alpha & \equiv_{def} & (\bot\to\bot) = \alpha .
\end{array}
\]}

�����Œ�`���ꂽ $\to$ �Ȃǂɂ��Ē��ώ�`�_�� NJ �̐��_�K�������̂܂ܔh���K���ɂȂ���
����B������, $\to$ �̓��� $\to i$ �ɂ��Ă�, ���X 1 �̉��肾���𗎂Ƃ����Ƃ��ł����
�����������t���B�܂�,�u!�v�͐��`�_���́u!�v�Ɏ��Ă��邪���`�_���́u!�v�̐�����S��
�͎����Ă��Ȃ��B

�u$\alpha = \beta$�v�ɂ��Ă͎��̐��_�K�����������B
{\[
\infer[k (=\to i)]{(\alpha = \beta)\to \gamma}{\infer*{\gamma}{\deduce{\alpha = \beta}{k}}} .
\]}
������, ($=\to$i) �ɂ����ĉ���͂����ł����Ƃ���B

�u!�v�ɂ��Ă͎��� 2 �̐��_�K�����������B
\[
\infer[!e]{\alpha}{\deduce{!\alpha}{\Pi}}, \hspace{7mm}
\hspace{7mm} \infer[k(!\to i)]{!\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{!\alpha}{k}}}} �B
\]
������, (!$\to$i) �ɂ����ĉ���͂����ł����Ƃ���B

$Q$ �� $\lambda x.(\neg !xx)$ �̏ȗ��L���Ƃ���B��̓���������K���ł��邱�Ƃ��g����,
���̂悤�� $QQ$ �ł��邱�Ƃ�������B
\[
\infer[\beta]{QQ}{\infer[1 (!\to i)]{\neg !QQ}{\infer[\to e]{\bot}{
		\infer[\beta]{\neg !QQ}{
			\infer[!e]{QQ}{\deduce{!QQ}{1}}} 
		& \deduce{!QQ}{1} }}}
\]
�܂�{�N���X $Q$ �͎������g�����Ƃ��Ċ܂�}�̂ł���B

���́u!�v�͐��`�_���́u!�v�Ƃ悭��������������, �S�������ł���� $BCK\beta$ ���������邱�ƂɂȂ�̂�,
������������قȂ�_�����邱�Ƃ�������B�u!�v�͗l���T�O�̈��ł��邪, {���̑̌n�łǂ̂悤�ȗl��
�T�O����`�ł���̂�}�Ƃ������Ƃ�����������ł���B

�k��K�����Ȃ���Ζ������ȕ�����������W���_���������Ȃ����Ƃɍŏ��ɋC�t�����̂�
 Gri\v{s}in\cite{Grisin1974} �ł������B
����ɊO�����������k��K���𓱂������𓱏o���邱�Ƃ�������(\cite{Grisin1982})�B
U. Petersen\cite{Petersen2000} �̎d������͑S�̏W���ɂ��Ă̊O���������Ŗ������o�Ă��邱�Ƃ�
�M����B�Ƃ��낪�ŋ�, ��W���̂悤�ȏ����ȏW���̊O���������Ŗ����������o�����Ƃ������Ƃ�
���������B

�܂�, BCK �_���ł����̌`�̓�d�ے����������K�����h���K���ł���B�ؖ��͒��ώ�`�_���ɂ�����
�h���K���ł��邱�Ƃ̏ؖ��Ɠ����ł���B
\[\infer[D]{\neg \alpha}{\neg\neg\neg\alpha}
\]
�܂�, ��W���ɂ��Ă̊O�����͎��̂悤�ɏq�ׂ邱�Ƃ��ł���B$\neg\alpha$ ������Ȃ��ŏؖ�
�\�ȂƂ�, $\bot\to\alpha$ ����� $\alpha\to\bot(\equiv \neg\alpha)$ ���Ƃ��ɉ���Ȃ���
�ؖ��\�ł���B���̌���, �W�� $\lambda x.\bot$ �ɂ��Ă̊O������
$(\lambda x.\bot)=(\lambda x.\alpha)$ �ƂȂ�B$\lambda x.\bot$ �͋�W���ł���̂�, ��W����
���Ă̊O������F�߂�Ƃ������Ƃ�, ���̋K����F�߂�Ƃ������Ƃł���B
\[\infer[ext2]{(\lambda x.\bot)=(\lambda x.\alpha)}{\neg\alpha}\]
���̐��_�}(���̒��� $\delta$ �ɂ��Ă� $\delta\equiv \lambda y.x(\lambda x.yu\to\bot)$)
�����Ă������������B
\[
\infer[\forall i]{!\neg\alpha}{
  \infer[\beta]{x(\bot\to\bot)\to x(\neg\alpha)}{
    \infer[\forall e]{(\delta (\lambda x.\bot))\to (\delta (\lambda x.\alpha))}{
      \infer[ext2]{(\lambda x.\bot)=(\lambda x.\alpha)}{\neg\alpha}
    }
  }
}
\]
���̋K�����玟�̋K�������e�K��(���肪���ׂė����Ă���Ƃ��̂ݎg����K��)�ł��邱�Ƃ�������B
\[\infer[ext]{!\neg\alpha}{\neg\alpha}\]

$R$ �� $\lambda x.(\neg !\neg\neg xx)$ �̏ȗ��L���Ƃ���B
���̂悤�� ��W���̊O�������g���Ɩ������������B
\[
\infer{\bot}{
\infer[1 (!\to i)]{\neg !\neg\neg RR}{\infer[\to e]{\bot}{
		\infer[D]{\neg !\neg\neg RR}{
		\infer[\beta]{\neg\neg\neg !\neg\neg RR}{
			\infer[!e]{\neg\neg RR}{\deduce{!\neg\neg RR}{1}}}} 
		& \deduce{!\neg\neg RR}{1} }}
    &
\infer[ext]{!\neg\neg RR}{
\infer[2(\to i)]{\neg\neg RR}{
\infer{\bot}{\deduce{\neg RR}{2}   &
\infer[\beta]{RR}{
      \infer[1 (!\to i)]{\neg !\neg\neg RR}{\infer[\to e]{\bot}{
		\infer[D]{\neg !\neg\neg RR}{
		\infer[\beta]{\neg\neg\neg !\neg\neg RR}{
			\infer[!e]{\neg\neg RR}{\deduce{!\neg\neg RR}{1}}}} 
		& \deduce{!\neg\neg RR}{1} }}
		}}}}}
\]
%
\section{�̌n $BCK\beta$ �ł̏W���_�̃V�~�����[�g}
%
�ÓT�_����̏W���_�͒��ώ�`�_��(��\{$\to, \bot, \forall$\}-�f��)��̏W���_�ŗe�ՂɃV�~�����[�g
�ł���(Glivenko �̒藝�ɂ��)�̂�, ���ώ�`�_����̏W���_�̃V�~�����[�g���l����B
���ώ�`�_����\{$\to, \bot, \forall$\}-�f�Ђ� NJ �ƌĂԂ��Ƃɂ���B�W���_�̌���Ƃ��Ă�
�񍀏q�� $\in$ �݂̂������̂��l����B

$!(i\alpha)$ �� $\alpha\to !\alpha$ �Ƃ����ꂼ�� $j\alpha$ �� $p\alpha$ �ƋL�����Ƃɂ���B
���Ȃ킿
$$ j\alpha\equiv !(i\alpha) \hspace{5mm} p\alpha\equiv\alpha\to !\alpha .$$

$\alpha$ �� NJ ��̘_�����Ƃ���B
$BCK\beta$ �̘_���� $\alpha^\circ$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B\\
{
$(\bot)^\circ \equiv \bot$, \ \ 
$(x\in y)^\circ \equiv yx$, \ \ 
$(\alpha \to \beta)^\circ \equiv \alpha^\circ \to \beta^\circ$, \ \ 
$(\forall x \alpha)^\circ \equiv \forall x (jx \to \alpha^\circ).$
}\\

�܂�, �ȉ��� 4 �_��������ׂ���� $\Delta$ �Ƃ���B
$$ j(\lambda x.\bot)$$
$$ !(\forall x \forall y (px\to py\to p(x \to y))) $$
$$ !(\forall x (\forall y (jy \to p(xy))) \to p(\forall y (jy\to xy))) $$
$$ !(\forall x \forall y (jx \to jy \to p(xy))) $$

���̒�`�� $j$ �Ȃǂ̉��߂��ȉ��̂悤�ɍl����Ɠǂ݂₷���B\\
{$jx$} �̈Ӗ��� {$x$ �͏W���ł���}, �� {$p\alpha$} �̈Ӗ��� {$\alpha$ �͖���ł���} �ł���B

�W���_�̘_�����̗� $\Sigma (\equiv \alpha_1, \alpha_2,...)$ (�Z������ł��悢) �ɂ�������
$\Sigma^\circ\equiv\alpha_1^\circ, \alpha_2^\circ,...$ �Ƃ���B
%
\begin{theorem}
{ $\Sigma$ ���W���_�̘_�����̗�, $\alpha$ ���W���_�̘_�����Ƃ����,
\[\Sigma\vdash_{NJ}\alpha \Longrightarrow \Sigma^\circ, \Delta\vdash_{BCK\beta}
 \alpha^\circ .\]}
\end{theorem}
���̒藝��
http://www.math.s.chiba-u.ac.jp/\~{}komori/masters\_thesis/2003/\\ takayama/takayama.dvi
�ɂ��鍂�R�}���F�̏C�m�_���̎�藝�Ɠ��l��(����������̕����Ղ���)�ؖ��ł���B���̍ۂɕ⏕
�藝�u�C�ӂ̏W���_�̘_���� $\alpha$ �ɂ�������, $\vdash_{BCK\beta} p\alpha^\circ$
�ł���v�����ƂȂ�B

���̒藝�̋t�͂܂��ؖ��ł��Ă��Ȃ��B�ÐX(\cite{Komori07-2})�ł�, {$\alpha$ �͖���ł���} ��
{$\alpha=!\alpha$} �Ƃ��Ă������t�̏ؖ��� {$\alpha$ �͖���ł���} �������ł̒�`���̗p
����ق����Ղ������ł���B������ɂ��Ă�, ���̏ؖ��ɂ̓��f�����g���K�v������Ǝv����B
���Ȃ킿, $\Sigma\not\vdash_{NJ}\alpha$ ������ Kripke ���f������
$\Sigma^\circ, \Delta\not\vdash_{BCK\beta} \alpha^\circ$ �������̌n $BCK\beta$ ��
���f��������Ă��΂悢�B
���ώ�`�_���� Kripke ���f���͂��Ȃ��݂̂��̂ł��邪, �̌n BCK$\beta$ �̃��f����
�ÐX(\cite{Komori89})�ɏq�ׂ��Ă���B
%\nocite{Komori07-3}
\bibliography{logic.bib}
\bibliographystyle{plain}
\end{document}
