\documentclass[12pt]{jarticle}
\setlength{\textwidth}{145truemm}
\setlength{\textheight}{230truemm}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
%\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
% \pagestyle{empty}
\newtheorem{definition}{��`}[section]
\newtheorem{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{corollary}[definition]{�n}
\newtheorem{proposition}[definition]{����}
\newtheorem{example}[definition]{��}
\newtheorem{remark}[definition]{����}
\newtheorem{conjecture}[definition]{�\�z}
\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
% \newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{�ϐ�����ʂ��Ȃ��Ƃ��� Gentzen �̊�{�藝}
\author{�ÐX�Y��(��t��w)}
\date{}
\begin{document}
\pagestyle{empty}
\maketitle
\thispagestyle{empty}
Gentzen �͕ϐ������R�ϐ��Ƒ����ϐ��ɕ�����Ă��錾��Ŋ�{�藝���ؖ����Ă���B
������Ă��Ȃ�����Ŋ�{�藝���ؖ�����ɂ͒��ӂ��K�v�ł���B���� cut �����ؖ��}
�����ė~�����B
\[\infer[(cut)]{\forall x\forall y p(x,y)\rightarrow p(y,x)}
  {\infer{\forall x\forall y p(x,y)\rightarrow\forall u p(u,x)}
           {\infer{\forall x\forall y p(x,y)\rightarrow p(z,x)}
             {\infer{\forall y p(z,y)\rightarrow p(z,x)}{p(z,x)\rightarrow p(z,x)}}} & 
   \infer{\forall u p(u,x)\rightarrow p(y,x)}{p(y,x)\rightarrow p(y,x)}}
\]
���� cut �� Gentzen �̕��@�ł͎�邱�Ƃ��ł��Ȃ��B������, ���_\\
$\forall x\forall y p(x,y)\rightarrow p(y,x)$
�Ɏ��� cut �Ȃ��̏ؖ��}�͑��݂���B�u���Ȋw�ɂ�����_��(�V��)�v(���슰��)�ł� cut �Ȃ��̏ؖ��}�͂Ȃ��Ƃ���
���邪�ԈႢ�B�u�����_���w�v(������)�ł�cut �Ȃ��̏ؖ��}�͂Ȃ��Ƃ��Ă��邪, �����ϐ���ς��đ�����s������
�������Ă��Ȃ��̂Ő������B�����ł̘b�͑����ϐ���ς��đ�����s�����Ƃ������̌n�̘b�ł���B

���� LJ �̏ؖ��}�ɑΉ����� NJ �̐��_�}�͎��̂悤�ɂȂ�B
\[\infer{p(y,x)}{\infer{\forall u p(u,x)}{\infer{p(z,x)}{\infer{\forall y p(z,y)}
   {\forall x\forall y p(x,y)}}}}
\]
���̂悤�Ɏ��R��㈂̑̌n�̂ق����Z���Đ��������₷���{���͕ς��Ȃ��̂� NJ �̐��K���藝�̖���
���Đ�������B

���� NJ �̐��_�}���ɑ�_���� $\forall u p(u,x)$ �������ό`������ƈȉ��̂悤�ɂȂ�B
\[\infer{p(y,x)}{\infer{\forall x p(y,x)}{\forall x\forall y p(x,y)}}
\]
������, $[y/z]\forall y p(z,y)\equiv\forall x p(y,x)$ �Ƃ����B����͈ꌩ, ���K�Ȑ��_�}�Ɍ����邪
$[y/x]\forall y p(x,y)\equiv\forall z p(y,z)$ �Ƃ����, ���_�}�ɂȂ��Ă��Ȃ��B������, �����O���
���_�������̂悤�Ȑ��_�}������B
\[\infer{p(y,x)}{\infer{\forall z p(y,z)}{\forall x\forall y p(x,y)}}
\]

��ʂ�, �ϐ�����ʂ��Ȃ����R��㈂̑̌n�ł�, �ؖ��ł���_�����̐��K�ȏؖ��}�����݂���B�{�����ł�
���̏ؖ��̊T�����q�ׂ�B
%
\begin{enumerate}
\item �^����ꂽ���_�} M �ɂ�������, �����ϐ��Ǝ��R�ϐ��Ɏg����ϐ��𕪗��������_�} N �����BN �̉���
      ���_�� M �̉���ƌ��_���� $\alpha$�ϊ����ē�������̂ƂȂ��Ă���B
\item ���_�} N �𐳋K�` P �ɕό`����BP �̉���ƌ��_�� N �Ɠ����ł���B
\item ���K�Ȑ��_�} P ������ M �̉���ƌ��_���������K�Ȑ��_�} Q �����B
\end{enumerate}

���ڂ������Ƃ͉��L�ɂ��� �u�֘A���_: �ϐ�����ʂ��Ȃ��Ƃ��̎��R��㈑̌n NJ �̐��K�`�藝�v
�������������B\\
http://komoriyuichi.web.fc2.com/masters\_thesis/

�u�ϐ�����ʂ��Ȃ���㈂̑̌n�ł�, �ؖ��ł��鐄������_������ cut �Ȃ��̏ؖ��}�␳�K�ȏؖ��}������
����v�Ƃ��������ɂ͍��쓹�v(�V����)���񂪑啪�O�ɋC�Â��Ă����悤�ł���B
\end{document}
