\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \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}}}
\title{��񐔊w\Romannumeral{1}  ���� 3}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2011 �N 5 �� 31 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 
\item\label{1} 
$\lambda^* xy.xy$ ������, $(\lambda^* xy.xy)xy$ �̐��K�`�����߂�(���ʂ����łȂ��r���o�߂�
��������).
\vspace{4mm}
% 2
\item\label{2} 
���̘_�����ɂ���, �u$M: \mbox{�_����}$�v ���̌n NJ �ŏؖ��ł���悤�ȕ����_�� $M$ ������,
 �u$M: \mbox{�_����}$�v �� NJ �̏ؖ��}��`���B�ȗ��`�ŏؖ��}�������ꍇ��, �����_�� $M$ �𖾋L
 ���邱��.
\begin{enumerate}
  \item\label{2}
    $(\alpha\to\beta\to\gamma)\to\beta\to\alpha\to\gamma$
  \item $((\alpha \to \beta) \to \alpha) \to \neg\neg\alpha$
  \item\label{3}
    $((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \neg\neg\alpha$
  \item\label{4}
    $\neg\neg(((\alpha \to \beta) \to \beta) \to (\beta \to \alpha) \to \alpha)$
\end{enumerate}
\vspace{4mm}
% 3
\item $(\lambda zyx.z(yx))(\lambda z.yz) \equiv_\alpha (\lambda xyz.x(yz))(\lambda x.yx)$ ������
	�̌n $\lambda\alpha$ �̏ؖ��}���������B
% 4
\item ���������D
\[
\lambda xy.x \rhd_1 \lambda x.x \vdash_{\lambda\beta} x = y
\]
\end{enumerate}
\newpage
\noindent
{\bf ���ώ�`����_��(intuitionistic propositional logic)} NJ �̐��_�K���͎��� 3 �ł���:
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha} \ \ , \hspace{5mm}
\infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}} \ \ , \hspace{5mm}
\infer{\mathsb{A}M:\alpha}{M:\bot}  \ \ .\]

\begin{definition}[����]\label{def-abstract}\em \ 
$M$ �� CL-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ� CL-�� $(\lambda^* x.M)$ ���ȉ��̂悤��
�A�[�I�ɒ�`����.
	\begin{enumerate}
		\item $(\lambda^* x.M) \equiv (\mathsb{K}M)$ \ \ ($x \notin FV(M)$ �̂Ƃ�),
		\item $(\lambda^* x.x) \equiv \mathsb{I}$ \ \ (������ $\mathsb{I} \equiv \mathsb{SKK}$),
		\item $(\lambda^* x. UV) \equiv \mathsb{S}(\lambda^* x.U)(\lambda^* x.V)$ \ .
	\end{enumerate}
\end{definition}
\vspace{4mm}
{\bf �̌n $\lambda\alpha$ �̌����^}�͎��� 1 �ł�:
\[
\begin{array}{crcl}
(\rho) & M & = & M .\\
\end{array}
\]
%
{\bf �̌n $\lambda\alpha$ �̐��_�K��}�͎��� 2 �ł�(�K�� $\alpha$ �� $x\equiv y$ �̎����g����):
\[
\infer[(\tau)]{MN = UV}{M = U & N = V},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\alpha)\ (\mbox{������} z\notin V((\lambda x.M)(\lambda y.N)))]{\lambda x.M = \lambda y.N}{[z/x]M = [z/y]N} .
\]
%
{\bf �̌n $\lambda\beta$ �̌����^�͎��� 2 �ł�:
\[
\begin{array}{lcccl}
(\beta) & (\lambda x.M)N & \rhd_{1} & [N/x]M, & \\
(\rho) & M & \rhd & N & (\mbox{ ������ } M\equiv_\alpha N).\\
\end{array}
\]
%
{\bf �̌n $\lambda\beta$ �̐��_�K��}�͎��� 8 �ł�:
\[
\infer[(\mu)]{MN \rhd_{1} MR}{N \rhd_{1} R},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{MR \rhd_{1} NR}{M \rhd_{1} N},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\xi)]{\lambda x.M \rhd_{1} \lambda x.N}{M \rhd_{1} N},
\]
\[
\infer[(\kappa 1)\ \ (\mbox{ ������ } R\equiv_\alpha N)]{M \rhd_1 R}{M \rhd_{1} N}, \ \ \ \ \ \ \ \ \ 
\infer[(\tau)]{M \rhd R}{M \rhd_{1} N & N \rhd R},
\]
\[
\infer[(\kappa)]{M = N}{M \rhd N}, \ \ \ \ \ \ \ \ \ 
\infer[(\sigma)]{N = M}{M = N}, \ \ \ \ \ \ \ \ \ 
\infer[(\tau=)]{M = R}{M = N & N = R}.
\]
\end{document}
