\documentclass{slides}
\usepackage{graphicx, color, myhyper}
\usepackage{proof}
\usepackage{amsthm,amssymb}
\usepackage{latexsym}
\usepackage{proof}
\def\pause{\special{pause}}
\newcommand{\arrow}{\hspace{-0.2em}\rightarrow\hspace{-0.2em}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}

\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}

\paperwidth=10.24in
\paperheight=7.68in
\textwidth=9in
\textheight=6.6in
\voffset=-.9in
\hoffset=-.48in

\title{$\alpha$���l�Ș_�����𓯈ꎋ���Ȃ��Ƃ��̏q��_���̐��K���藝}
\special{dviout `keep y}
%  1024 x 768, general screen, cover sheet On, cover bottom, Presentation;
%  Fit
\special{dviout -e=0 -y=XGAP !AN0N5NP!w!p;!bdf}
\pagecolor[rgb]{1,1,0.8}% slightly yellow
%}
\author{�ÐX�Y��(��t��w)}
\date{}
\begin{document}
%\pagestyle{empty}
\maketitle
%\thispagestyle{empty}
http://komoriyuichi.web.fc2.com/masters\_thesis/ \\
�ɂ��� �u�֘A���_: $\alpha$���l�Ș_�����𓯈ꎋ���Ȃ��Ƃ��̏q��_���̐��K���藝�v
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
�u���Ȋw�ɂ�����_��(�V��)�v(���슰��)�ł� cut �Ȃ��̏ؖ��}�͂Ȃ��Ƃ���
���邪�ԈႢ��, ���� cut �Ȃ��̏ؖ��}�������B�u�����_���w�v(������)�ł� cut �Ȃ�
�̏ؖ��}�͂Ȃ��Ƃ��Ă���ÐX�ɂ���(�����ϐ���ς��đ�����s�����Ƃ������Ă��Ȃ���
�Ő�����)�B�ǂ�������R��� NJ �ōl��, ���ȒP�Ȃ��̂ɂ���Ƃ̎��̐��_�}�ɂȂ�B
\[\infer{pyx}{\infer{\forall u \,pux}{\infer{pzx}{\infer{\forall y \,pzy}
   {\forall x\forall y \,pxy}}}}
\]

���� NJ �̐��_�}���ɑ�_���� $\forall u \,pux$ �������ό`������ƈȉ��̂悤�ɂȂ�B
\[\infer{pyx}{\infer{\forall x \,pyx}{\forall x\forall y \,pxy}}
\]
������, $[y/z]\forall y \,pzy\equiv\forall x \,pyx$ �Ƃ����B����͈ꌩ, ���K�Ȑ��_�}�Ɍ����邪
$[y/x]\forall y \,pxy\equiv\forall z \,pyz$ �Ƃ����, ���_�}�ɂȂ��Ă��Ȃ��B
\end{slide}
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
������, �����O���
���_�������̂悤�Ȑ��K�Ȑ��_�}������B
\[\infer{pyx}{\infer{\forall z \,pyz}{\forall x\forall y \,pxy}}
\]

��ʂ�, $\alpha$���l�Ș_�����𓯈ꎋ���Ȃ����R��㈂̑̌n�ł�, �ؖ��ł���_�����̐��K�ȏؖ��}������
����B

���, �u���㐔���_���w�����v(�ÐX, ����) �ł� NJ �� $\forall$-int �����̌`�ɂȂ��Ă���B
\[ \infer{\forall x\alpha}{\alpha} \]
����́u���Ȋw�ɂ�����_���v�� NJ ���ア�̌n�ƂȂ��Ă���B���̎ア�̌n�� NJ\_ �Ƃ�,
�Ή����� sequent �̑̌n�� LJ\_ �Ƃ���BLJ �� cut �����藝�� NJ ���K���藝�̊Ԃɂ͖��ڂȊ֌W������,
LJ �� cut �Ȃ��̏ؖ��}�ɑΉ����� NJ �̐��_�}�͐��K�Ȑ��_�}�ł���, NJ �̐��K�Ȑ��_�}�ɑΉ����� LJ ��
�ؖ��}�� cut �̂Ȃ��ؖ��}�ƂȂ��Ă���B
\end{slide}
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
������, NJ\_ �̐��K�Ȑ��_�}�ɑΉ����� LJ\_ �̏ؖ��}�� cut �Ȃ�
�ؖ��}�ł��邪, LJ\_ �� cut �Ȃ��̏ؖ��}�ɑΉ����� NJ\_ �̐��_�}���ǂ������_�}�ƂȂ�Ȃ��ꍇ������B
���� LJ$_-$ �� cut �Ȃ��̏ؖ��}�ɑΉ����� NJ\_ �̐��_�}���ǂ��͐��_�}�Ƃ͂Ȃ��Ă��Ȃ��B
\[
\infer{qx\supset r,  qx,  \forall x(r\supset px)\rightarrow \forall x \,px}
       {qx\rightarrow qx
        &
      \infer{r,  \forall x(r\supset px)\rightarrow \forall x \,px}
            {\infer={r,  \forall x(r\supset px)\rightarrow px}{\infer{r\supset px,  r\rightarrow px}
      {r\rightarrow r &  px\rightarrow px}}
           }}
\]
�Ή����� NJ\_ �̐��_�}���ǂ�
\[\infer{\forall x \,px}{\infer{px}{\infer{r\supset px}{\forall x(r\supset px)} & \infer{r}{qx\supset r & qx}}}
\]
�܂�, $qx\supset r,  qx,  \forall x(r\supset px)\vdash_{NJ\_} \forall x \,px$ 
���������K�Ȑ��_�}�����݂��Ȃ����Ƃ��ؖ��ł���B
\end{slide}
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
���� NJ\_ �ł͐��K�Ȑ��_�}���Ȃ���ł���B����ɑΉ����� LJ\_ �̏ؖ��}�� cut ���������邱�Ƃ͂ł��Ȃ���, ���_
�Ɏ��� cut �Ȃ��� LJ\_ �̏ؖ��}�����݂��Ȃ��B
\[\infer{\forall z\,pz}{\infer[\lambda u]{\forall x\,px\to\forall z\,pz}{\infer{\forall z\,pz}{\infer{pz}
                 {u:\forall x\,px}}} & \infer{\forall x\,px}{\infer{px}{\infer{pz\to px}
                                      {\forall x(pz\to px)} & pz}}}
\]
\end{slide}
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
\begin{enumerate}
\item $\Gamma\vdash_{NJ\_}\gamma$ ���������K�Ȑ��_�}�����݂��邽�߂�
      $\Gamma, \gamma$ �̖������ׂ��ǂ��\�������͉���?
\item �K�� $\forall$-int �����̂悤�ɕς���Ɛ��K���藝�����藧��?:
\[ \infer[\mbox{ ������ }\beta\equiv_\alpha\forall x\alpha]{\beta}{\alpha} \] 
\end{enumerate}
\end{slide}
\begin{slide}
\pagecolor[rgb]{1,1,0.8}%
\begin{enumerate}
\item 
\item �ɂ��Ă͑�������������\�ȂƂ��͑����ϐ��̒u�������������ɂ��̂܂ܑ������
      �悤�Ȓ�`�Ȃ�ΐ��藧���Ă���B
\end{enumerate}
\end{slide}
\end{document}
