%\documentclass{jarticle}
\documentclass{jsarticle}
\usepackage{proof}

\pagestyle{plain}
\def\imp{\to}
\newtheorem{df}{��`}[section]
\newtheorem{thm}[df]{�藝}
\newtheorem{cor}[df]{�n}

\begin{document}

%%�@�\��
\thispagestyle{empty}
\vspace*{1cm}
\begin{center}
{\Large\gt ��t��w��w�@�@���R�Ȋw�����ȁ@\\[3mm]
�C�m�_��}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf �������l�_����̏W���_�̖�������}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����15�N3��24��}
\end{center}

\vspace*{5.7cm}
\begin{center}
{\Large\gt ���w�E��񐔗��w ��U \\[2mm]
        ��񐔗��w �u��}
\end{center}

\vspace*{5mm}
\begin{center}
{\Large\gt �Γc�@�^�V}
\end{center}

\setcounter{page}{0}

\newpage

%% �T�v
\thispagestyle{empty}
\section*{�T�v}

1979�N�AWhite��\L ukasiewicz�̖������l�_���ɂ�����comprehension axiom
�̖����������������B���̎菇�͈ȉ��̒ʂ�ł���B�܂��ALouise Hay�̗p�ӂ���
�������l�_���̑̌n��comprehension axiom���������̌nH�����AH��$\tau$-term��
�������̌nH$_1$���l����B������H$_1$�ɑΉ����鎩�R���_�̑̌nG�iG��H$_1$���
�ア�̌n�j��p�ӂ��AG�̖����������������B������G�̖������������ƂɁA
H�̖����������������B

���̘_���ł́AWhite�̑̌nG�̑���ɁAG����$\tau$-term�������AG�̐��_�K����
���R�Ȃ��̂ɂ����̌nG*���l���A���̖��������ɂ��Ē��ׂ��B�܂��A
�̌nG*��$\lambda$-term�𓱓������̌n�ɂ��Ă��c�_����B

\setcounter{page}{0}

\newpage

%% �ڎ�
\tableofcontents

\newpage

%% ��P��
\section{�͂��߂�}

$R$���A�������g�����Ƃ��Ċ܂܂Ȃ��W���S�́A���Ȃ킿
$R \equiv \{x:x \notin x\}$�ƒ�`����ƁA$R \in R$�Ȃ��$R \notin R$�A
�܂�$R \notin R$�Ȃ��$R \in R$�ƂȂ�B�����Russell�̃p���h�b�N�X�Ƃ����B

1920�N�A\L ukasiewicz��3�l�_�����l�����B���̓��@��1��Russell��
�p���h�b�N�X�̉����ł������B���̌�A\L ukasiewicz��Tarski�͂����
��ʉ�����n�l�_��($2 \le n \le \omega$)���l�����B

\L ukasiewicz��n�l�_���̐^���l�̏W����$S_n$�Ƃ���ƁA
$$S_n = \Big{\{}0,\frac{1}{n-1} ,\frac{2}{n-1} ,\ldots ,\frac{n-2}{n-1} 
  ,1\Big{\}} (n \neq \omega)$$
$$S_\omega = [0,1] $$
�ł���BRussell�̃p���h�b�N�X�́A�_����P�Ƃ��̔ے肪���l�ɂȂ�Ƃ���
�����ł��邪�A\L ukasiewicz��3�l�_���ł́A����͖����Ƃ͂Ȃ�Ȃ��B

������1954�N�AM.Shaw-Kwei�́A���R��n�ɑ΂���\L ukasiewicz��n�l�_����
��������comprehension axiom(comprehension axiom 
$\exists x \forall y (y \in x \leftrightarrow A)$�ɂ����āA
$A$�͂ǂ̂悤�Ș_�����ł��悢)��������Ɩ������o�邱�Ƃ�������(\cite{sh})�B
���̂Ƃ��AM.Shaw-Kwei�́u\L ukasiewicz�̖������l�q��_���ɖ�������
comprehension axiom��������Ɩ������o�邩�H�v�Ƃ��������c�����B
������1979�N�ɁAR.B.White��\L ukasiewicz�̖������l�q��_���ɖ�������
comprehension axiom�������Ă��������ł��邱�Ƃ��ؖ�����(\cite{wh})�B

\L ukasiewicz�̖������l�q��_���ɂ����čP�^�Ș_�����͋A�[�I�Z�łȂ����߁A
�L���I�Ȑ��_�K���ƗL���̌����^��\L ukasiewicz�̖������l�q��_����
�̌n����邱�Ƃ��ł��Ȃ��B������Louise Hay�͖����I�Ȑ��_�K����p����
\L ukasiewicz�̖������l�q��_���̑̌n�������(\cite{ha})�BWhite��Louise Hay��
������̌n�ɖ�������comprehension axiom���������̌n��H�Ƃ��A
���̖����������ؖ����Ă���B

White�́A�̌nH�̖����������ؖ����邽�߂Ɏ��R���_�̑̌nG���g�������A
�ȉ��ł�H�̖����������ؖ�����ƂƂ��ɁAG�̐��_�K�������R�Ȃ��̂ɂ���
�̌nG*���l���A���̖��������������B

%% ��Q��
\section{�̌nH}

�̌nH��Louise Hay���p�ӂ���\L ukasiewicz�̖������l�q��_���̑̌n�ɖ�������
comprehension axiom���������̌n�ł���B
H��term��formula�͎��̂悤�ɋA�[�I�ɒ�`�����B

\begin{df}(term and formula)

(1) ���ׂĂ̕ϐ���term�ł���B

(2) �萔$\bot$��formula�ł���B

(3) $A$,$B$��formula�Ȃ�΁A$(A \to B)$��formula�ł���B

(4) $s$,$t$��term�Ȃ�΁A$s \in t$��formula�ł���B

(5) $x$���ϐ��A$A$��formula�Ȃ�΁A
    $\{x:A\}$��term�A$\forall x A$��formula�ł���B
\end{df}

\begin{df}
term�܂���formula s�ɑ΂��A$[t/a]s$�����̂悤�ɒ�`����B

$\cdot [t/a]a \equiv t$

$\cdot [t/a]b \equiv b$ if $b \not\equiv a$

$\cdot [t/a]\bot \equiv \bot$

$\cdot [t/a](A \to B) \equiv [t/a]A \to [t/a]B$

$\cdot [t/a](s_1 \in s_2) \equiv [t/a]s_1 \in [t/a]s_2$

$\cdot [t/a]\{x:A(x)\} \equiv \{x:[t/a]A(x)\}$

$\cdot [t/a]\forall x A(x) \equiv \forall x [t/a]A(x)$
\end{df}

�ȉ��A����Ȃ����ʂ͉E����₤���̂Ƃ���B

\begin{df}

$\neg A \equiv A \to \bot$,

$A \vee B \equiv (A \to B) \to B$,

$A \& B \equiv \neg (\neg A \vee \neg B)$,

$A \leftrightarrow B \equiv (A \to B) \& (B \to A)$,

$A \cdot B \equiv \neg (A \to \neg B)$,

$A^1 \to B \equiv A \to B$, $A^{n+1} \to B \equiv A \to A^n \to B$
(for $n \ge 1$),

$s \notin t \equiv \neg s \in t$,

$\exists xA \equiv \neg \forall x \neg A$.
\end{df}

�̌nH�͎��̂悤�Ȍ����Ɛ��_�K�������B

{\large\gt Axiom schemes}


H1.  $A \to B \to A$.

H2.  $(A \to B) \to (B \to C) \to A \to C$.     

H3.  $A \vee B \to B \vee A$.

H4.  $(\neg A \to \neg B) \to B \to A$.

H5.  $\exists x A \cdot \exists x A \to \exists x (A \cdot A)$.
 
H6.  $[t/x]A \to \exists x A$.

H7.  $\exists x A \to \exists y [y/x]A$.

H8.  $\forall x (A \to B) \to \exists x A \to B$, $B$��$x$��
���R�Ɍ���Ȃ�.

H9.  $(A \to \exists x B) \to \exists x (A \to B)$, $A$��$x$��
���R�Ɍ���Ȃ�.

H10. $[t/x]A \to t \in \{x:A\}$.

H11. $t \in \{x:A\} \to [t/x]A$.

\vspace*{5mm}

{\large\gt Inference rules}
$$ 
$$ 
\infer[\mbox{(modus ponens)}]{B}{A \to B & A}
$$
$$
\infer[\mbox{(generalization)}]{\forall x A}{A}
$$
$$
\infer[\mbox{(inf)}]{A}{\{(A^n \to \bot) \to A\}_{1 < n < \omega}}.
$$
$$

comprehension axiom $\exists x \forall y(y \in x \leftrightarrow
A)$�͈ȉ��̂悤�Ɏ������B�܂��A����H10,H11����A
$$a \in \{x:[x/y]A\} \to [a/y]A , \qquad [a/y]A \to a \in \{x:[x/y]A\}$$
�𓾁A������H1-H4, modus ponens����
$$a \in \{x:A\} \leftrightarrow [a/y]A$$
�𓾂�B�����generalization��K�p����
$$\forall y(y \in \{x:A(x)\} \leftrightarrow A)$$
�����H6, modus ponens����
$$\exists x \forall y(y \in x \leftrightarrow A)$$
�𓾂�B

%% ��R��
\section{�̌nG*}

G*��White��G�����ƂɁAG�̐��_�K�������R�Ȃ��̂ɂ������R���_�̑̌n�ł���B

G*�̏ؖ��}(proof)�͏���ɕ��򂷂�L���̖؂ł���B
���ꂼ��̐�(node)��formula�ł���A��[�͉����formula�ł���B
���ꂼ��̉����formula�ɂ͐��̐��������蓖�Ă��A���̏��
���ڏ������B�����G*�̐��_�K���ɂ���ė��Ƃ���邱�Ƃ�����B

�啶����$\Sigma,\Pi$�́A���X�Y�������āAG*�̏ؖ��}��\���̂Ɏg����B
$\vcenter{\deduce{A}{\Sigma}}$�͌��_��A�ł���ؖ��}��\���B

\begin{df}(disjoint)

2�̏ؖ��}$\Sigma,\Pi$��disjoint�ł���Ƃ́A�C�ӂ�formula A��
�C�ӂ̐��̐���k�ɑ΂��āA����$\vcenter{\deduce{A}{k}}$��$\Sigma,\Pi$��
�����ɂ͌���Ȃ����Ƃł���B
\end{df}

G*�̐��_�K���͎��̂W�ł���B

\vspace*{5mm}

{\large\gt Inference rules}
$$
$$
Implication Introduction
$$
\vcenter{\infer[(\to i),k]{A \to B}{\deduce{B}{\deduce{\displaystyle \Sigma}
    {\deduce{A}{k}}}}}
$$
Implication Elimination
$$
\vcenter{\infer[(\to e)]{B}{\deduce{A \to B}{\displaystyle \Sigma} 
    & \deduce{A}{\displaystyle \Pi}}}
\qquad
\vcenter{\deduce{A \to B}{\displaystyle \Sigma}}��
\vcenter{\deduce{A}{\displaystyle \Pi}}��disjoint
$$
Disjunction
$$
\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\displaystyle \Sigma}}
$$
Ex falso quodlibet
$$
\infer[(q)]{A}{\deduce{\bot}{\displaystyle \Sigma}}
$$
Universal Quantifier Introduction
$$
\vcenter{\infer[(ui)]{\forall x A}{\deduce{A}{\displaystyle \Sigma}}}
\qquad
x�͗����Ă��Ȃ�����Ɍ���Ȃ�
$$
Universal Quantifier Elimination
$$
\vcenter{\infer[(ue)]{[t/x]A}{\deduce{\forall x A}{\displaystyle \Sigma}}}
$$
Class Introduction
$$
\infer[(ci)]{t \in \{x:[x/t]A\}}{\deduce{A}{\displaystyle \Sigma}}
$$
Class Elimination
$$
\infer[(ce)]{[t/x]A}{\deduce{t \in \{x:A\}}{\displaystyle \Sigma}}
$$

\begin{df}
G*�̏ؖ��}$\Sigma$�ɑ΂��A$[t/a]\Sigma $�����̂悤�ɒ�`����B

$$
\Sigma \equiv \vcenter{\infer[(\to i),k]{A \to B}{\deduce{B}{\deduce{\Pi}
                 {\deduce{A}{k}}}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(\to i),k]{[t/a](A \to B)}{\deduce{[t/a]B}
                      {\deduce{[t/a]\Pi}{\deduce{[t/a]A}{k}}}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(\to e)]{B}{\deduce{A \to B}{\Pi_1} 
                  & \deduce{A}{\Pi_2}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(\to e)]{[t/a]B}{\deduce{[t/a](A \to B)}
                      {[t/a]\Pi_1} & \deduce{[t/a]A}{[t/a]\Pi_2}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(\vee)]{[t/a](B \vee A)}
%                      {\deduce{t/a}(A \vee B)}{[t/a]\Pi}}]
                      {\deduce{[t/a](A \vee B)}{[t/a]\Pi}}]
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(q)]{A}{\deduce{\bot}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(q)]{[t/a]A}{\deduce{\bot}{[t/a]\Pi}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(ui)]{\forall x A(x)}{\deduce{A(a)}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(ui)]{[t/a]\forall x A}
                      {\deduce{[t/a]A}{[t/a]\Pi}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(ue)]{[t_1/x]A}{\deduce{\forall x A}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(ue)]{[t/a][t_1/x]A}
                      {\deduce{[t/a]\forall x A}{[t/a]\Pi}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(ci)]{t_1 \in \{x:A\}}{\deduce{[t_1/x]A}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(ci)]{[t/a](t_1 \in \{x:A\})}
                      {\deduce{[t/a] [t_1/x]A}{[t/a]\Pi}}}
$$
\vspace*{2mm}
$$
\Sigma \equiv \vcenter{\infer[(ce)]{A}{\deduce{t_1 \in \{x:[x/t_1]A\}}{\Pi}}}
�Ȃ�΁A
[t/a]\Sigma \equiv \vcenter{\infer[(ce)]{[t/a]A}
                      {\deduce{[t/a](t_1 \in \{x:[x/t_1]A\})}{[t/a]\Pi}}}
$$
\end{df}

\begin{thm}
�C�ӂ�G*�̏ؖ��}$\Sigma$��term t�ɑ΂��āA
$[t/a]\Sigma $��G*�̏ؖ��}�ł���B
\end{thm}

%% ��S��
\section{�̌nG*�̖�������}

\begin{df}(categorical proof)
�����Ă��Ȃ����肪���݂��Ȃ��ؖ��}�̂��Ƃ�categorical proof�Ƃ����B
\end{df}

\begin{df}(contradictive proof)

���_��$\bot$�ł���categorical proof��contradictive proof�Ƃ����B
\end{df}

G*�̖��������͈ȉ��̂悤�Ɏ����B

�܂��Anormal�Ƃ����T�O���`���A���ׂĂ�contradictive proof��normal��
reduce�ł��邱�Ƃ������B������normal��contradictive proof��
���݂��Ȃ����Ƃ������B���̂��߂ɂ܂��A���̂悤��reduction���`����B

\begin{df}(reduction)

$\Sigma$��G*�̏ؖ��}�Ƃ���B
\vspace*{5mm}

{\large\gt $\bot$-reduction}

\vspace*{5mm}
$\Sigma$��contradictive proof�ŁAsubproof 
$\vcenter{\deduce{\bot}{\displaystyle \Pi}}$�������A
���ꂪcategorical�Ȃ�΁A����Œu��������B
\vspace*{5mm}

{\large\gt $\to$-reduction}

\vspace*{5mm}
$\Sigma$��
$$
\infer[(\to e)]{B}{\infer[(\to i),k]{A \to B}{\deduce{B}
   {\deduce{\displaystyle \Sigma_2}{\deduce{A}{k}}}} & 
   \deduce{A}{\displaystyle \Sigma_1}}
$$
�Ƃ������������Ă΁A���̕�����
$$
\deduce{B}{\deduce{\displaystyle \Sigma_2}{\deduce{A}{\displaystyle \Sigma_1}}}
$$
�Œu��������B�܂��A$\Sigma$��
$$
\infer[(\to e)]{B}{\infer[(\to i),k]{A \to B}{\deduce{B}
   {\displaystyle \Sigma_2}} & \deduce{A}{\displaystyle \Sigma_1}}
$$
�Ƃ������������Ă΁A���̕�����
$$
\deduce{B}{\displaystyle \Sigma_2}
$$
�Œu��������B
\vspace*{5mm}

{\large\gt $u$-reduction}

\vspace*{5mm}
$\Sigma$��
$$
\infer[(ue)]{A}{\infer[(ui)]{\forall x A}{\deduce{[t/x]A}
   {\displaystyle \Pi}}}
$$
�Ƃ������������Ă΁A���̕�����
$$
\deduce{[t/x]A}{\displaystyle [t/x]\Pi}
$$
�Œu��������B
\vspace*{5mm}

{\large\gt $c$-reduction}

\vspace*{5mm}
$\Sigma$��
$$
\infer[(ce)]{A}{\infer[(ci)]{t \in \{x:[x/t]A\}}{\deduce{A}
   {\displaystyle \Pi}}}
$$
�Ƃ������������Ă΁A���̕�����
$$
\deduce{A}{\displaystyle \Pi}
$$
�Œu��������B
\end{df}
\vspace*{5mm}

\begin{df}(weakly normal)

reduction������ȏ�ł��Ȃ�proof��
weakly normal proof�Ƃ����B
\end{df}

\begin{thm}

���ׂĂ�proof�͗L�����reduction���{����
weakly normal proof�ɂ��邱�Ƃ��ł���B
\end{thm}

\begin{df}(categorical $\vee$)

$\vcenter{\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Sigma}}}$
��$\vee$��categorical�ł���Ƃ́A$\vcenter{\deduce{A \vee B}{\Sigma}}$
��categorical�ł��邱�Ƃł���B
\end{df}

\begin{df}(normal)

weakly normal���Acategorical��$\vee$�������Ȃ�contradictive proof��
normal contradictive proof�Ƃ����B
\end{df}

\begin{thm}\label{no}
����contradictive proof�����݂���΁Anormal contradictive proof�����݂���B
\end{thm}

proof.

categorical��$\vee$�͎�菜�����Ƃ��ł��邱�Ƃ������B

���̗�ɂ��Ď����Ώ\���ł���B

$$
\infer*{\bot}{\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Sigma_1}}
    & \infer[(\vee)]{C \vee D}{\deduce{D \vee C}{\deduce{\Sigma_3}
    {\infer[(\vee)]{(E \vee F)}{\deduce{F \vee E}{\Sigma_2}}}}}}
$$

��weakly normal contradictive proof�Ƃ���B
�����A�ǂ�$\vee$��categorical�łȂ���΁A���̏ؖ��}�͂��ł�normal�ł���B

$\vcenter{\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Sigma_1}}}$
��categorical�ł���Ƃ���B���̂悤��categorical proof���`������B

$$
\infer[(\to e)]{B}{\deduce{A \vee B}{\Sigma_1} & \infer[(\to i),m]
    {A \to B}{\infer[(q)]{B}{\infer*{\bot}{\infer[(\to i)]{B \vee A}
    {\deduce{A}{m}} & \infer[(\vee)]{C \vee D}{\deduce{D \vee C}
    {\deduce{\Sigma_3}{\infer[(\vee)]{(E \vee F)}{\deduce{F \vee E}
    {\Sigma_2}}}}}}}}}
$$

($\vcenter{\deduce{A \vee B}{\Sigma_1}}$��categorical������A
$\to e$�̐����͖�������Ă���B)

���̏ؖ��}��$\vcenter{\deduce{B}{\Pi}}$�Ƃ���B
���̂悤��contradictive proof���`������B

$$
\infer*{\bot}{\infer={B \vee A}{\deduce{B}{\Pi}} & \infer[(\vee)]{C \vee D}
    {\deduce{D \vee C}{\deduce{\Sigma_3}{\infer[(\vee)]{(E \vee F)}
    {\deduce{F \vee E}{\Sigma_2}}}}}}
$$

�����ŁA

$$
\vcenter{\infer={B \vee A}{\deduce{B}{\Pi}}}
\qquad
\equiv 
\qquad
\vcenter{\infer[(\to i),j]{B \vee A}
    {\infer[(\to e)]{A}{\deduce{B \to A}{j} & \deduce{B}{\Pi}}}}
$$

�Ƃ���($j$�͓K���Ȑ�����)�B

���contradictive proof��weakly normal contradictive proof��
reduce���āA���̂悤��contradictive proof�𓾂�B

$$
\infer*{\bot}{\infer[(\vee)]{C \vee D}{\infer*{D \vee C}
    {\infer[(\vee)]{E \vee F}{\deduce{F \vee E}{\Sigma_4}}}} &
    \infer[(\vee)]{C \vee D}{\infer*{D \vee C}{\infer[(\vee)]
    {E \vee F}{\deduce{F \vee E}{\Sigma_5}}}}}
$$

�����A�ǂ�$\vee$��categorical�łȂ���΁A���̏ؖ��}�͂��ł�
normal�ł���B 

$\vcenter{\deduce{F \vee E}{\Sigma_5}}$��categorical�ł���Ƃ���B
���̂悤��categorical proof���`������B

$$
\infer[(\to e)]{E}{\deduce{F \vee E}{\Sigma_5} & \infer[(\to i),j_2]
    {F \to E}{\infer[(\to e)]{E}{\deduce{F \vee E}{\Sigma_5} &
    \infer[(\to i),j_1]{F \to E}{\infer[(q)]{E}{\infer*{\bot}
    {\infer[(\vee)]{C \vee D}{\infer*{D \vee C}{\infer[(\to i)]
    {E \vee F}{\deduce{F}{j_1}}}} & \infer[(\vee)]{C \vee D}
    {\infer*{D \vee C}{\infer[(\to i)]{E \vee F}{\deduce{F}{j_2}}}}}}}}}}
$$

���̏ؖ��}��$\vcenter{\deduce{E}{\Pi_1}}$�Ƃ���B
���̂悤��contradictive proof���`������B

$$
\infer*{\bot}{\infer={E \vee F}{\deduce{E}{\Pi_1}} & \infer={E \vee F}
    {\deduce{E}{\Pi_1}}}
$$

���contradictive proof��weakly normal contradictive proof��
reduce���āA���̂悤��contradictive proof�𓾂�B

$$
\infer*{\bot}{\infer[(\vee)]{C \vee D}{\deduce{D \vee C}{\Sigma_6}} &
    \infer[(\vee)]{C \vee D}{\deduce{D \vee C}{\Sigma_7}} &
    \infer[(\vee)]{C \vee D}{\deduce{D \vee C}{\Sigma_8}} &
    \infer[(\vee)]{C \vee D}{\deduce{D \vee C}{\Sigma_9}}}
$$

�����A�ǂ�$\vee$��categorical�łȂ���΁A���̏ؖ��}�͂��ł�
normal�ł���B 

$\vcenter{\deduce{D \vee C}{\Sigma_6}}$��categorical�ł���Ƃ���B
���̂悤��categorical proof���`������B

$$
\infer[(\to e)]{C}{\deduce{D \vee C}{\Sigma_6} & \infer[(\to i),k_4]
    {D \to C}{\infer[(\to e)]{C}{\deduce{D \vee C}{\Sigma_6} &
    \infer[(\to i),k_3]{D \to C}{\infer[(\to e)]{C}{\deduce{D \vee C}
    {\Sigma_6} & \infer[(\to i),k_2]{D \to C}{\infer[(\to e)]{C}
    {\deduce{D \vee C}{\Sigma_6} & \infer[(\to i),k_1]{D \to C}
    {\infer[(q)]{C}{\infer*{\bot}{\infer[(\to i)]{C \vee D}
    {\deduce{D}{k_1}} & \infer[(\to i)]{C \vee D}{\deduce{D}{k_2}} &
    \infer[(\to i)]{C \vee D}{\deduce{D}{k_3}} & \infer[(\to i)]
    {C \vee D}{\deduce{D}{k_4}}}}}}}}}}}}
$$

���̏ؖ��}��$\vcenter{\deduce{C}{\Pi_2}}$�Ƃ���B
���̂悤��contradictive proof���`������B

$$
\infer*{\bot}{\infer={C \vee D}{\deduce{C}{\Pi_2}} & \infer={C \vee D}
    {\deduce{C}{\Pi_2}} & \infer={C \vee D}{\deduce{C}{\Pi_2}} & 
    \infer={C \vee D}{\deduce{C}{\Pi_2}}}
$$

���̏ؖ��}�ɂ͂��͂␄�_�K��$\vee$�͊܂܂�Ă��Ȃ��B���Ȃ킿�A���̕ό`��
�s���΁Anormal contradictive proof��������B

\vspace*{2mm}
G*�̖��������͎��̒藝�ɂ���Ď������B

\begin{thm}
G*��normal contradictive proof�͑��݂��Ȃ��B
\end{thm}

proof.

normal contradictive proof�͗L���̖؂łȂ��Ă͂Ȃ�Ȃ����A
���ꂪ�s�\�ł��邱�Ƃ���A���̒藝�������B

$\vcenter{\deduce{\bot}{\Sigma}}$��normal contradictive proof�Ƃ���B
$\vcenter{\deduce{\bot}{\Sigma}}$��$\to e$����̂ݓ������̂ŁA
$\vcenter{\deduce{\bot}{\Sigma}}$��$\vcenter{\infer[(\to e)]{\bot}
{\deduce{\neg A}{\Sigma_1} & \deduce{A}{\Sigma_2}}}$�łȂ���΂Ȃ�Ȃ��B

$\vcenter{\deduce{\bot}{\Sigma}}$��normal�ł��邩��A$\vcenter{\deduce
{\neg A}{\Sigma_1}}$�̍Ō�̐��_�K����$\to i, q, \vee$�ł͂Ȃ��B
�܂��Aformula�̌`����$ui, ci$�ł͂Ȃ��B���Ȃ킿$\to e, ue, ce$��
�����ꂩ�ł���B

$\vcenter{\deduce{\neg A}{\Sigma_1}}$�̍Ō�̐��_�K����$ue$�ł�����
�Ƃ���ƁA$\vcenter{\deduce{\neg A}{\Sigma_1}}$�́A

$$
\infer[(ue)]{[t/x]\neg B}{\deduce{\forall x (\neg B)}{\Sigma_3}}
$$

�Ƃ����`�����Ă���B$\vcenter{\deduce{\bot}{\Sigma}}$��normal�ł��邩��A
$\vcenter{\deduce{\forall x (\neg B)}{\Sigma_3}}$�̍Ō�̐��_�K����
$q, \vee , ui$�ł͂Ȃ��B�܂��Aformula�̌`����$\to i, ci$�ł͂Ȃ��B
���Ȃ킿$\to e, ue, ce$�̂����ꂩ�ł���B

$\vcenter{\deduce{\neg A}{\Sigma_1}}$�̍Ō�̐��_�K����$ce$�ł�����
�Ƃ���ƁA$\vcenter{\deduce{\neg A}{\Sigma_1}}$�́A

$$
\infer[(ce)]{[t/x]\neg B}{\deduce{t \in \{x:\neg B\}}{\Sigma_4}}
$$

�Ƃ����`�����Ă���B$\vcenter{\deduce{\bot}{\Sigma}}$��normal�ł��邩��A
$\vcenter{\deduce{t \in \{x:\neg B\}}{\Sigma_4}}$�̍Ō�̐��_�K����
$q, \vee , ci$�ł͂Ȃ��B�܂��Aformula�̌`����$\to i, ui$�ł͂Ȃ��B
���Ȃ킿$\to e, ue, ce$�̂����ꂩ�ł���B

$\vcenter{\deduce{\neg A}{\Sigma_1}}$�̍Ō�̐��_�K����$\to e$�ł����� 
�Ƃ���ƁA$\vcenter{\deduce{\neg A}{\Sigma_1}}$�́A

$$
\infer[(\to e)]{\neg A}{\deduce{C \to \neg A}{\Sigma_5} & \deduce{C}{\Sigma_6}}
$$

�Ƃ����`�����Ă���B$\vcenter{\deduce{\bot}{\Sigma}}$��normal�ł��邩��A
$\vcenter{\deduce{C \to \neg A}{\Sigma_5}}$�̍Ō�̐��_�K����
$\to i, q, \vee$�ł͂Ȃ��B�܂��Aformula�̌`����$ui, ci$�ł͂Ȃ��B
���Ȃ킿$\to e, ue, ce$�̂����ꂩ�ł���B

������ɂ��Ă��A$\vcenter{\deduce{\neg A}{\Sigma_1}}$�ɁA����鐄�_�K����
$\to e, ue, ce$�݂̂ł���悤�ȓ������邩��A$\vcenter{\deduce{\bot}{\Sigma}}$
��contradictive proof�ɂȂ蓾�Ȃ��B

%% ��T��
\section{�̌nG�Ƃ��̖�������}

\begin{df}(closed)

term�܂���formula�����R�Ɍ����ϐ����܂܂Ȃ��Ƃ��A����term�܂���formula��
closed�ł���Ƃ����B
\end{df}

White�́AH��term�̒�`�Ɏ��̒�`�����������̌n��H$_1$�Ƃ����B

\begin{df}($\tau$-term)

�C�ӂ̕ϐ�x�ƁA���R�Ɍ����ϐ����P��������formula A�ɑ΂��āA
$\tau^n_xA$ ��term�ł���(n�͐��̐���)�B
\end{df}

����H$_1$�����Ƃ�White�͎��R���_�̑̌nG��p�ӂ����B���̐��_�K����
$\to i$, $\to e$, $\vee$, $q$, $ci$(�ȏ�G*�Ɠ���)�ƁA
$$
$$
Universal Quantifier Introduction
$$
\vcenter{\infer[(ui)]{\forall x A}{\deduce{A(\tau^n_xA)}
   {\displaystyle \Sigma}}}
\qquad
A�ɂ͎��R�Ɍ����ϐ����P��
$$
Negative Universal Quantifier Introduction
$$
\vcenter{\infer[(\neg ui)]{\neg \forall x [x/t]A}{\deduce{\neg A}{\Sigma}}}
\qquad
t��closed
$$
Negative Class Introduction
$$
\infer[(\neg ci)]{t \notin \{x:[x/t]A\}}{\deduce{\neg A}{\Sigma}}
$$
�ł���B

\begin{thm}(derived rules)

��̐��_�K������A����derived rules��������B
\end{thm}
$$
$$
Double Nagation
$$
\infer[(dn),k]{A}{\deduce{\bot}{\deduce{\displaystyle \Sigma}
    {\deduce{\neg A}{k}}}}
$$
Universal Quantifier Elimination
$$
\infer[(ue)]{[t/x]A}{\deduce{\forall x A}{\Sigma}}
\qquad
t��closed
$$
Existential Quantifier Introduction
$$
\vcenter{\infer[(ei)]{\exists x [x/t]A}{\deduce{A}{\displaystyle \Sigma}}}
\qquad
t��closed
$$
Existential Quantifier Elimination
$$
\vcenter{\infer[(ee)]{A(\in^n_xA)}{\deduce{\exists x A}{\Sigma}}}
\qquad
\exists x A ��closed
\qquad
\in^n_xA \equiv \tau^n_x\neg A
$$
Class Elimination
$$
\infer[(ce)]{[t/x]A}{\deduce{t \in \{x:A(x)\}}{\Sigma}}
$$

proof.

$$
\infer[(\to e)]{A}{\infer[(\vee)]{\bot \vee A}{\infer[(\to i),k]{A \vee \bot}
    {\deduce{\bot}{\deduce{\displaystyle \Sigma}{\deduce{\neg A}{k}}}}}
    & \infer[(\to i),m]{\bot \to A}{\infer[(q)]{A}{\deduce{\bot}{m}}}}
\qquad
\infer[(dn),k]{[t/x]A}{\infer[(\to e)]{\bot}{\infer[(\neg ui)]
   {\neg \forall x A}{\deduce{\neg [t/x]A}{k}} & \deduce{\forall x A}
   {\Sigma}}}
$$
$$
\infer[(\to i),k]{\exists x [x/t]A}{\infer[(\to e)]{\bot}{\infer[(ue)]{\neg A}
    {\deduce{\forall x \neg [x/t]A}{k}} & \deduce{A}{\displaystyle \Sigma}}}
\qquad
\infer[(dn),k]{A(\in^n_xA)}{\infer[(\to e)]{\bot}{\deduce{\exists x A}
    {\displaystyle \Sigma} & \infer[(ui)]{\forall x \neg A}
    {\deduce{\neg A(\in^n_xA)}{k}}}}
$$
$$
\infer[(dn),k]{[t/x]A}{\infer[(\to e)]{\bot}{\infer[(\neg ci)]
   {t \notin \{x:A\}}{\deduce{\neg [t/x]A}{k}} & \deduce{t \in \{x:A\}}
   {\Sigma}}}
$$

H�̂��ׂĂ̌�����G�ŏؖ��ł���킯�ł͂Ȃ����A
H�̂��ׂĂ�closed axiom��G�ŏؖ��ł���B

\begin{df}\label{theo}(theorem)

����formula��theorem�ł���Ƃ́A����formula�����_�Ƃ��Ă���
categorical proof�����݂��邱�ƂƂ���B
\end{df}

\begin{thm}

H�̂��ׂĂ�closed axiom��G��theorem�ł���B
\end{thm}

proof.

H1-H4�͎��̂悤�ɊȒP�ɏؖ��ł���B

$$
\infer[(\to i),1]{A \to B \to A}{\infer[(\to i)]{B \to A}
    {\deduce{A}{1}}}
\qquad
\infer[(\to i),1]{A \vee B \to B \vee A}{\infer[(\vee)]{B \vee A}
    {\deduce{A \vee B}{1}}}
$$
\vspace*{2mm}
$$
\infer[(\to i),1]{(A \to B) \to (B \to C) \to A \to C}{\infer[(\to i),3]
    {(B \to C) \to A \to C}{\infer[(\to i),2]{A \to C}{\infer[(\to e)]
    {C}{\deduce{B \to C}{3} & \infer[(\to e)]{B}{\deduce{A \to B}{1}
    & \deduce{A}{2}}}}}}
\qquad
\infer[(\to i),1]{(\neg A \to \neg B) \to B \to A}{\infer[(\to i),3]{B \to A}
    {\infer[(dn),2]{A}{\infer[(\to e)]{\bot}{\infer[(\to e)]{\neg B}{\deduce
    {\neg A \to \neg B}{1} & \deduce{\neg A}{2}} & \deduce{B}{3}}}}}
$$
\vspace*{2mm}
H5-H9��closed instance�͈ȉ��̒ʂ�B

$$
\infer[(\to i),4]{\exists x A \cdot \exists x A \to 
    \exists x (A \cdot A)}{\infer[(ei)]{\exists x (A \cdot A)}
    {\infer[(\to i),2]{A(\in^1_xA) \cdot A(\in^1_xA)}{\infer[(\to e)]
    {\bot}{\deduce{\exists x A \cdot \exists x A}{4} & \infer[(\to i),3]
    {\exists x A \to \neg \exists x A}{\infer[(\to i),1]
    {\neg \exists x A}{\infer[(\to e)]{\bot}{\infer[(\to e)]
    {\neg A(\in^1_xA)}{\deduce{A(\in^1_xA) \to \neg A(\in^1_xA)}{2} 
    & \infer[(ee)]{A(\in^1_xA)}{\deduce{\exists x A}
    {1}}} & \infer[(ee)]{A(\in^1_xA)}{\deduce{\exists x A}{3}}}}}}}}}
$$
\vspace*{2mm}
$$
\infer[(\to i),1]{[t/x]A \to \exists x A}{\infer[(ei)]{\exists x A}
    {\deduce{[t/x]A}{1}}}
\qquad
\infer[(\to i),1]{\exists x A \to \exists y [y/x]A}{\infer[(ei)]
    {\exists y [y/x]A}{\infer[(ee)]{A(\in^1_xA)}{\deduce{\exists x A}{1}}}}
$$
\vspace*{2mm}
$$
\infer[(\to i),1]{\forall x (A \to B) \to \exists x A \to B}
    {\infer[(\to i),2]{\exists x A \to B}{\infer[(\to e)]{B}
    {\infer[(ue)]{A(\in^1_xA) \to B}{\deduce{\forall x (A \to B)}{1}} &
    \infer[(ee)]{A(\in^1_xA)}{\deduce{\exists x A}{2}}}}}
\qquad
\infer[(\to i),1]{(A \to \exists x B) \to \exists x (A \to B)}
    {\infer[(ei)]{\exists x (A \to B)}{\infer[(\to i),2]{A \to 
B(\in^1_xB)}
    {\infer[(ee)]{B(\in^1_xB)}{\infer[(\to e)]{\exists x B}
    {\deduce{A \to \exists x B}{1} & \deduce{A}{2}}}}}}
$$
\vspace*{2mm}
H10,H11���ȒP�ɏؖ��ł���B

$$
\infer[(\to i),1]{[t/x]A \to t \in \{x:A\}}{\infer[(ci)]
    {t \in \{x:A\}}{\deduce{[t/x]A}{1}}}
\qquad
\infer[(\to i),1]{t \in \{x:A\} \to [t/x]A}{\infer[(ce)]
    {[t/x]A}{\deduce{t \in \{x:A\}}{1}}}
$$

G�̖���������White���ؖ������B

%% ��U��
\section{�̌nH�̖�������}
\begin{df}\label{ma}(maximally G-consistent)

X,M��formula�̏W���Ƃ���B

$\cdot$ X��G-inconsistent�ł���Ƃ́A����G��proof $\vcenter{\deduce{\bot}
{\displaystyle \Sigma}}$�����݂��āA���̂��ׂĂ̗����Ă��Ȃ������
formula��X�ɑ����Ă��邱�Ƃł���B

$\cdot$ X��G-consistent�ł���Ƃ́AX��G-inconsistent�łȂ����Ƃł���B

$\cdot$ M��maximally G-consistent�ł���Ƃ́AM��G-consistent���A
�C�ӂ�formula A�ɑ΂���$M \cup \{A\}$��G-consistent�Ȃ��
A��M�ɑ����Ă��邱�Ƃł���B
\end{df}

\begin{thm}
M��C�ӂ�maximally G-consistent�ȏW���Ƃ���BM�͎��̂悤�Ȑ��������B

M1. A��G��theorem�Ȃ�΁AA��M�Ɋ܂܂��B

M2. A��$A \to B$��M�Ɋ܂܂��΁AB��M�Ɋ܂܂��B

M3. $\forall x A$��closed�Ȃ�΁A$\tau^n_xA$��term�ł���B
���̂Ƃ��A$A(\tau^n_xA)$��M�Ɋ܂܂��΁A$\forall x A$��M�Ɋ܂܂��B

M4. �C�ӂ�formula A�ɑ΂��āAA��M�Ɋ܂܂�Ȃ���΁A$A^n \to f$��
M�Ɋ܂܂��(n�͐��̐���)�B
\end{thm}

proof.

M1. $A$��G��theorem����$A$��M�Ɋ܂܂�Ȃ��Ƃ���B
��`\ref{theo}���A���_��$A$�ł���G��categorical proof�����݂���B
�����$\vcenter{\deduce{A}{\Sigma}}$�Ƃ���B
��`\ref{ma}���A$M \cup \{A\}$��G-inconsistent�łȂ���΂Ȃ�Ȃ��B
���Ȃ킿�A����proof $\vcenter{\deduce{\bot}{\Pi}}$�����݂��āA����
�����Ă��Ȃ������M�Ɋ܂܂�邩$A$�ł���B$\vcenter{\deduce{\bot}{\Pi}}$
�Ɍ���闎���Ă��Ȃ�����$A$��$\vcenter{\deduce{A}{\Sigma}}$��
����������proof��$\vcenter{\deduce{\bot}{\Pi_1}}$�Ƃ���ƁA����
�����Ă��Ȃ������M�Ɋ܂܂��B���Ȃ킿�AM��G-inconsistent�ƂȂ�B

M2. $A, A \to B$��M�Ɋ܂܂�邪�A$B$��M�Ɋ܂܂�Ȃ��Ƃ���B
$M \cup \{B\}$��G-inconsistent�łȂ���΂Ȃ�Ȃ��B
���Ȃ킿�A����proof $\vcenter{\deduce{\bot}{\Sigma}}$�����݂��āA����
�����Ă��Ȃ������M�Ɋ܂܂�邩$B$�ł���B
$\vcenter{\deduce{\bot}{\Sigma}}$�Ɍ���闎���Ă��Ȃ�����$B$��

$$
\infer[(\to e)]{B}{\deduce{A \to B}{i} & \deduce{A}{j}}
\qquad
i,j�͓K���Ȑ��̐���
$$

�ł���������proof��$\vcenter{\deduce{\bot}{\Sigma_1}}$�Ƃ���ƁA����
�����Ă��Ȃ������M�Ɋ܂܂��B���Ȃ킿�AM��G-inconsistent�ƂȂ�B

M3. $A(\tau^n_xA)$��M�Ɋ܂܂�邪�A$\forall x A$��M�Ɋ܂܂�Ȃ��Ƃ���B
���l�ɁA�����Ă��Ȃ�����$\forall x A$��

$$
\infer[(ui)]{\forall x A}{\deduce{A(\tau^n_xA)}{k}}
$$

�ł���������΂悢�B

M4. $A$��M�Ɋ܂܂�Ȃ��Ȃ�΁A�����Ă��Ȃ����肪�A
$\vcenter{\deduce{B_1}{k_1}}$$\vcenter{,\ldots ,\deduce{B_m}{k_m} ,
\deduce{A}{p_1} ,\ldots ,\deduce{A}{p_n}}$�ł���悤��proof
$\vcenter{\deduce{\bot}{\Sigma}}$�����݂���(�e$B_i$��$M$�Ɋ܂܂��)�B
$\vcenter{\deduce{\bot}{\Sigma}}$��$\to i$��$m+n$��K�p���邱�Ƃɂ���āA
$B_1 \to \cdots \to B_m \to A^n \to \bot$��categorical proof��������B
�����M2��$m$��K�p����΂悢�B

\begin{df}
$H_1$�̏ؖ��}�̍������A���̂悤�ɋA�[�I�ɒ�`����B

$\cdot$ $H_1$�̌����́A����0�̏ؖ��}�ł���B

$\cdot$ $\vcenter{\deduce{A}{\Sigma}}$������$\alpha$�̏ؖ��}�Ȃ�΁A
$\vcenter{\infer{\forall x A}{\deduce{A}{\Sigma}}}$�́A
����$\alpha +1$�̏ؖ��}�ł���B

$\cdot$ $\vcenter{\deduce{A \to B}{\Sigma}}$��$\vcenter{\deduce{A}
{\Pi}}$�����ꂼ�ꍂ��$\alpha ,\beta$�̏ؖ��}�Ȃ�΁A
$\vcenter{\infer{B}{\deduce{A \to B}{\Sigma} & \deduce{A}{\Pi}}}$�́A
����$max(\alpha ,\beta )+1$�̏ؖ��}�ł���B

$\cdot$ $\Big{\{} \vcenter{\deduce{(A^i \to \bot) \to A}{\Sigma_i}}\Big{\}} 
_{1 < i < \omega}$�����ꂼ�ꍂ��$\alpha_1 ,\alpha_2 ,\ldots$
�̏ؖ��}�Ȃ�΁A
$\vcenter{\infer{A}{\Big{\{} \vcenter{\deduce{(A^i \to \bot) \to A}
{\Sigma_i}}\Big{\}}_{1 < i < \omega}}}$�́A
����$Sup\{\alpha_i |1 < i < \omega \}$�̏ؖ��}�ł���B
\end{df}

\begin{df}(pure)

$H_1$�̏ؖ��}��pure�ł���Ƃ́A���̏ؖ��}�̂��ׂĂ�subproof
$\vcenter{\infer{\forall x A}{\deduce{A}{\Sigma}}}$�ɂ��āA
�ϐ�x��$\vcenter{\deduce{A}{\Sigma}}$�ɂ�������Ȃ����Ƃł���B
\end{df}

\begin{thm}
���ׂĂ�$H_1$�̏ؖ��}��pure�ɂł���B
\end{thm}

\begin{thm}\label{su}
�C�ӂ�$H_1$�̏ؖ��}$\Sigma$��closed term t�ɑ΂��āA$\Sigma$��subproof
$\vcenter{\infer{\forall x A}{\deduce{A}{\Pi}}}$�������Ȃ���΁A
$[t/x]\Sigma $��$H_1$�̏ؖ��}�ł���B
\end{thm}

H�̖��������͎��̒藝���玦�����B

\begin{thm}

$\vcenter{\deduce{A}{\Sigma}}$��$H_1$��pure proof�Ƃ���B
���̌��_A��closed�Ȃ�΁AA�͂��ׂĂ�maximally G-consistent set�Ɋ܂܂��B
\end{thm}

proof.

$\vcenter{\deduce{A}{\Sigma}}$�̍����Ɋւ���transfinite induction�ɂ��B

M��maximally G-consistent set�Ƃ���B

$\vcenter{\deduce{A}{\Sigma}}$��$H_1$��closed axiom�Ȃ�΁AA��G��
theorem������AA��M�Ɋ܂܂��B

$\vcenter{\deduce{A}{\Sigma}}$��$\vcenter{\infer{A}{\Big{\{} \vcenter
{\deduce{(A^i \to \bot) \to A}{\Sigma_i}}\Big{\}}_{1 < i < \omega}}}$�Ȃ�΁A
A��closed�Ȃ̂ł��ꂼ���$(A^i \to \bot) \to A$��closed�A�A�[�@�̉���ɂ��A
������M�Ɋ܂܂��BA��M�Ɋ܂܂�Ȃ��Ƃ���ƁAM4�ɂ�肻�ꂼ���
$(A^i \to \bot)$��M�Ɋ܂܂��B���ꂼ���$(A^i \to \bot) \to A$��
M�Ɋ܂܂�邩��AM2�ɂ��A��M�Ɋ܂܂�邱�ƂɂȂ�B����āA
A��M�Ɋ܂܂�Ȃ���΂Ȃ�Ȃ��B

$\vcenter{\deduce{A}{\Sigma}}$��$\vcenter{\infer{A}
{\deduce{B \to A}{\Sigma_1} & \deduce{B}{\Sigma_2}}}$�Ƃ���B
$b_1,\ldots ,b_n$��B�����ϐ��Ƃ��AB��$B(b_1,\ldots ,b_n)$�ŕ\���B
$\vcenter{\deduce{A}{\Sigma}}$��pure������A���ׂĂ�$b_i$��
$\vcenter{\deduce{B \to A}{\Sigma_1}}$ , $\vcenter{\deduce{B}{\Sigma_2}}$��
generalization rule�̕ϐ��ł͂Ȃ��B�藝\ref{su}�ɂ��A
$\vcenter{\deduce{B \to A}{\Sigma_1}}$ , $\vcenter{\deduce{B}{\Sigma_2}}$��
�e$b_i$��closed term t������������
$\vcenter{\deduce{B(t,\ldots ,t) \to A}{\Sigma_3}}$ ,
$\vcenter{\deduce{B(t,\ldots ,t)}{\Sigma_4}}$��H$_1$�̏ؖ��}�ł���B
$\vcenter{\deduce{B(t,\ldots ,t) \to A}{\Sigma_3}}$ ,
$\vcenter{\deduce{B(t,\ldots ,t)}{\Sigma_4}}$�̍����͂��ꂼ��
$\vcenter{\deduce{B \to A}{\Sigma_1}}$ , $\vcenter{\deduce{B}{\Sigma_2}}$
�̍����Ɠ������B�A�[�@�̉���ɂ��A$B(t,\ldots ,t) \to A,
 B(t,\ldots ,t)$��M�Ɋ܂܂��BM2�ɂ��A��M�Ɋ܂܂��B

$\vcenter{\deduce{A}{\Sigma}}$��$\vcenter{\infer{\forall y B}
{\deduce{B}{\Pi}}}$�Ƃ���B$\forall y B$��closed�Ȃ̂�
$\tau^n_yB$��term�ł���B
$\vcenter{\deduce{A}{\Sigma}}$��pure������A�藝\ref{su}�ɂ��A
$\vcenter{\deduce{B}{\Pi}}$��$y$��$\tau^n_yB$������������
$\vcenter{\deduce{[\tau^n_yB(y)/y]B}{\Pi_1}}$��H$_1$�̏ؖ��}�ł���B
$[\tau^n_yB(y)/y]B $��closed�A�A�[�@�̉���ɂ��A$[\tau^n_yB(y)/y]B $��
M�Ɋ܂܂��BM3�ɂ��$\forall y B(y)$��M�Ɋ܂܂��B

\begin{cor}
���ׂĂ�A�ɂ��āAA��$\neg A$���Ƃ���H�ŏؖ��ł���Ƃ������Ƃ͂Ȃ��B
\end{cor}

proof.

$A$��$\neg A$���Ƃ���H�ŏؖ��ł���Ȃ�΁A$\bot$��H��(H$_1$�ł�)�ؖ��ł���B
$\bot$��closed�Ȃ̂ŁA���ׂĂ�maximally G-consistent set�Ɋ܂܂�Ȃ����
�Ȃ�Ȃ��B���炩�ɁA$\bot$�͂ǂ̂悤��maximally G-consistent set�ɂ�
�܂܂�Ȃ��B�܂��AG�̂��ׂĂ�theorem����Ȃ�W����G-consistent
������Amaximally G-consistent set�͑��݂���B

%% ��V��
\section{$\lambda$-term�̓���}

�̌n$BCK\beta \eta$�͈ȉ��̂悤�ɒ�`�����B

\begin{df}($\lambda$-term)

$\cdot$ ���R�ϐ���term�ł���B

$\cdot$ �萔$\Xi$��term�ł���B

$\cdot$ A, B��term�Ȃ�΁A$(AB)$��term�ł���B

$\cdot$ A��term�Ȃ�΁A$(\lambda x.A)$��term�ł���B
\end{df}

\begin{df}($\beta \eta$-equality)

$\cdot A =_{\beta \eta} A$

$\cdot \lambda x.A =_{\beta \eta} \lambda y.[y/x]A$(y��A�Ɏ��R�Ɍ���Ȃ�)

$\cdot (\lambda x.A)B =_{\beta \eta} [B/x]A$

$\cdot (\lambda x.A)x =_{\beta \eta} A$

$\cdot A =_{\beta \eta} B$ �Ȃ�� $CA =_{\beta \eta} CB$

$\cdot A =_{\beta \eta} B$ �Ȃ�� $AC =_{\beta \eta} BC$

$\cdot A =_{\beta \eta} B$ �Ȃ�� $\lambda x.A =_{\beta \eta} \lambda x.B$

$\cdot A =_{\beta \eta} B$ ���� $B =_{\beta \eta} C$ �Ȃ�� $A =_{\beta \eta} C$

$\cdot A =_{\beta \eta} B$ �Ȃ�� $B =_{\beta \eta} A$
\end{df}
 
�̌n$BCK\beta \eta$�ɂ����ẮA���ׂĂ�term��formula�ł���B
�̌n$BCK\beta \eta$�̐��_�K���͎���3�ł���B

\vspace*{5mm}

{\large\gt Inference Rules}
$$
$$
$\Xi$ Introduction
$$
\infer[(\Xi i),k]{\Xi AB}{\deduce{Bx}{\deduce{\Sigma}{\deduce{Ax}{k}}}}
\qquad
�ϐ�x��A,B����ї����Ă��Ȃ�����Ɏ��R�Ɍ���Ȃ��B
$$
$\Xi$ Elimination
$$
\infer[(\Xi e)]{BC}{\deduce{\Xi AB}{\Sigma} & \deduce{AC}{\Pi}}
\qquad
\vcenter{\deduce{\Xi AB}{\Sigma}}��\vcenter{\deduce{AC}{\Pi}}��disjoint
$$
$\beta \eta$ equality
$$
\infer[(\beta \eta)]{B}{\deduce{A}{\Sigma}}
\qquad
A =_{\beta \eta} B
$$

\begin{df}

$A \to B \equiv \Xi (KA)(KB)$, $K \equiv \lambda xy.x$,

$T \equiv \Xi II$, $I \equiv \lambda x.x$,

$\forall xA \equiv \Xi (KT)(\lambda x.A)$,

$\exists xA \equiv \forall y(\forall x(A \to y) \to y)$,

$B \in A \equiv AB$,

$\{x:A\} \equiv \lambda x.A$,

$\bot \equiv \forall xx$.
\end{df}

\begin{df}(categorical proof)

�����Ă��Ȃ����肪���݂��Ȃ��ؖ��}�̂��Ƃ�categorical proof�Ƃ����B
\end{df}

\begin{thm}
G*�̐��_�K���́A$\vee$�ȊO��$BCK\beta \eta$��derived rule�Ƃ��ē�����B
\end{thm}

proof. $\to e$, $ui$, $ue$�̂ݎ����B

$$
\infer[(\beta \eta)]{B}{\infer[(\Xi e)]{KBC}{\deduce{A \to B}{\Sigma}
    & \infer[(\beta \eta)]{KAC}{\deduce{A}{\Pi}}}}
\qquad
\infer[(\Xi i),1]{\forall xA}{\infer[(\beta \eta)]{(\lambda x.A)x}
    {\infer[(\Xi e)]{IA}{\infer[(\beta \eta)]{T}{\deduce{KTx}{1}}
    & \infer[(\beta \eta)]{IA}{\deduce{A}{\Sigma}}}}}
\qquad
\infer[(\Xi e)]{(\lambda x.A)t}{\deduce{\forall xA}{\Sigma}
    & \infer[(\beta \eta)]{KTt}{\infer[(\Xi i),1]{T}
    {\deduce{Ix}{1}}}}
$$

\vspace*{2mm}
$BCK\beta \eta$�̖��������͂��łɏؖ�����Ă���(\cite{ko})�B
$BCK\beta \eta$�ɁA���_�K��
$$
\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Sigma}}
\qquad
A \vee B \equiv (A \to B) \to B
$$
���������̌n(G*�̊g���ɂȂ��Ă���)�̖����������ȉ��Ɏ����B

\begin{thm}\label{in}(Invariance of form)

a,b��non-redex atom(�萔�܂��͎��R�ϐ�)�ŁA
$$aX_1\ldots X_k =_{\beta \eta} bY_1\ldots Y_n$$
�Ȃ�΁A$a \equiv b$, $k = n$, $X_i =_{\beta \eta} Y_i$ 
(for $i = 1,\ldots ,n$)�B
\end{thm}

proof. Church-Rosser theorem(cf. \cite{hi})�ɂ��B

\begin{cor}

�C�ӂ�term A,B,C,D�ɑ΂���$\Xi AB =_{\beta \eta} \Xi CD$�Ȃ��
$A =_{\beta \eta} C$ ���� $B =_{\beta \eta} D$
\end{cor}

\begin{df}(reduction)
\vspace*{5mm}

{\large\gt $\Xi$-reduction}

\vspace*{5mm}
$$
\infer[(\Xi e)]{BC}{\infer[(\Xi i),k]{\Xi AB}{\deduce{Bx}{\deduce{\Sigma}
    {\deduce{Ax}{k}}}} & \deduce{AC}{\Pi}}
$$
�Ƃ���������
$$
\deduce{BC}{\deduce{[C/x]\Sigma}{\deduce{AC}{\Pi}}}
$$
�Œu��������B

{\large\gt Eq$\beta \eta$-reduction}

\vspace*{5mm}
$$
\infer[(\beta \eta)]{C}{\infer[(\beta \eta)]{B}{\deduce{A}{\Sigma}}}
$$
�Ƃ���������
$$
\infer[(\beta \eta)]{C}{\deduce{A}{\Sigma}}
$$
�Œu��������B
\vspace*{5mm}

{\large\gt $\Xi$-Eq$\beta \eta$-reduction}

\vspace*{5mm}
$$
\infer[(\beta \eta)]{\Xi CD}{\infer[(\Xi i),k]{\Xi AB}{\deduce{Bx}
    {\deduce{\Sigma}{\deduce{Ax}{K}}}}}
$$
�Ƃ���������
$$
\infer[(\Xi i),k]{\Xi CD}{\infer[(\beta \eta)]{Dy}{\deduce{By}
    {\deduce{[y/x]\Sigma}{\infer[(\beta \eta)]{Ay}{\deduce{Cy}{k}}}}}}
\qquad
y��A,B�Ɍ���Ȃ�
$$
�Œu��������B
\end{df}

\begin{df}(weakly normal)

reduction������ȏ�ł��Ȃ��ؖ��}��
weakly normal�Ƃ����B
\end{df}

\begin{thm}

���ׂĂ̏ؖ��}�͗L�����reduction���{����
weakly normal�ɂ��邱�Ƃ��ł���B
\end{thm}

proof.�@�ؖ��}�̒����Ɋւ���A�[�@(cf.\cite{ko})

\begin{df}(categorical $\vee$)

$\vcenter{\infer[(\vee)]{B \vee A}{\deduce{A \vee B}{\Sigma}}}$
��$\vee$��categorical�ł���Ƃ́A$\vcenter{\deduce{A \vee B}{\Sigma}}$
��categorical�ł��邱�Ƃł���B
\end{df}

\begin{df}(normal)

weakly normal���Acategorical��$\vee$�������Ȃ��ؖ��}��
normal�Ƃ����B
\end{df}

\begin{thm}
�����ϐ�x�����_�ł���categorical proof�����݂���΁Anormal�Ȃ��̂����݂���B
\end{thm}

proof. �藝\ref{no}�̏ؖ��Ƃقړ��l

\begin{thm}
�ϐ�x�����_�ł���normal categorical proof�͑��݂��Ȃ��B
\end{thm}

proof. 

�ϐ�x�����_�ł���normal categorical proof�����݂����Ƃ���B

Case 1.�@�Ō��$\Xi$�Ɋւ��鐄�_�K����$\Xi i$�̂Ƃ�

$\Xi AB =_{\beta \eta} x$�ƂȂ�term $A,B$�����݂��Ȃ���΂Ȃ�Ȃ����A
�藝\ref{in}���A����͂��蓾�Ȃ��B

Case 2.�@�Ō��$\Xi$�Ɋւ��鐄�_�K����$\Xi e$�̂Ƃ�

���̕�����
$$
\infer[(\Xi e)]{BC}{\deduce{\Xi AB}{\Sigma} & \deduce{AC}{\Pi}}
$$
�Ƃ���B$\vcenter{\deduce{\Xi AB}{\Sigma}}$�̍Ō�̐��_�K����
$\Xi i$, $\vee$�ł͂Ȃ�(normal���)�B$\Xi e$�܂���$\beta \eta$�ł���B
$\Xi e$�̂Ƃ��A���̏�̍Ō�����l��$\Xi e$�܂���$\beta \eta$�ł���B
$\beta \eta$�̂Ƃ��A���̏�̍Ō��$\beta \eta$, $\vee$�ł͂Ȃ�(normal���)�B
�܂��A$\Xi i$�ł��Ȃ�\Big{(}$\vcenter{\deduce{\Xi AB}{\Sigma}}$��
$\vcenter{\infer[(\beta \eta)]{\Xi AB}{\deduce{\Xi CD}{\Sigma_1}}}$
�Ȃ��normal���A�����łȂ��ꍇ\Big{(}$\vcenter{\infer[(\beta \eta)]{\Xi AB}
{\deduce{K(\Xi AB)x}{\Sigma_1}}}$�Ȃ�\Big{)}�͌`����\Big{)}�B����āA$\Xi 
e$�ł���B
������ɂ��Ă��A$\Xi e$��$\beta \eta$��������Ȃ��������邩��A
categorical proof�ɂȂ蓾�Ȃ��B


%% ��W��
\section{�⑫}

H�̌���

H1.  $A \to B \to A$.

H2.  $(A \to B) \to (B \to C) \to A \to C$.     

H3.  $A \vee B \to B \vee A$.

H4.  $(\neg A \to \neg B) \to B \to A$.

��modus ponens����A
$$(A \to B) \vee (B \to A)$$
���o�邱�Ƃ��A�ȉ��̂悤�Ɏ���(cf. \cite{ro},\cite{me})�B

�܂��A(1)$A \to A \vee B$�����̏ؖ��}�ɂ���ē���B
$$
\infer{A \to A \vee B}{\infer{(B \vee A \to A \vee B) \to A \to A \vee B}
    {\deduce{(A \to B \vee A) \to (B \vee A \to A \vee B) \to A \to A \vee B}
    {H2} & \deduce{A \to B \vee A}{H1}} & \deduce{B \vee A \to A \vee B}{H3}}
$$
H2���A
$$((A \to B \to C) \to B \vee C \to A \to C)$$ $$\to ((B \vee C \to A \to C)
\to B \to A \to C) \to (A \to B \to C) \to B \to A \to C$$
H2���A
$$(A \to B \to C) \to B \vee C \to A \to C$$
����炩��A
$$((B \vee C \to A \to C) \to B \to A \to C) 
\to (A \to B \to C) \to B \to A \to C$$
�܂��A
$$\infer{(B \vee C \to A \to C) \to B \to A \to C}{\deduce
   {(B \to B \vee C) \to (B \vee C \to A \to C) \to B \to A \to C}{H2}
    & \deduce{B \to B \vee C}{(1)}}$$
����āA
$$(A \to B \to C) \to B \to A \to C \cdots (C)$$
�𓾂�B

(C)���A
$$((A \to B) \to (B \to C) \to A \to C) 
\to (B \to C) \to (A \to B) \to A \to C$$
�����H2���A
$$(B \to C) \to (A \to B) \to A \to C \cdots (B)$$
�𓾂�B

���ɁA(2)$((B \to A) \to B \to C) \to (A \to B) \to A \to C$�������B

H2���A
$$(((A \to B) \to C \to B) \to C \to A \vee B)$$ $$\to ((C \to A \vee B)
 \to C \to B \vee A) \to ((A \to B) \to C \to B) \to C \to B \vee A$$

(C)���A
$$((A \to B) \to C \to B) \to C \to A \vee B$$
�܂��A(B)���A
$$(A \vee B \to B \vee A) \to (C \to A \vee B) \to C \to B \vee A$$
�����H3���A
$$(C \to A \vee B) \to C \to B \vee A$$
�ȏォ��A
$$((A \to B) \to C \to B) \to C \to B \vee A$$
�𓾂�B(C)���A
$$(((A \to B) \to C \to B) \to C \to B \vee A)$$
$$\to ((A \to B) \to C \to B) \to (B \to A) \to C \to A$$
����āA
$$((A \to B) \to C \to B) \to (B \to A) \to C \to A$$
�𓾂�B������A
$$((\neg A \to \neg B) \to \neg C \to \neg B) 
\to (\neg B \to \neg A) \to \neg C \to \neg A \cdots(3)$$

H2���A
$$((\neg A \to \neg B) \to B \to A) \to ((B \to A) \to B \to C)
 \to (\neg A \to \neg B) \to B \to C$$
H4���A
$$(\neg A \to \neg B) \to B \to A$$
����炩��A
$$((B \to A) \to B \to C) \to (\neg A \to \neg B) \to B \to C \cdots(4)$$
�܂��A(B)���A
$$((B \to C) \to \neg C \to \neg B) \to ((\neg A \to \neg B) \to B \to C)
 \to (\neg A \to \neg B) \to \neg C \to \neg B$$
H2���A
$$(B \to C) \to \neg C \to \neg B$$
����炩��A
$$((\neg A \to \neg B) \to B \to C) 
\to (\neg A \to \neg B) \to \neg C \to \neg B$$ 
�����(4)�AH2���A
$$((B \to A) \to B \to C) \to (\neg A \to \neg B) \to \neg C \to \neg B$$
�����(3)�AH2���A
$$((B \to A) \to B \to C) \to (\neg B \to \neg A) 
\to \neg C \to \neg A \cdots(5)$$
�𓾂�B
H2���A
$$((A \to B) \to \neg B \to \neg A) \to ((\neg B \to \neg A) 
\to \neg C \to \neg A) \to (A \to B) \to \neg C \to \neg A$$
H2���A
$$(A \to B) \to \neg B \to \neg A$$
����炩��A
$$((\neg B \to \neg A) \to \neg C \to \neg A) 
\to (A \to B) \to \neg C \to \neg A \cdots(6)$$
�܂��A(B)���A
$$((\neg C \to \neg A) \to A \to C) \to ((A \to B) \to \neg C \to \neg A)
 \to (A \to B) \to A \to C$$
H4���A
$$(\neg C \to \neg A) \to A \to C$$
����炩��A
$$((A \to B) \to \neg C \to \neg A) \to (A \to B) \to A \to C$$
�����(6)�AH2���A
$$((\neg B \to \neg A) \to \neg C \to \neg A) \to (A \to B) \to A \to C$$
�����(5)�AH2���A
$$((B \to A) \to B \to C) \to (A \to B) \to A \to C \cdots(2)$$
�𓾂�B

H2���A
$$(A \vee B \to B \vee A)$$
$$\to (B \vee A \to (A \to B) \to A) \to A \vee B \to (A \to B) \to A$$
�����H3���A
$$(B \vee A \to (A \to B) \to A) \to A \vee B \to (A \to B) \to A \cdots(7)$$
�܂��AH2���A
$$(((A \to B) \to B \to A) \to B \vee A \to (A \to B) \to A)$$
$$\to ((B \vee A \to (A \to B) \to A) \to A \vee B \to (A \to B) \to A)$$
$$\to ((A \to B) \to B \to A) \to A \vee B \to (A \to B) \to A$$
H2���A
$$((A \to B) \to B \to A) \to B \vee A \to (A \to B) \to A$$
�����(7)���A
$$((A \to B) \to B \to A) \to A \vee B \to (A \to B) \to A$$
H2���A
$$(((A \to B) \to B \to A) \to A \vee B \to (A \to B) \to A)$$
$$\to ((A \vee B \to (A \to B) \to A) \to (B \to A \to B) \to B \to A)$$
$$\to ((A \to B) \to B \to A) \to (B \to A \to B) \to B \to A$$
����炩��A
$$((A \vee B \to (A \to B) \to A) \to (B \to A \to B) \to B \to A)$$
$$\to ((A \to B) \to B \to A) \to (B \to A \to B) \to B \to A$$
(2)���A
$$(A \vee B \to (A \to B) \to A) \to (B \to A \to B) \to B \to A$$
����炩��A
$$(A \to B) \to B \to A) \to (B \to A \to B) \to B \to A$$
(C)���A
$$(((A \to B) \to B \to A) \to (B \to A \to B) \to B \to A)$$
$$\to (B \to A \to B) \to (A \to B) \vee (B \to A)$$
����炩��A
$$(B \to A \to B) \to (A \to B) \vee (B \to A)$$
H1���A
$$B \to A \to B$$
����āA
$$(A \to B) \vee (B \to A)$$
�𓾂�B

\vspace*{5mm}

G*(G)�ɂ�����$(A \to B) \vee (B \to A)$�̏ؖ�

$$
\infer[(\to i),4]{(A \to B) \vee (B \to A)}{\infer[(\to i),9]{B \to A}
   {\infer[(dn),6]{A}{\infer[(\to e)]{\bot}{\deduce{\neg B}{\Sigma}
   & \deduce{B}{9}}}}}
$$
$$
\Sigma \equiv \vcenter{
\infer[(\to e)]{\neg B}{\infer[(\vee)]{\neg (A \to B) \vee \neg B}
    {\infer[(\to i),1]{\neg B \vee \neg (A \to B)}{\infer[(\to i),5]
    {\neg (A \to B)}{\infer[(\to e)]{\bot}{\deduce{\neg A}{6} & 
    \deduce{A}{\Pi}}}}} & \infer[(\to i),8]{\neg (A \to B) \to \neg B}
    {\infer[(\to i),7]{\neg B}{\infer[(\to e)]{\bot}{\deduce{\neg (A \to B)}
    {8} & \infer[(\to i),10]{A \to B}{\deduce{B}{7}}}}}}
}
$$
$$
\Pi \equiv \vcenter{
\infer[(\to e)]{A}{\infer[(\vee)]{B \vee A}{\infer[(\to i),3]{A \vee B}
    {\infer[(dn),2]{B}{\infer[(\to e)]{\bot}{\infer[(\to e)]{\neg (A \to B)}
    {\deduce{\neg B \to \neg (A \to B)}{1} & \deduce{\neg B}{2}} & 
    \deduce{A \to B}{3}}}}} & \infer[(\to e)]{B \to A}
    {\deduce{(A \to B) \to B \to A}{4} & \deduce{A \to B}{5}}}
}
$$

%% ��X��
\section{������}

�{�_���ł͑̌nG*�̖����������ؖ��������A��������Ƃɑ̌nH�̖���������
�ؖ����邱�Ƃ��ł��邩�Ƃ������Ƃ܂ł͂킩��Ȃ������̂ŁA����̉ۑ�Ƃ������B

\newpage

\section*{�ӎ�}
�{�_���쐬�ɂ�����A�w�������̌ÐX�Y��搶�A���V�l������͂���
�ÐX�������̊F�l�A�͓��b����ɑ���Ȃ����͂𒸂��܂������Ƃ�
�S���犴�ӂ������܂��B

%% �Q�l����
\begin{thebibliography}{99}
\addcontentsline{toc}{section}{�Q�l����}
\bibitem{sh} Moh Shaw-Kwei,
{\it Logical paradoxes for many valued systems,}\
Journal of Symbolic Logic 19, (1954), pp.\ 37--40.

\bibitem{wh} Richard B. White,
{\it The consistency of the axiom of comprehension in the
infinite-valued predicate logic of \L ukasiewicz,}\
Journal of Philosophical Logic 8, (1979), pp.\ 509--534.

\bibitem{ha} Louise Schmir Hay,
{\it Axiomatization of the infinite-valued predicate calculus,}\
Journal of Symbolic Logic 28, (1963), pp.\ 77--86.

\bibitem{ko} Yuichi Komori,
{\it Illative combinatry logic based on $BCK$-logic,}\
Mathematica Japonicae 34, (1989), pp.\ 585--596.

\bibitem{hi} J. R. Hindrey and J. P. Seldin,
{\it Introduction to combinators and $\lambda$-calculus,}\
Cambridge University Press, (1986)

\bibitem{ro} Alan Rose and J. Barkley Rosser,
{\it Fragments of many-valued statement calculi,}\
Trans. Amer. Math. Soc. vol.87, (1958), pp.\ 1-53.

\bibitem{me} C. A. Meredith,
{\it The dependence of an axiom of \L ukasiewicz,}\
Trans. Amer. Math. Soc. vol.87, (1958), pp.\ 54.
\end{thebibliography}
\end{document}
