\documentstyle{jarticle}
\title{ ���������� \\ ���� }
\author{ G96P073-6 ����ʹ�� }
\date{
  ���� 1999/5/11 \\
  ��� 1999/5/25
}

\begin{document}
\maketitle


\section{ ���� }

���� $T = \{ \varphi \; | \; (Q, \leq) \models \varphi \} $
�βĻ���ǥ� $(R, \leq)$ �ϡ�
$(Q, \leq)$ ��Ʊ���Ǥ��뤳�Ȥ򼨤���
\\
�����ǡ�
$Q$ ��ͭ�������Τν���Ǥ��롣


\section{ ���� }

ɽ����ʷ�ˤ��뤿��ˡ�
����Ū�ǤϤʤ����������Υ�ǥ�ξ�ǽҸ��$<$�ˤ�������롣
$$ \forall x \forall y [x<y \Leftrightarrow (x \leq y) \wedge \neg (x=y)] $$

���ơ�����Ū�ˤϡ�\\
\begin{tabular}{lll}
$T = \{ $
&�����
  &$ \forall x \forall y \forall z [(x \leq y) \wedge (y \leq z) \Rightarrow (x \leq z)] $\\
& &$ \forall x \forall y [(x \leq y) \wedge (y \leq x) \Rightarrow (x=y)] $\\
& &$ \forall x \forall y [(x \leq y) \vee (y \leq x)] $\\
&����Ǿ��ʤ� &$ \forall x \exists y \exists z [(y<x) \wedge (x<z)] $\\
&��̩ &$ \forall x \forall y \exists z [(x<y) \Rightarrow (x<z) \wedge (z<y)] $\\
\}
\end{tabular}
\\�Ǥ��롣


\section{ ���� }

$(R, \leq)$ �� $(Q, \leq)$ ��Ʊ���Ǥ��뤳�Ȥ򼨤��ˤϡ�
$R$ �� $Q$ �δ֤ˡ�
����ط�����¸������ñ�ͤ�¸�ߤ��뤳�Ȥ򼨤����ɤ���

�ޤ������Τ褦�ʴؿ� $f: Q \rightarrow R$ ���������ʤ��뤤�ϡ�ȯ������סˡ�
\\
���ˡ��ؿ� $f$ �������Ǥ��뤳�Ȥ򸡾ڤ��롣
�ʼºݤˤϡ����� $2$ �ĤΥ��ƥåפ�ʿ�Ԥ��ƿʤ����������


\section{ ���� }

\begin{tabular}{l}
$Q = \{ q_0, q_1, q_2, \ldots \} $\\
$R = \{ r_0, r_1, r_2, \ldots \} $\\
\end{tabular}
\\�Ȥ��롣

�ޤ���
$f(q_0) = r_0$ �Ȥ��롣
��$Q, R$ �϶�����Ǥʤ��Τǡ�����������Ǥ��롣��


\subsection{ ��֤򹭤��� }

����ޤǤ����� $f$ ������ط�����¸���ʤ��顢
$Q, R$ �Τ����Ĥ��θ����б��Ť��Ƥ����ΤȤ��롣
\\
��$f': X \rightarrow Y$�ʤ����� $(X \subset Q) \wedge (Y \subset R)$��
  �ʤ���ñ�� $f'$ �����������б��Ť����Ǥ��Ƥ����ΤȤ��롣��

$Q$ ���б����ߤθ��Τ������Ǿ��Τ�Τ� $q_i$������Τ�Τ� $q_j$ �Ȥ���
$(f(q_i)=r_i) \wedge (f(q_j)=r_j)$ �Ȥ���ȡ�
$r_i, r_j$ �ϡ����줾�� $R$ ���б����ߤθ��Τ������Ǿ�������Τ�ΤǤ��롣
\\
�ʤ��Τ褦���б��Ť����Ƥ���Ȳ��ꤷ�Ƥ���Τǡ������Ǥ��롣��

���ΤȤ���
$(q_m<q_i) \wedge (q_j<q_n)$ �Ǥ���褦�� $q_m, q_n$ ��
$(r_m<r_i) \wedge (r_j<r_n)$ �Ǥ���褦�� $r_m, r_n$ ���б��Ť��롣
���ʤ����
$(f(q_m)=r_m) \wedge (f(q_n)=r_n)$ �Ȥ��롣
\\
�ʡֺ���Ǿ��ʤ��פ����������� $q_m, q_n$ �� $r_m, r_n$ ��¸�ߤ���
  �������������Ǥ��롣��

�������ˤ�ä� $f$ ������ط�������ʤ����Ȥ򼨤���
\\
�����ޤǤ��б����ߤ�
$Q$ ����ʬ����� $X'$��
$R$ ����ʬ����� $Y'$ �Ȥ���ȡ�
$\forall q_x \in X' \; [(q_m \leq q_x) \wedge (q_x \leq q_n)]$��
$\forall r_y \in Y' \; [(r_m \leq r_y) \wedge (r_y \leq r_n)]$ �Ǥ��롣
\\
���ʤ�����������б��Ť���줿 $q_m, q_n$ �� $r_m, r_n$ ��ޤ�ƽ���ط����ݤ���Ƥ��롣

$Q, R$ ���줾��Ρ�
���ܤ��� $2$ �ĤΡ��б����ߤΡ˸��ˤ�äƶ��ڤ�줿����֤ϡ�
��֤򹭤������ˤ�ä� $2$ �Ĥդ��롣
���ʤ����
�������ξ���֤θĿ��� $a$ �Ȥ���ȡ�
����ξ���֤θĿ��� $a+2$ �Ǥ��롣


\subsection{ ����֤� $2$ ʬ���� }

����ޤǤ����� $f$ ������ط�����¸���ʤ��顢
$Q, R$ �Τ����Ĥ��θ��� $1$ �� $1$������б��Ť��Ƥ����ΤȤ��롣

$Q, R$ ���б����ߤ���ʬ����򤽤줾�� $X, Y$ �Ȥ��롣
$X, Y$ ���줾��Ρ�
���ܤ��� $2$ �Ĥθ��ˤ�äƶ��ڤ�줿����֤θĿ��� $a$ �Ȥ���ȡ�
���줫��Ԥ����ϡ�����֤θĿ��� $2a$ �ˤ����ΤǤ��롣
��$x_i$ �� $x_j$�ʤ����� $x_i<x_j$�ˤ����ܤ���Ȥϡ�
  $\forall x [(x \leq x_i) \vee (x_j \leq x)]$
  ��ɽ���롣��

�������ϡ�
$a$ �Ĥξ���֤��줾��ˤĤ��ơ�
���ζ�����¸�ߤ��븵�� $1$ �������б��Ť��롣

����Ū�ˤϡ����ΤȤ���Ǥ��롣
\\
$Q$ �ξ���֤���ڤ� $2$ �ĤΡ����ܡ˸���
$q_i, q_j$�ʤ����� $q_i<q_j$�ˤȤ���
$(f(q_i)=r_i) \wedge (f(q_j)=r_j)$ �Ȥ���ȡ�
$(q_i<q_m) \wedge (q_m<q_j)$ �ʤ� $q_m$ ��
$(r_i<r_m) \wedge (r_m<r_j)$ �ʤ� $r_m$ ��¸�ߤ��롣
�ʡ���̩�פ��������������Ǥ��롣��
���ΤȤ���
$f(q_m) = r_m$ �Ȥ��롣
�ʤ������ˤ�ä� $f$ ������ط�������ʤ��Τ����餫�Ǥ��롣��


\section{ �ޤȤ� }

�ֶ�֤򹭤�������ȡ־���֤� $2$ ʬ��������򷫤��֤����Ȥˤ�äơ�
�ǽ�Ū�� $Q, R$ �Τ��٤Ƥθ��ϡ�
����ط�����¸������ñ�� $f$ �ˤ�ä��б��Ť����롣
�������äơ�
$(R, \leq)$ �ϡ�
$(Q, \leq)$ ��Ʊ���Ǥ��롣


\subsection{ ����֤ˤĤ��� }

����֤θĿ��ϡ�
�ֶ�֤򹭤�������ˤ�ä� $2$ �Ĥդ���
�־���֤� $2$ ʬ��������ˤ�ä� $2$ �ܤˤʤ롣

���� $2$ �Ĥ����򷫤��֤����Ȥˤ�äơ�
����֤θĿ��϶���ñĴ���ä��롣
����Ļ���������ʤ��ȡ�����֤θĿ��ϲĻ��Ĥˤʤꡢ
�������ä��б��Ť���줿���θĿ���Ļ��Ĥˤʤ롣

$Q$ �ʤ����� $R$�ˤ�ǻ�٤ϲĻ��Ǥ��ꡢ
�Ļ���������θ塢
$Q, R$ �Τ��٤Ƥθ��� $f$ �ˤ�ä��б��Ť�����ȸ����롣


\subsection{ $f$ �������� }

�����ǡ�
$f$ �������Ǥ��뤫���ڤ��롣


\subsubsection{ ����ط�����¸���뤫 }

$f$ ������ط�����¸���뤳�Ȥ�Τ���롣

�ǽ���б��Ť� $f(q_0)=r_0$ �ˤ�äƽ���ط�������뤳�ȤϤʤ���
���λ����� $Q, R$ ���б����ߤ���ʬ���� $X, Y$ �Ϥ��줾�� $1$ ������Ǥ��롣

���ˡֶ�֤򹭤���ס�
��$1$ ��������Ф��ƾ���֤� $0$ �ĤǤ��ꡢ
  �־���֤� $2$ ʬ����פ��ȤϤǤ��ʤ�����
�������ˤ�äƽ���ط�������ʤ����Ȥ����˽Ҥ٤���

�����ơ־���֤� $2$ ʬ����ס�
�������ˤ�äƽ���ط�������뤳�ȤϤʤ���
����� $[q_i, q_j], [r_i, r_j]$ ��
$2$ ʬ���� $q_m$ �� $r_m$ �ˤĤ��ơ�\\
\begin{tabular}{ll}
$\forall q_x \in X \subset Q \; [(f(q_x)=r_y) \wedge $
  & $((q_x=q_m) \Rightarrow (r_y=r_m)) \wedge $\\
  & $((q_x \leq q_i) \Rightarrow (q_x<q_m) \wedge (r_y<r_m)) \wedge $\\
  & $((q_j \leq q_x) \Rightarrow (q_m<q_x) \wedge (r_m<r_y)) ]$\\
\end{tabular}
\\�Ǥ��롣

�ֶ�֤򹭤�������ȡ־���֤� $2$ ʬ���������
�����֤��Ƥ����ط�������뤳�ȤϤʤ���


\subsubsection{ ��ñ�ͤ� }

$f$ ��ñ�ͤǤ��롣
����ޤǽҤ٤������ϡ�
�б����ߤθ����б��Ť���ľ�����ȤϤʤ���
�Ĥޤꡢ
$R$ �θ� $1$ �Ĥ� $2$ �İʾ� $Q$ �θ����б��Ť����뤳�ȤϤʤ���

$f$ �����ͤǤ��뤳�Ȥ�����ˡ��ȤäƼ�����
����� $[r_i, r_j]$ �δ֤ˡ��б��Ť����Ƥ��ʤ��� $r$ ������Ȥ��롣
��$[r_i, r_j]$ �� $r$ ��ޤ�Ǿ���֤Ȥ��롣���ʤ����
  $r_i, r_j$ �ϡ��б����ߤ� $R$ �θ��Τ��������ܤ��� $2$ �Ĥθ��Ǥ���Ȥ��롣��
���ΤȤ� $\exists q_i \exists q_j [(f(q_i)=r_i) \wedge (f(q_j)=r_j)]$ �Ǥ��롣
�ʺǽ���б��Ť��θ塢�ֶ�֤򹭤�������Ͼ�˲�ǽ�ʤΤǡ���

���ơ���̩�פ�������ꡢ
�б��Ť����Ƥ��ʤ� $Q$ �θ� $q$ ��¸�ߤ���
$(q_i<q) \wedge (q<q_j)$ �Ǥ��롣
$q$ ��¸�ߤ��뤳�Ȥϡ���̩�פ������������餫������
$q$ ���б��Ť����Ƥ��ʤ����Ȥϡ�
$f$ ������ط����ݤĤ��Ȥ�������롣
�⤷ $f(q)=r'$ �ʤ� $r'$ ��¸�ߤ���
$q$ ���б����ߤȤ���ȡ�
$[r_i, r_j]$ �� $r$ ��ޤ�Ǿ���֤Ǥ���Ȥ��������ȿ���뤫��Ǥ��롣

�������äơ�̤�б��� $r$ ���Ф��ƾ��̤�б��� $q$ ��¸�ߤ���
$f(q)=r$ ���б��Ť����롣
�ǽ�Ū�ˡ�
$R$ �θ��ϡ����٤��б��Ť����롣
�Ĥޤꡢ
$f$ �����ͤǤ��롣

\end{document}
