\documentclass{jarticle}
% \documentclass[11pt]{jarticle}
\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{lemma}[definition]{�⏕�藝}
\newtheorem{theorem}[definition]{�藝}
\newtheorem{proposition}[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{2011 �N 12 �� 13 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���ώ�`�q��_���̑̌n NJ �ƌÓT�q��_���̑̌n NK �ɂ���, �����������_�}��������:
  \begin{enumerate}
    \item $\forall x(\neg pxx\to pxy), \forall x(pxy\to\neg pxx)\vdash_{NJ} \bot$ ,
    \item $\forall x((px\to r)\to q), \forall x \, px\to q\vdash_{NK} q$ .
  \end{enumerate}
% 2
\item ���̘_�������ÓT�q��_���ŏؖ��ł��Ȃ����Ƃ�����:
  \begin{enumerate}
	\item $\forall x \forall y \forall z ( rxy \to ryz \to rxz )\to\forall x\, rxx \to
	  \exists x \forall y\,rxy\to\forall x \forall y ( \neg rxy \to ryx)$ ,
    \item $\forall x \forall y \forall z ( rxy \to ryz \to rxz ) \to \forall x \forall y \exists z
   (rxy\to (rxz\wedge rzy))\to\exists x\forall y\,rxy\to\exists x \, rxx$ .
 \end{enumerate}
%\vspace{2mm}
% 3
\item 
���ώ�`�q��_�� HJ �̉�㈒藝 �u$x:\alpha,\Gamma \vdash_{HJ} M:\beta$ \ \ ���� \ \ $\Gamma$ \ \ �̎�
���ɕϐ� $x$ ������Ȃ��Ȃ�� \ \ 
$\Gamma \vdash_{HJ} \lambda^* x.M:\alpha \to \beta$ \ \ �ł���v�� $\lambda^* x.M$ �̒�`�ɂ��A�[
�@�ŏؖ�����B
%\vspace{5mm}
\end{enumerate}
\vspace{10mm}
%\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\bf �ÓT�q��_�� NK} �̐��_�K���͎��� 6 �ł��B
\[ \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} \hspace{5mm} \]
\[ \infer{\mathsb{J}M: \forall x \alpha}{M: \alpha} \hspace{5mm}
 \infer{\mathsb{F}M: [t/x]\alpha}{M: \forall x \alpha} \hspace{5mm}
 \infer{\mathsb{D}M:\alpha}{M:\neg\neg\alpha}\ \ . \]

\begin{definition}[�\��(structure)]\label{def-structure}\em
���� $\cal L$ �̍\�� $\cal A$ �͎��� 3 �̂��̂���\������Ă��܂�:
\begin{enumerate}
\item $\cal A$ �̐��E�ƌĂ΂���łȂ��W�� $|\cal A|$.
	$|\cal A|$ �̌��� $\cal A$ �̌̂Ƃ����܂�.
\item ���� $\cal L$ �̊e�X�� $n$ �ϐ��֐��L�� $f$ �ɑ΂���, $|\cal A|$ ����
 $|\cal A|$ �ւ� $n$ �ϐ��֐� $f_{\cal A}$.
 (�Ƃ���, 0 �ϐ��֐��L�� $e$ �ɑ΂���, $e_{\cal A}$ �� $\cal A$ �̌̂ł�.)
\item ���� $\cal L$ �̊e�X�� $n$ �ϐ��q��L�� $p$ �ɑ΂���, $|\cal A|$ �� $n$
 �̒��� $|{\cal A}|^n$ �̕����W�� $p_{\cal A}$.
\end{enumerate}
\end{definition}

���� $\cal L$ �� $\cal A$ �̌̂̑S�Ă̖��O��t�������ē����錾��
�� $\cal L(A)$ �Ə����܂�. �� $c$ �̖��O�� $\bar{c}$ �Ə����܂�. 

$t$ ������ $\cal L(A)$ �̕��Ƃ��܂�. ���� ${\cal A}$ �̌� ${\cal A}(t)$
 ���A�[�I�ɒ�`���܂�.
\begin{enumerate}
\item ${\cal A}(\bar{c}) = c$,
\item ${\cal A}(ft_1...t_n) = f_{\cal A}({\cal A}(t_1),...,{\cal A}(t_n))$.
\end{enumerate}

$\alpha$ ������ $\cal L(A)$ �̕_�����Ƃ��܂�. ���� $\alpha$ �̐^�U�l
 ${\cal A}(\alpha)$ ���A
�[�I�ɒ�`���܂�.
\begin{definition}\em \ 
\begin{enumerate} 
\item ${\cal A}(pt_1...t_n) = \top \Longleftrightarrow p_{\cal A}
({\cal A}(t_1),...,{\cal A}(t_n))$,
\item ${\cal A}(\bot) = \bot$,
\item ${\cal A}(\alpha \to \beta) = {\cal A}(\alpha) \to {\cal A}(\beta)$,
\item ${\cal A}(\forall x \alpha) = \top \Longleftrightarrow 
{\cal A} �̔C�ӂ̌� c �ɑ΂��� {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{definition}

\begin{theorem}\em \ 
�������藧���Ă���:
\begin{enumerate} 
\item ${\cal A}(\neg\alpha) = \top \Longleftrightarrow {\cal A}(\alpha) = \bot$,
\item ${\cal A}(\alpha\wedge\beta) = \top \Longleftrightarrow {\cal A}(\alpha) = \top
   ���� {\cal A}(\beta) = \top$,
\item ${\cal A}(\exists x \alpha) = \top \Longleftrightarrow 
{\cal A} �̂���� c �ɑ΂��� {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{theorem}

\begin{definition}[����]\label{def-abstract}\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. \mathsb{J}U) \equiv \mathsb{G(J}(\lambda^* x.U))$,
		\item $(\lambda^* x. UV) \equiv \mathsb{S}(\lambda^* x.U)(\lambda^* x.V)$ \ .
	\end{enumerate}
\end{definition}

\end{document}
