\documentclass[11pt]{jarticle}
\usepackage{latexsym}
%\usepackage{proof2}
\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}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔊w\Romannumeral{1}  ���� 1}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2006 �N 4 �� 25 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item\label{c-p1.1} �� \ \ $\mathsb{S}(\mathsb{K}x)yz \rhd x(yz)$ \ \ �Ɏ��� CLw �̏ؖ��}������.
%\vspace{7mm}
% 2
\item �� \ \ $\mathsb{S}(\mathsb{KS})\mathsb{K}xyz \rhd x(yz)$ \ \ ���̌n CLw �ŏؖ��\�ł��邱�Ƃ�����(�K�������ؖ��}
	��`���Ȃ��Ă��悢).
%\vspace{7mm}
% 3
\item ��������(������, $\mathsb{I}$ �� $\mathsb{I}x \rhd x$ �� CLw �ŏؖ��\�ȕ��Ƃ���).
	\[\mathsb{KI} \rhd_1 \mathsb{K} \vdash_{CLw} x = y\]
%\vspace{7mm}
% 4
\item
	\begin{enumerate}
		\item �� \ \ $\mathsb{S(KK)}: (\alpha\to\beta)\to\alpha\to\gamma\to\beta$
		\ \ �� HK �̏ؖ��}��������.
		\item\label{p1.2} �� \ \ $\mathsb{S(KP)}: (\beta\to\neg\alpha\to\alpha)\to\beta\to\alpha$ \ \ �� HK �̏ؖ�
		�}��������.
	\end{enumerate}
\end{enumerate}
\newpage
�̌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}
\]

�ؖ��}�͌�����t�Ƃ���؏�̐}�`�ł�. �ؖ��}����邽�߂̋K����
{\bf ���_�K��\index{������񂫂���@���_�K��}(rule of inference)}�Ƃ����܂�. 
 �̌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}.
\]
\\[1cm]

{\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}
\]

\end{document}
