\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{2007 �N 5 �� 22 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item\label{1} 
\begin{enumerate}
  \item $\vdash_{NJ} ((\alpha \to \beta) \to \alpha) \to \neg\neg\alpha$
    ������(���Ȃ킿, �� $M: ((\alpha \to \beta) \to \alpha) \to \neg\neg\alpha$
     �� NJ �ŏؖ��\�ƂȂ�� $M$ ������, ���̎��̏ؖ��}��������)�B
  \item\label{2}
    $\vdash_{NJ} (\alpha\to\neg\neg\beta)\to\neg\neg(\alpha\to\beta)$ \ \ \ �������B
  \item\label{3}
    $\vdash_{NJ} \neg\neg\neg\alpha\to\neg\alpha$ \ \ �������B
  \item\label{4}
    $\vdash_{NJ} \neg\neg(\alpha\to\gamma)\to\neg\neg\alpha\to\neg\neg\gamma$ \ \ �������B
\end{enumerate}
\vspace{4mm}
% 2
\item ��� \ref{2}, \ref{3}, \ref{4} �ŋ��߂������_�������ꂼ�� $T, U, V$ �Ƃ���B\\
  �܂�, $\Gamma \vdash_{NK} M:\gamma$ �Ƃ���B�萔 $\mathsb{D}$ ���܂ނ����m��Ȃ������_�� $M$ �ɑ΂���,
  $\mathsb{D}$ ���܂܂Ȃ������_�� $M^j$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B
\begin{enumerate}
  \item $x^j \equiv \lambda y.yx \ ,$
  \item $(\mathsb{D}N)^j \equiv UN^j \ ,$
  \item $(\mathsb{A}N)^j \equiv (\lambda x.\mathsb{A}(x(\lambda x.x)))N^j \ ,$
  \item $(NR)^j \equiv VN^jR^j \ ,$
  \item $(\lambda x.N)^j \equiv T(\lambda x.N^j) \ .$
\end{enumerate}
���̂Ƃ�, $\Gamma \vdash_{NJ} M^j:\neg\neg\gamma$ �ł��邱�Ƃ�
  �����_�� $M^j$ �̒�`�ɂ��Ă̋A�[�@�ŏؖ�����B(�̌n NK �̒�`�͎��y�[�W�ɂ���B)
\vspace{4mm}
% 3
\item $(\lambda xyz.xz(yz))(\lambda x.zx) \equiv_\alpha (\lambda zyx.zx(yx))(\lambda y.zy)$ ������
	�̌n $\lambda\alpha$ �̏ؖ��}���������B
% 4
\item $V\equiv \lambda y.x(yy)$, $\mathsb{Y}\equiv\lambda x.VV$ �Ƃ���B���̂Ƃ�
	$\mathsb{Y}x =_\beta x(\mathsb{Y}x)$ �ł��邱�Ƃ�����($\vdash_{\lambda\beta}
	\mathsb{Y}x = x(\mathsb{Y}x)$ �������ؖ��}�͂������Ȃ��Ă��悢)�B
\end{enumerate}
\newpage
{\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}  \ \ .\]

{\bf �ÓT����_��}\index{���Ă�߂���������@�ÓT����_��} NK �͑̌n NJ �Ɏ���
��d�ے�̏����K����t�����������̂ł���:
\[ \infer{\mathsb{D}M:\alpha}{M:\neg\neg\alpha}\ \ . \]

\begin{definition}[{\bf ���\index{�����ɂイ@���}(substitution)}]\label{sub}\em \ 
$M, N$ �������_��, $x$ ��ϐ��Ƃ���. $M$ �̒���(���R�Ɍ����) $x$ �� $N$ ������������
$[N/x]M$ �����̂悤�ɋA�[�I�ɒ�`����.
	\begin{enumerate}
		\item\label{sub1} $[N/x]x \equiv N$ ,
		\item\label{sub2} $[N/x]M \equiv M$ \ \ ($x \notin FV(M)$ �̂Ƃ�),
		\item\label{sub3} $[N/x](QR) \equiv ([N/x]Q\ [N/x]R)$ \ \ ($x \in FV(QR)$ �̂Ƃ�),
		\item\label{sub4} $[N/x](\lambda y.Q) \equiv \lambda y.[N/x]Q$ \ \ ($x \in FV(Q)$ ���� $y\notin FV(N)$ ��
		�Ƃ�),
		\item\label{sub5} $[N/x](\lambda y.Q) \equiv \lambda z.[N/x][z/y]Q$ \ \ ($x \in FV(Q)$ ���� $y\in FV(N)$
		�̂Ƃ�).
	\end{enumerate}
	������ $y\not\equiv x$ �͉��肳��Ă���. �܂�, $z$ �� $V(N(\lambda y.Q))$ �̒��ɂ͂Ȃ��ŏ��̕ϐ��ł���
	(�ϐ��� '$u_0$', '$u_1$', '$u_2$',... �̏��ɕ��ׂ��Ă��܂�).
\end{definition}

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