\documentclass{jarticle}
%\documentclass[11pt]{jarticle}
% \usepackage{amsthm,amssymb}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newtheorem{definition}{��`}[section]
\newtheorem{theorem}[definition]{�藝}
%\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 4}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2004 �N 12 �� 14 �� (��)}
\begin{document}
\maketitle
�ȉ��ɂ�����, $\mathsb{I}$ �� $\mathsb{I}x \rhd x$ �� CLw �ŏؖ��\�ȕ��Ƃ���B
\begin{enumerate}
% 1
\item ��������(�̌n CLw �����ȏ��ƈ���Đ��_�K���������Ă��邱�Ƃɒ��ӂ���)�B
\[\mathsb{KI} \rhd_1 \mathsb{K} \vdash_{CLw} x = y\]
% 2
\item �� \ \ $\mathsb{S(KS)K}: (\beta\to\gamma)\to(\alpha\to\beta)\to\alpha\to\gamma$
		\ \ �� HK �̏ؖ��}���������B
% 3
\item $\lambda^* x.\mathsb{S}x\mathsb{I}$ ������, $(\lambda^* x.\mathsb{S}x\mathsb{I})M$ �̐��K�`�����߂�
(�ǂ�����r���o�߂���������)�B
% 4
\item $\lambda^\eta x.M$ �͎��y�[�W�̒�`\ref{eta}�Œ�`���ꂽ���̂Ƃ���B���̂Ƃ�, $\lambda^\eta xy. xyy$ ������,
$(\lambda^\eta xy. xyy)MN$ �̐��K�`�����߂�(�ǂ�����r���o�߂��������ƁB$\lambda^\eta xy.R$ ��
$(\lambda^\eta x.(\lambda^\eta y.R))$ �̂��Ƃł���)�B
\end{enumerate}
\newpage
\vspace{1cm}
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%

{\bf �̌n CLw} ��
�����^�͎��� 3 �ł�.
\[
\begin{array}{ll}
(\mathsb{K}) & \mathsb{K}MN \rhd_{1} M \\
(\mathsb{S}) & \mathsb{S}MNR \rhd_{1} MR(NR) \\
(\rho) & M \rhd M \\
\end{array}
\]

{\bf �̌n CLw} �̐��_�K���͎��� 6 �ł�:
\[
\infer[(\mu)]{MN \rhd_{1} MR}{N \rhd_{1} R},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{MR \rhd_{1} NR}{M \rhd_{1} N},
\]
\[
% \infer[(\kappa)]{M \rhd N}{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}.
\]

{\bf �ÓT����_��\index{���Ă�߂���������@�ÓT����_��}
(classical propositional logic)} HK �̌����^�͎��� 4 �ł�.
\[
\begin{array}{l}
\mathsb{K}: \alpha \to \beta \to \alpha \\
\mathsb{S}: (\alpha \to \beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma\\
\mathsb{P}: ((\alpha \to \beta) \to \alpha) \to \alpha \\
\mathsb{A}: \bot \to \alpha
\end{array}
\]

\begin{definition}[����]\em \ 
$M$ �� CL-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ��� $(\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)$ \ \ ($x\in FV(UV)$ �̂Ƃ�).
	\end{enumerate}
\end{definition}

\begin{definition}[����$\eta$]\label{eta}\em \ 
$M$ �� CL-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ��� $(\lambda^\eta x.M)$ ���ȉ��̂悤��
�A�[�I�ɒ�`����.
	\begin{enumerate}
		\item\label{1} $(\lambda^\eta x.M) \equiv (\mathsb{K}M)$ \ \ ($x \notin FV(M)$ �̂Ƃ�),
		\item $(\lambda^\eta x.x) \equiv \mathsb{I}$ \ \ (������ $\mathsb{I} \equiv \mathsb{SKK}$),
		\item\label{3} $(\lambda^\eta x. Ux) \equiv U$ \ \ ($x\notin FV(U)$ �̂Ƃ�).
		\item $(\lambda^\eta x. UV) \equiv \mathsb{S}(\lambda^\eta x.U)(\lambda^\eta x.V)$ \ \ (\ref{1} �� \ref{3}
		 ���K�p�ł��Ȃ��Ƃ�).
	\end{enumerate}
\end{definition}
\end{document}
