%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% これは『Ｑ & Ａ 数学基礎論入門、共立出版』を電子写植機 %%%
%%% にかけるために作ったテスト用 \LaTeX ファイルです.      %%%
%%% このファイルの使用には久馬栄道作の myjbook.sty と      %%%
%%% myjbk10.sty と def.tex, またアスキー出版作の ascmac.sty%%%
%%% が必要です.                                            %%%
%%% test1.tex に rename してお使いください.                %%%
%%%                                                        %%%
%%%                         愛知学院大学 教養部 久馬 栄道  %%%
%%%                          kyuma@dpc.aichi-gakuin.ac.jp  %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentstyle[b5j,ascmac]{myjbook}

\setcounter{tocdepth}{2}

\title{Q \& A 数学基礎論入門}
\date{\today}
\author{愛知学院大学 教養部 数学教室 \\ 久馬栄道}

\textheight 175mm
\textwidth 115mm

\input{def}

\begin{document}

\maketitle

\setcounter{page}{1}
\pagenumbering{roman}
\tableofcontents
\cleardoublepage
\pagenumbering{arabic}
\setcounter{page}{1}

\part{初級編}

\begin{flushright}
\framebox{
\begin{tabular}{p{6mm}cp{10mm}}
& & \\
&
\begin{minipage}{60mm}
\noindent
初級編では, おもに数学基礎論の基本
的なテクニックの習得を行なう. 
読者はなるべく手元に紙と鉛筆を置き, 
手を動かしながら問題を解くように
して欲しい. 
困難な問題は先に答えを見てもよいが, 
その場合でも後で必ず手を動かして
解いてみることが大事である. 
\end{minipage}
& \\
& & 
\end{tabular}}
\end{flushright}

\cleardoublepage


\chapter{基礎の知識}

\sec{命\hspace{3.5pt}題\hspace{3.5pt}論\hspace{3.5pt}理}

\begin{problem}
$((\Not A) \Imp B)\Iff ((\Not B) \Imp A)$ がトートロジーであることを示せ. 
\end{problem}

真理値表を書いてもよいが, すでに以前の問題で, 
 $(A \Imp B)\Iff((\Not B)\Imp(\Not A))$ と
 $(A\Imp \Not(\Not B)) \Iff (A\Imp B)$ 
のトートロジーがいえている.  
$$
\begin{array}{c}
\begin{array}{ccc}
(A \Imp B)\Iff((\Not B)\Imp(\Not A)) & 　 & 
(A\Imp \Not(\Not B)) \Iff (A\Imp B) \\
\Downarrow \;\;\mbox{\footnotesize $A$ を $\Not A$ に置き換える} & & 
\Downarrow \;\;\mbox{\footnotesize $A$ を $\Not B$ に, $B$ を $A$ に} \\
((\Not A) \Imp B)\Iff((\Not B)\Imp \Not(\Not A)) & & 
((\Not B)\Imp \Not(\Not A)) \Iff ((\Not B) \Imp A) 
\end{array} \\
\Downarrow\;\;\mbox{\footnotesize 前の問題で組み合わせる}\;\;\Downarrow \\
((\Not A) \Imp B) \Iff ((\Not B) \Iff A)
\end{array}
$$
となって証明できる. 

\begin{eqnarray*}
(A \Imp(B\Imp C))\Imp (A \Imp C) & が & D \;\;で, \\
(A\Imp B) \Imp ((A \Imp(B\Imp C))\Imp (A \Imp C)) & が & E \;\;であった
\mbox{. }
\end{eqnarray*}
\begin{center}
\begin{tabular}{|c|c|c||c|c|c|c|c|c|}
	\hline 
	$A$ & $B$ & $C$ & $A \Imp B$ & $B \Imp C$ 
	& $A \Imp (B \Imp C)$ 
	& $A \Imp C$ 
	& $D$ & $E$ \\
	\hline   
	\hline
	$T$ & $T$ & $T$ & $T$ & $T$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
	$T$ & $T$ & $F$ & $T$ & $F$ &$F$ & $F$ & $T$ & $T$ \\ \hline	
	$T$ & $F$ & $T$ & $F$ & $T$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
	$T$ & $F$ & $F$ & $F$ & $T$ &$T$ & $F$ & $F$ & $T$ \\ \hline	
	$F$ & $T$ & $T$ & $T$ & $T$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
	$F$ & $T$ & $F$ & $T$ & $F$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
	$F$ & $F$ & $T$ & $T$ & $T$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
	$F$ & $F$ & $F$ & $T$ & $T$ &$T$ & $T$ & $T$ & $T$ \\ \hline	
\end{tabular}	
\end{center}

\begin{problem}
『100歳以上の二人の人間が存在し, 彼らは双子である』
という文章を述語論理で書け. 
素論理式は適当に考えよ. 
\end{problem}

『$x$ は人間』と『$x$ と $y$ は双子』と『$x$ は100歳以上』を
素論理式とすると, 
$$
\exists \;x\;\left(\exists \;y\;\left(
\begin{array}{l}
(x \;は人間) \And(x \;は100歳以上) \\
　　　\And(y\;は人間) \And (y\;は100歳以上)\And(x\;と\;y\;は双子)
\end{array}
\right)\right)
$$
となる. 
この文章はきんさん・ぎんさんが存在するので、いまのところ
(1995年７月現在)正しい. 

\begin{problem}
『３以上の自然数 $n$ に対して, $x^n+y^n=z^n$ となる
１以上の自然数 $x,y,z$ は存在
しない』というのを述語論理で書け. 
\end{problem}

これを{\gt フェルマーの最終定理}
(正確にいえば定理ではなく最終問題とでもいうべきだが)
といい, 数学上の超難問であった
\footnote{
フェルマーの最終定理はいままでに何回となく『解けた』と発表する
学者がいて、かなりいい線はいっているものの結局は間違っていた, 
という繰り返しの歴史であった. 
そのようなこともあり1994年にアンドリュー・ワイルズが解けたとインターネットに
流れたときも, 慎重にかなり長い間をかけて検討されたが, 
その結果どうやら正真正銘の正しい証明らしい. 
%既に数学専門雑誌のレフリー
%(一般に数学専門雑誌に掲載するときにはレフリーといわれる人の審査が必要)
%もとうり、もうすぐ(現在は1995年４月)雑誌にも掲載されるらしい. 
このことに大打撃を受けている学者は
(コミック・モーニングの『菜』の旦那さん以外にも)世界中でかなり
多いはずである. }. 

１以上の自然数の部分を簡単にするため、
$N^+ = \big\{n\;\big|\;(nは自然数)\And(n > 0)\big\}$ とする. 
さて問題の解答は 
$$\forall \;n \in N^+ \Biggl((n \geq 3) \Imp \Not \Biggl(\exists \;x \in N^+
\biggl(\exists \;y \in N^+ \Bigl(\exists \;z\in N^+
(x^n+y^n=z^n)\Bigr)\Biggr)\Biggr)$$
となる
\footnote{それはそうとして, 
念のために括弧の数が正しいか確かめるのも大事である. }. 


\begin{problem}
２つの集合 $a$ と $b$ に対して, その元 $x\in a$ と $y\in b$ とが対応して
いることを $x \sim y$ と書くことにする. 
そのとき $a$ と $b$ が１対１対応であることを述語論理を用いて表せ. 
\end{problem}

はっきりいって相当難しいが, 頑張るように. 

つぎの４つのことがいえれば１対１対応である. 
\begin{eqnarray*}
& & \forall \;x \in a\;\exists \;y \in b (x\sim y) \\
& & \forall \;x \in a\;\forall \;y_1 \; y_2 \in b 
\biggl(\Bigl((x\sim y_1)\And(x\sim y_2)\Bigr)\Imp (y_1=y_2)\biggr) \\
& & \forall \;y \in b\;\exists \;x \in a (x\sim y) \\
& & \forall \;y \in b\;\forall \;x_1 \; x_2 \in a 
\biggl(\Bigl((x_1\sim y)\And(x_2\sim y)\Bigr)\Imp (x_1=x_2)\biggr)
\end{eqnarray*}

このようなものは, とにかく式の多さに圧倒されずに冷静に１つずつ
かたをつけてよう. 

\begin{screen}
{\gt 雑談}　
この隣の部屋に移る方法は収束する等比級数の無限和 $S=a+ak+ak^2+ak^3+\cdots$ が 
$a \over 1-k$ になることに使っている. 
すなわち
\begin{center}
\begin{tabular}{ccccl}
　& $S$ & $=$ & $a+$ & $ak+ak^2+ak^3+\cdots$ \\
　& $kS$ & $=$ & & $ak+ak^2+ak^3+\cdots$ \\
\hline
　& $(1-k)S$ & $=$ & $a$ & \\
\end{tabular}
\end{center}
のように引き算をすれば 
{$S={a \over 1-k}$} になる. 
２列目の $k$ 倍したとき, 右辺の項が１つずつ右にずれることに注意せよ. 
\end{screen}

\begin{problem}
正の有理数全体の集合は可算か？
\end{problem}

可算である. 
可算であるためには１列に並べてやればよいので, 
正の有理数全体の集合 $\left\{\;{x \over y}\;\;|\; x,y\;は0でない自然数
\right\}$ を次のように並べる(これがどのようなルールで並べられているか
わかるか？). 
ただし, この中には $\frac{2}{1}=\frac{4}{2}=\frac{6}{3}=\cdots$ のように
同じものがあるので省く. 
{\def\Batu{\kern -0.5mm\surd\kern -3mm}
$$
\begin{array}{cccccccccccccccccccccccccccccccccccccccccccccccccccccccccc}
\frac{1}{1}& &
\frac{1}{2}&
\frac{2}{1}& &
\frac{1}{3}&
\Batu\frac{2}{2}&
\frac{3}{1}& &
\frac{1}{4}&
\frac{2}{3}&
\frac{3}{2}&
\frac{4}{1}& &
\frac{1}{5}&
\Batu\frac{2}{4}&
\Batu\frac{3}{3}&
\Batu\frac{4}{2}&
\frac{5}{1} \\
\updownarrow& &\updownarrow&\updownarrow& &\updownarrow&\updownarrow
&\updownarrow& &\updownarrow&\updownarrow&
\updownarrow&\updownarrow& &\updownarrow& \updownarrow&
\updownarrow & \updownarrow&\updownarrow & \\
0 & &
1 & 2 & &
3 &   & 4 & &
5 & 6 & 7 & 8 & &
9 &  &  &  & 10 & \\
\end{array}
$$
$$
\begin{array}{cccccccccccccccccccccccccccccccccccccccccccccccccccccccccc}
\frac{1}{6}&
\frac{2}{5}&
\frac{3}{4}&
\frac{4}{3}&
\frac{5}{2}&
\frac{6}{1}& &
\frac{1}{7}&
\Batu\frac{2}{6}&
\frac{3}{5}&
\Batu\frac{4}{4}&
\frac{5}{3}&
\Batu\frac{6}{2}&
\frac{7}{1}& &
\cdots \\
\updownarrow&\updownarrow&\updownarrow&\updownarrow&
\updownarrow&\updownarrow& &\updownarrow& \updownarrow&
\updownarrow& \updownarrow&\updownarrow& \updownarrow&\updownarrow& &  & \\
11 & 12 & 13 & 14 & 15 & 16 & &
17 &    & 18 &    & 19 &    & 20 &  & \cdots \\
\end{array}
$$}
そして, 上のように左から $0,1,2,3,4,5\ldots$ と番号を付けて
いけばよい. 

\begin{problem}
$4=\{0,1,2,3\}$ のべき集合を求めよ. 
\end{problem}

いままでの公理で $\{0,1,2,3\}$ が集合になることが証明できる. 
$$
\Power(4)=
\left\{
\begin{array}{l}
\phi,\{0\},\{1\},\{2\},\{3\},\\
　\{0,1\},\{0,2\},\{0,3\},\{1,2\},\{1,3\},\{2,3\}, \\
　　\{1,2,3\},\{0,2,3\},\{0,1,3\},\{0,1,2\},\{0,1,2,3\} 
\end{array}
\right\}$$
となる. 
$\phi$ がどのような集合に対しても部分集合になることはやった. 
$a=b$ ならば $a \subset b$ ということはすでに証明したので, 
$4=\{0,1,2,3\}$ 自身も部分集合であることに注意せよ. 

\bigskip

さて選択公理を考える. 
$$\forall \;T\;\;\exists \;S\left(\begin{array}{l}
\left(
\begin{array}{l}
\forall\; E\in T\;\Not(E=\phi)\\
　　\And \forall\; E_1\;E_2 \in T
\Big(\Not(E_1=E_2)\Imp(E_1\cap E_2 =\phi)\Big)\\
\end{array}
\right) \\
　　　　　　\Imp\forall\; E\in T\;\exists\;!\;x(x\in E \And x\in S) \\
\end{array}\right)$$
が選択公理を述語論理式で書いたものとなる. 
大変難しい形だが, ここまでの説明をよく理解して
１つ１つの意味をばらして考えよ. 

\def\br{\framebox{　} }
\def\sbr{{\Large $\Box$}}

\Turing{0}{}{s1{\clubsuit}s>021{T_1}{T_2}01s}


\Turing{5}{s_6}{s1{\clubsuit}s>021{T_1}{T_2}01s}

\begin{tabular}{|c||c|c|c|c|}
	\hline
	    & $s_0$ & $s_1$ & $s_2$ & $s_3$ \\ \hline
	\hline
	$1$    & $1Rs_1$ & \sbr$Rs_3$ & & $1Cs_2$ \\ \hline
	\sbr &         & $1Ls_2$      & &         \\ \hline
\end{tabular}
　　　この一覧表を $\delta$ という. 
\index{aaa@$\delta$}
\index{いちらんひょう@一覧表, $\delta$}

\bigskip

この一覧表の見方であるが, 
テープの指し示しているテープ記号が $1$ で ヘッドの状態が $s_1$ 
のときは一覧表の縦の欄の $1$ と横の欄の $s_1$ のところを見れば, 
\sbr$Rs_3$ であるから, テープ記号を \br にして, 
$R$ なのでヘッドを右に動かし($L$ は左で $C$ は動かないことを表す)
, ヘッドの状態を $s_3$ に変更せよ, 
という意味になる. 

\vspace*{0.5cm}

つまり　　
\Turing{2}{s_1}{{\cdots}1s}
　　
は
　　
\Turing{3}{s_3}{{\cdots}ss}
　　
と変更される. 

\vspace*{-1.5cm}

このような変更を次々と連続して行なうことにより, チューリング機械
は計算を行なう. 
一覧表はすべて書かれている必要はない. 

\begin{problem}
次のチューリング機械を計算せよ. 
\end{problem}

\Turing{1}{s_0}{s11111s}
\begin{tabular}{l}
$H=\{s_3\}$ \\
\begin{tabular}{|c||c|c|c|c|}
\hline
   & $s_0$ & $s_1$ & $s_2$ & $s_3$ \\ \hline
\hline
$1$  & $1Rs_1$    & $1Rs_1$    & \sbr$Ls_2$ & \\ \hline
\sbr & \sbr$Rs_0$ & \sbr$Ls_2$ & \sbr$Cs_3$ & \\ \hline
\end{tabular} \\
\end{tabular} 

\bigskip

これを計算すると, テープ上のすべての $1$ は消されヘッドが１番左に来て
止まる. 
確かめよ. 

\begin{problem}
ハノイの塔という問題がある. 
これは３本の棒と大きさの異なる任意の枚数の真ん中に
穴があいた円盤で行なうものである. 
まず初めに１本の棒に大きな順に下から円盤が差し込んである. 
これを自分より小さな円盤が下に来ることなく１枚ずつ動かし, 
他の棒にすべて下から大きな円盤順に並び換えよ, というものである. 
ハノイの塔はいかなる枚数の円盤でも解けるか？
\end{problem}

{\unitlength 0.75mm
\begin{picture}(70,25)
\put(0,0){\line(1,0){60}}

\put(9.5,16){\line(0,1){4}}
\put(10.5,16){\line(0,1){4}}
\put(9.5,20){\line(1,0){1}}

\put(29.5,0){\line(0,1){20}}
\put(30.5,0){\line(0,1){20}}
\put(29.5,20){\line(1,0){1}}

\put(49.5,0){\line(0,1){20}}
\put(50.5,0){\line(0,1){20}}
\put(49.5,20){\line(1,0){1}}

\multiput(0,2)(1,2){8}{\line(1,0){5}}
\multiput(0,2)(1,2){8}{\line(0,-1){2}}
\multiput(20,2)(-1,2){8}{\line(-1,0){5}}
\multiput(20,2)(-1,2){8}{\line(0,-1){2}}
\multiput(5,2)(0,2){5}{\line(1,0){10}}

\put(65,8){\line(1,0){7}}
\put(65,8){\line(0,1){4}}
\put(65,12){\line(1,0){7}}
\put(74,10){\line(-1,1){5}}
\put(74,10){\line(-1,-1){5}}

\put(80,0){\line(1,0){60}}

\put(89.5,0){\line(0,1){20}}
\put(90.5,0){\line(0,1){20}}
\put(89.5,20){\line(1,0){1}}


\put(109.5,16){\line(0,1){4}}
\put(110.5,16){\line(0,1){4}}
\put(109.5,20){\line(1,0){1}}

\put(129.5,0){\line(0,1){20}}
\put(130.5,0){\line(0,1){20}}
\put(129.5,20){\line(1,0){1}}

\multiput(100,2)(1,2){8}{\line(1,0){5}}
\multiput(100,2)(1,2){8}{\line(0,-1){2}}
\multiput(120,2)(-1,2){8}{\line(-1,0){5}}
\multiput(120,2)(-1,2){8}{\line(0,-1){2}}
\multiput(105,2)(0,2){5}{\line(1,0){10}}
\end{picture}
}

まず１枚なら(明らかに)ハノイの塔は解ける. 

次に $(n-1)$ 枚でハノイの塔が解けたと仮定する. 
すると $n$ 枚の場合は, 仮定よりまず上の $(n-1)$ 枚の円盤を目的とする
棒以外の棒に下から大きい順に積み上げることが可能である. 

{\unitlength 0.75mm
\begin{picture}(70,25)
\put(0,0){\line(1,0){60}}

\put(9.5,16){\line(0,1){4}}
\put(10.5,16){\line(0,1){4}}
\put(9.5,20){\line(1,0){1}}

\put(29.5,0){\line(0,1){20}}
\put(30.5,0){\line(0,1){20}}
\put(29.5,20){\line(1,0){1}}

\put(49.5,0){\line(0,1){20}}
\put(50.5,0){\line(0,1){20}}
\put(49.5,20){\line(1,0){1}}

\multiput(0,2)(1,2){8}{\line(1,0){5}}
\multiput(0,2)(1,2){8}{\line(0,-1){2}}
\multiput(20,2)(-1,2){8}{\line(-1,0){5}}
\multiput(20,2)(-1,2){8}{\line(0,-1){2}}
\multiput(5,2)(0,2){5}{\line(1,0){10}}

\put(65,8){\line(1,0){7}}
\put(65,8){\line(0,1){4}}
\put(65,12){\line(1,0){7}}
\put(74,10){\line(-1,1){5}}
\put(74,10){\line(-1,-1){5}}

\put(80,0){\line(1,0){60}}

\put(89.5,2){\line(0,1){18}}
\put(90.5,2){\line(0,1){18}}
\put(89.5,20){\line(1,0){1}}


\put(109.5,0){\line(0,1){20}}
\put(110.5,0){\line(0,1){20}}
\put(109.5,20){\line(1,0){1}}

\put(129.5,14){\line(0,1){6}}
\put(130.5,14){\line(0,1){6}}
\put(129.5,20){\line(1,0){1}}

\multiput(80,2)(1,2){1}{\line(1,0){5}}
\multiput(80,2)(1,2){1}{\line(0,-1){2}}
\multiput(100,2)(-1,2){1}{\line(-1,0){5}}
\multiput(100,2)(-1,2){1}{\line(0,-1){2}}
\multiput(85,2)(0,2){1}{\line(1,0){10}}

\multiput(121,2)(1,2){7}{\line(1,0){5}}
\multiput(121,2)(1,2){7}{\line(0,-1){2}}
\multiput(139,2)(-1,2){7}{\line(-1,0){5}}
\multiput(139,2)(-1,2){7}{\line(0,-1){2}}
\multiput(125,2)(0,2){4}{\line(1,0){10}}
\end{picture}
}

\begin{problem}
$h(n)=\underbrace{(2n+1) + (2n-1) + \cdots + 3 + 1}_{n+1}$ を
再帰的に定義せよ. 
\end{problem}

$h(0)=1$ で $\overl{h(n)=(2n+1) + h}(n-1)$ とすれば定義できる. 

\medskip

しかし $1+3+5+7+\cdots$ というように次々と奇数を足した
ものの合計は, 次のように面積で考えればよいことが昔から知られている. 
ちなみに数字はその囲まれた部分の面積である. 

\bigskip

{
\unitlength 1mm
\begin{picture}(100,50)(-25,0)
{\linethickness{0.5mm}
\put(0,0){\line(1,0){50}}
\put(0,0){\line(0,1){50}}
\put(50,50){\line(-1,0){50}}
\put(50,50){\line(0,-1){50}}

\multiput(50,40)(-10,0){5}{\line(0,1){10}}
\multiput(50,30)(-10,0){4}{\line(0,1){10}}
\multiput(50,20)(-10,0){3}{\line(0,1){10}}
\multiput(50,10)(-10,0){2}{\line(0,1){10}}
\multiput(50,0)(-10,0){1}{\line(0,1){10}}


\multiput(0,0)(0,10){5}{\line(1,0){10}}
\multiput(10,0)(0,10){4}{\line(1,0){10}}
\multiput(20,0)(0,10){3}{\line(1,0){10}}
\multiput(30,0)(0,10){2}{\line(1,0){10}}
\multiput(40,0)(0,10){1}{\line(1,0){10}}
}
\multiput(10,0.5)(10,0){5}{
\multiput(0,0)(0,2){25}{\line(0,1){1}}}

\multiput(0.5,10)(0,10){5}{
\multiput(0,0)(2,0){25}{\line(1,0){1}}}

\put(2,42){\makebox(5,5){1}}
\put(12,32){\makebox(5,5){3}}
\put(22,22){\makebox(5,5){5}}
\put(32,12){\makebox(5,5){7}}
\put(42,2){\makebox(5,5){9}}
\end{picture}}

\medskip

となって奇数の面積を次々と足して行ったものは正方形になるので, 
$h(n)=(n+1)^2$ という簡単な関数となり, 
何もわざわざ 
$$\overl{h(n)=(2n+1) + h}(n-1)$$
などと再帰的な定義を用いる必要はないのである. 


\begin{problem}
$F$ を任意のコンビネータ項とすると 
$$
\Y_F \equiv \Big(\S(\K\;F)(\S\;\I\;\I)
\big( \S(\K\;F)(\S\;\I\;\I)\big)\Big)
$$
を変換せよ. 
\end{problem}

先ほどの問題を使えば 
$\big(\S(\K\;F)(\S\;\I\;\I)a\big) \tr \Big(F \big(a\;a\big)\Big)$ 
なので
$$
\begin{array}{rclcl}
\Y_F & \equiv & 
\Big(\underline{\S(\K\;F)(\S\;\I\;\I)\big( \S(\K\;F)(\S\;\I\;\I)\big)}\Big)\\
& \tr & 
\bigg(F\Big(\big(\S(\K\;F)(\S\;\I\;\I)\big)
\big( \S(\K\;F)(\S\;\I\;\I)\big)\Big)\bigg)
& \equiv & (F\;\Y_F)
\end{array}
$$
となる. 

\begin{problem}
$H$ と $N$ の定義を思い出せ. 
\end{problem}
$$H=\bigg\{N'\in Power(\omega')\;\Big|\;(0\in N')\And
\forall x \in N'\Big(f(x)\in N'\Big)\bigg\}$$
であり
$$N=\Big\{y \in \bigcup H\;\big|\;\forall x \in H(y \in x)\Big\}$$
である. 

\bigskip

{\gt 置換公理(axiom of replacement)}というのは次のような
\index{ちかんこうり@置換公理}
公理図式(というのを覚えているか)で表される. 
$A(x,y)$ を集合の論理式とする. 
\begin{eqnarray*}
& & \forall\; x\;y\;z\bigg(A(x,y)\And A(x,z)\Imp(y=z)\bigg)\\
& & 　　　　　　\Imp\forall\; a \;\exists\; b\;
\forall\; y\bigg( y\in b \Iff \exists\; x \in a A(x,y)\bigg)
\end{eqnarray*}

この公理はずいぶんややこしい形をしていてわかりにくいが, 
要するに公理の前半部分の条件を満たした
論理式 $A(x,y)$ と集合 $a$ から $b$ という集合が構成できるという
ものである. 
$$
\omega\cdot\omega=\lim_{n\in\omega}\;(n\cdot\omega)=\left\{
\begin{array}{ccccc}
0,&1,&2,&\ldots \\
\omega,&\omega +1,&\omega+2,&\ldots \\
2\cdot\omega,&2\cdot\omega+1,&2\cdot\omega+2,&\ldots \\
3\cdot\omega,&3\cdot\omega+1,&3\cdot\omega+2,&\ldots \\
\vdots & \vdots & \vdots & \vdots
\end{array}
\right\}
$$
これを $\omega^2$ とし, さらに続けて $\omega^3, \omega^4, \ldots$ も
考えることができ, 
$$
\omega^{\omega}=\lim_{n\in\omega}(\omega^n)
$$
も考えることができる. 
$A$ が 公理であるとき, 
$$\overline{A}$$
と書く. 
各論理記号の導入規則と除去規則は以下のようである. 
\medskip
$$
(\Or I)
\infer{A}{A \Or B}
　　
(\Or I)
\infer{B}{A \Or B}
　　
(\Or E)\infer{
{　\atop { \atop \iatop{　}{A \Or B}}}\;\;\;\;
\iatop{[A]}{\iatop{\SIGMA}{C}}\;\;\;\;
\iatop{[B]}{\iatop{\PI}{C}}
}{C}
$$
\medskip
$$
(\exists I)\infer{A(a)}{\exists\;x\;A(x)}
　　　
(\exists E)\infer{
\iatop{　}{\iatop{　}{\exists\;x\;A(x)}}\;\;\;\;\;\;
\iatop{[A(x)]}{\iatop{\SIGMA}{C}}
}{C}(*x)
$$
\bigskip
ただし $a$ は任意の項であり, $(*x)$ は $x$ が固有変数であることを
示している. 

\medskip

ここまでの推論規則だけでできる証明図の体系を{\bf NJ}という. 
\begin{problem}
$\Not A \Imp B$ を仮定して $\Not B \Imp A$ を NK で証明せよ. 
\end{problem}

$\Not A \Imp B$ と $\Not B \Imp A$ との関係とか, 
$\Not B \Imp \Not A$ と $A \Imp B$ との関係は, \mbox{\gt 対偶}といって
片方が正しいともう片方も正しいということはすでにこの本でも使っている. 
しかしながらその証明には NK のように排中律が必要なのである. 
一気に証明を書く. 
$$
(\Or E)\infer{
\iatop{　}{\iatop{　}{
\overline{A \Or \Not A}\;\;\;\;
[A]\;\;\;\;}}
\infer{
\infer{\Not A \Imp B\;\;\;\;[\Not A]}{B}
\;\;\;\;\iatop{　}{[\Not B]}
}
{(\bot E)\infer{\bot}{A}}
}{
(\Imp I)\infer{A}{\Not B\Imp A}}
$$
ここは, じっくりと読んで欲しい. 

\medskip

\begin{problem}
$$
\iatop{\iatop{B}{\SIGMA}}{A\Imp \Not A}
　と　
\iatop{\PI_1}{B}
　と　
\iatop{\PI_2}{C}　
という証明図があるとする. 
$$
次の証明図を標準形を作る変換方法に従い, できるだけ簡単にせよ. 
\end{problem}
$$
\kern-5mm3 \infer{
\iatop{
\iatop{\iatop{4}{[B]}}{\SIGMA}}
{\infer{A\Imp\Not A}{\Not(A\Or B)\Or(A\Imp \Not A)}}
\infer{
\iatop{3}{[\Not(A\Or B)]}\;\;
\infer{\iatop{1}{[A]}}{A\Or B}
}{1 \infer{\bot}{\Not A}}\;\;
\infer{
\infer{
\iatop{3}{[A\Imp \Not A]}\;
\infer{
\iatop{3}{[A\Imp \Not A]}\;\;
\iatop{2}{[A]}
}{\Not A}
}{
\infer{(A\Imp \Not A)\And \Not A}{\Not A}\;\;\;\;
\iatop{2}{[A]}
}
}{
2 \infer{\bot}{\Not A}}
}{
\infer{
\infer{
4 \infer{
(ない仮定を落とす)\infer{\Not A}{C\Imp \Not A}
}{B\Imp (C\Imp\Not A)}\;\;\;\;\;\;
\iatop{\PI_1}{B}
}{C \Imp \Not A}\;\;\;\;\;\;
\iatop{\PI_2}{C}
}{\Not A}
}
$$

目を皿のようにして見よ. 
さて($\Or I$)と($\Or E$)が縦に並んだところがあるのに気がつく
(別のところのに気がつく人もいるかもしれないが, その人はそこから
やってみよ). 
そこを変換すると, 
$$
\iatop{
\underline{
\infer{
\iatop{\iatop{\iatop{4}{[B]}}{\SIGMA}}{A\Imp \Not A}\;
\infer{
\iatop{\iatop{\iatop{4}{[B]}}{\SIGMA}}{A\Imp \Not A}\;\;
\iatop{2}{[A]}
}{\Not A}
}{
\infer{(A\Imp \Not A)\And \Not A}{\Not A}\;\;\;\;
\iatop{2}{[A]}
}}}{
\infer{
\infer{
4 \infer{
(ない仮定を落とす)\infer{2 \infer{\bot}{\Not A}}{C\Imp \Not A}
}{B\Imp (C\Imp\Not A)}\;\;\;\;\;\;
\iatop{\PI_1}{B}
}{C \Imp \Not A}\;\;\;\;\;\;
\iatop{\PI_2}{C}
}{\Not A}}
$$
となる. 
\begin{problem}
$\Not\Not A \Imp A$ を LK で証明せよ. 
\end{problem}
$$
\begin{array}{rcl}
A & \IMP & A \\
\hline
 & \IMP & A,\;\Not A \\
\hline
\Not \Not A & \IMP & A \\
\hline
 & \IMP & \Not\Not A \Imp A \\
\end{array}
$$
で, これもシーケントの右側を２つ使うことを使っている. 

\end{document}