%\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{theorem}[definition]{�藝}
%\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 2}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2003 �N 10 �� 28 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item �_���� \ \ $((\alpha \to \beta) \to \beta\to\alpha) \to \beta \to \neg\neg\alpha$
 \ \ �̖���_���̑̌n NJ �̏ؖ��}���������B
% 2
\item �_���� \ $\forall x(px\to q)\to\exists x\, px\to\neg\neg q$
 \ �̏q��_���̑̌n NJ �̏ؖ��}��������.
% 3
\item ������ $ \forall x \forall y \forall z ( rxy \to ryz \to	rxz ), 
	\forall x \exists y \, rxy \ra \exists x \, rxx$
	���̌n LK �ŏؖ��ł��Ȃ����Ƃ�����.
%\item ������ $ \forall x\ rxx \ra \forall x \forall y \forall z ( rxy \to rxz \to
%	\neg ryz \to rzy)$
%	���̌n LK �ŏؖ��ł��Ȃ����Ƃ�����.
%\vspace{5mm}
% 4
\item �ȉ���(�R���p�N�g���藝������)���藝���g���ăR���p�N�g���藝���ؖ�����.
\end{enumerate}
%\newpage
\vspace{2cm}
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
\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 
�C�ӂ� {\cal A} �̌� c �ɑ΂��� {\cal A}([\bar{c}/x]\alpha) = \top$.
\end{enumerate}
\end{definition}

\begin{theorem}\label{the-infinite2finite}\em
������ $\Gamma \ra \Theta$ �� LK �ŏؖ��\�Ȃ��, $\Gamma$ �� $\Theta$ ��
���ꂼ��̗L�������W�� $\Gamma'$ �� $\Theta'$ �����݂��� $\Gamma' \ra \Theta'$
�� LK �ŏؖ��\�ł���.
\end{theorem}

$\Gamma \ra \Theta$ ������ $\cal L$ �̕������Ƃ��܂�. �S�Ă� $\alpha \in
 \Gamma$ �ɂ��� ${\cal A}(\alpha) = \top$ �̂Ƃ��ɂ�, ���� $\beta \in \Theta$
 �����݂��� ${\cal A}(\beta) = \top$ �ƂȂ�Ƃ�, ������ $\Gamma \ra \Theta$
 �� $\cal A$ �Ő������Ƃ����܂�.

$\Gamma \ra \Theta$ ������ $\cal L$ �̐������Ƃ��܂�. $\Gamma \ra \Theta$ ��
���R�Ɍ����̕ϐ��̑S�Ă� $y_1,...,y_n,...$ �Ƃ��܂�. ��
��, $t_1,...,t_n,...$  ��
���� $\cal L(A)$ �̕��Ƃ��܂�.  $\Gamma \ra \Theta$ ��
���R�ϐ� $y_1,...,y_n,...$ �� $t_1,...,t_n,...$ �����ꂼ�������ē�����
���� $\cal L(A)$ �̕�������
 $\Gamma \ra \Theta$ �� $\cal A$-{\bf �����} �Ƃ����܂�.  $\Gamma \ra \Theta$ �̔C�ӂ�
 $\cal A$-����� $\Gamma' \ra \Theta'$ �� $\cal A$ �Ő������Ƃ�,
 ������ $\Gamma \ra \Theta$ �͍\�� $\cal A$ �Ő������Ƃ����܂�.

$\Gamma \ra \Theta$ ������ $\cal L$ �̐������Ƃ��܂�. $\cal L$ �̔C�ӂ̍\
�� $\cal A$ �� $\Gamma \ra \Theta$ ���������Ƃ�, $\Gamma \ra \Theta$ ��
{\bf �P�^}�ł���Ƃ����܂�.
%
\begin{theorem}[LK �̌��S���藝]\label{the-LK-kenzen}\em
������ $\Gamma \ra \Theta$ �� LK �ŏؖ��ł����, $\Gamma \ra \Theta$ ��
�P�^�ł���.
\end{theorem}

������ $\Gamma \ra \Theta$ ���P�^�łȂ���
��, ����\�� $\cal A$ �� $\Gamma \ra \Theta$ �� $\cal A$-�����
 $\Gamma' \ra \Theta'$ �����݂���, �S�Ă� $\alpha \in \Gamma'$ �ɂ���
 ${\cal A}(\alpha) = \top$ �� �S�Ă�
 $\beta \in \Theta'$ �ɂ��� ${\cal A}(\beta) = \bot$ �ƂȂ��Ă���Ƃ��ł�.
 ���̂悤�ȍ\�� $\cal A$ �� $\cal A$-����� $\Gamma' \ra \Theta'$ �̑�
 $<{\cal A},\Gamma' \ra \Theta'>$ �𐄌��� $\Gamma \ra \Theta$ ��{\bf ����
}�Ƃ����܂�. 

\begin{theorem}[LK �̋����S���藝]\label{z:the_completeness}\em
������ $\Gamma \ra \Theta$ ���P�^�Ȃ�� $\Gamma \ra \Theta$ ��
�̌n LK �ŏؖ��ł���.
\end{theorem}

�_������
�W�� $\Gamma$ ��{\bf �͌^}�Ƃ�, 
 ������\ $\Gamma \ra$ �̔����̂��Ƃł�.
 $\Gamma$ ���_�����̏W���̂Ƃ���, $\Gamma$�Ɋ܂܂��
�S�Ă̘_���� $\alpha$ �ɂ��� ${\cal A}(\alpha) = \top$ �ƂȂ��Ă���
�\�� $\cal A$ �� $\Gamma$ �̖͌^�ƂȂ�܂�.

\begin{theorem}[�R���p�N�g���藝]\label{the-compact}\em
�_�����̏W���̔C�ӂ̗L�������W�����͌^�����Ă�, ���Ƃ̏W�����͌^
������.
\end{theorem}
\newpage
\begin{itemize}
\item $\neg \alpha$ �� $\alpha \to \bot$ ��
\item $\alpha \wedge \beta$ �� $\neg(\alpha \to \neg \beta)$ ��
\item $\alpha \vee \beta$ �� $(\alpha \to \beta) \to \beta$ ��
\item $\alpha \leftrightarrow \beta$ �� $(\alpha \to \beta) \wedge
(\beta \to \alpha)$ ��
\item $\exists x\ \alpha$ �� $\neg \forall x \neg \alpha$ ��
\end{itemize}
���ꂼ�ꗪ���ď��������̂Ƃ��܂�. $\exists$ �́u���݂���v��\���_���L
���ł�.
\\[5mm]
{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B

{\bf �q��_�� NJ} �̐��_�K���͎��� 5 �ł��B
\[ \infer[\mbox{($\to$-E)}]{\beta}{\deduce{\alpha\to \beta}{\Pi_1}  & \deduce{\alpha}{\Pi_2}},
\hspace{7mm} \infer[k\mbox{($\to$-I)}]{\alpha \to \beta}{\deduce{\beta}{\deduce{\Pi}{\deduce{\alpha}{k}}}}
\]
\[
\infer[\mbox{($\bot$-E)}]{\alpha}{\deduce{\bot}{\Pi}}, \hspace{7mm}
\infer[\mbox{($\forall$-I)}]{\forall x \alpha}{\deduce{\alpha}{\Pi}}, \hspace{7mm}
\infer[\mbox{($\forall$-E)}]{[t/x]\alpha}{\deduce{\forall x \alpha}{\Pi}}
\]

\end{document}
