§E16.10一階論理の証明体系

証明. 最初に、この証明の内部だけで用いる仮定除去変換を証明する。H1–H3 と modus ponens だけからなる有限導出で$\Lambda\cup\{A\}\vdash_0 B$なら、$\Lambda\vdash_0 A\to B$である。実際、導出の各行$\delta$に対して$A\to\delta$を作る。$\delta=A$の場合は、H1 の二つの例

と、H2 で$\beta=A\to A$、$\gamma=A$とした例へ modus ponens を二回適用し、$A\to A$を得る。$\delta$が H1–H3 の例または$\Lambda$の元なら、$\delta$と H1 の例$\delta\to(A\to\delta)$から$A\to\delta$を得る。$\delta$が$\eta\to\delta$と$\eta$への modus ponens から得られたなら、帰納法で得た$A\to(\eta\to\delta)$と$A\to\eta$を H2 で結ぶ。この三場合で変換は閉じる。以下で一時的な仮定を外すときは、この有限変換だけを用いる。

(1)の恒等式は今の構成で得た。弱化は$\beta$と H1 の例$\beta\to(\alpha\to\beta)$への modus ponens である。共通前件の規則は H2 へ modus ponens を二回適用して得る。含意の推移では、$\beta\to\gamma$を弱化して$\alpha\to(\beta\to\gamma)$とし、共通前件の規則を適用する。

連言以下の導出に用いる四つの補助図式を作る。まず

は、一時的な仮定$A,A\to B$への modus ponens の後に仮定除去変換を二回適用して得る。$\vartheta=A\to(A\to A)$と置くと$\vartheta$は H1 の例である。H3 の二つの例

を(1)の含意の推移で結び、H1 の例$\neg\neg A\to(\neg\neg\vartheta\to\neg\neg A)$ともう一度結ぶと$\neg\neg A\to(\vartheta\to A)$を得る。(A) と定理$\vartheta$から$(\vartheta\to A)\to A$を得て、推移を用いると

となる。(B) で$A$を$\neg A$に置き換え、H3 の例

へ modus ponens を適用すると

を得る。H1 の例$\neg A\to(\neg B\to\neg A)$と H3 の例$(\neg B\to\neg A)\to(A\to B)$を推移で結ぶと

を得る。次に$A\to B$を一時的に仮定する。(B)、この仮定、(C1) を推移で結んで$\neg\neg A\to\neg\neg B$を得る。H3 の例

へ modus ponens を適用し、仮定除去変換を用いると

となる。また、(A) を$B=C$とした式と、(C3) を$A=A\to C$、$B=C$とした式を推移で結ぶと

を得る。最後に$U=A\to C$と$V=\neg A\to C$を一時的に仮定する。$\neg C$をさらに仮定すると、(C3) と$V$から$\neg\neg A$、(B) から$A$を得る。(C3') と$A$から$\neg C\to\neg U$を得て、仮定$\neg C$への modus ponens により$\neg U$となる。仮定$\neg C$だけを外すと$\neg C\to\neg U$である。H3 の例$(\neg C\to\neg U)\to(U\to C)$から$U\to C$を得て、仮定$U$への modus ponens で$C$となる。$V$、次に$U$を外すと

を得る。

(2)を示す。$K:=\alpha\land\beta=\neg(\alpha\to\neg\beta)$と置く。$K,\neg\alpha$を仮定すると、(C2) から$\alpha\to\neg\beta$を得て、(C2) を$A=\alpha\to\neg\beta$、$B=\alpha$として$K$と結べば$\alpha$を得る。したがって$K$の下で$\neg\alpha\to\alpha$であり、恒等式$\alpha\to\alpha$と (C4) から$\alpha$を得る。仮定$K$を外すと$K\to\alpha$である。

次に$K,\alpha,\neg\beta$を仮定する。H1 から$\alpha\to\neg\beta$を得て、直前と同じく$K$から (C2) を用いると$\beta$を得る。仮定$\neg\beta$を外し、恒等式$\beta\to\beta$と (C4) を用いると、$K,\alpha$から$\beta$を得る。また$K,\neg\alpha$からは、上で得た$\alpha$と、$K,\alpha$からの同じ有限導出を続けて$\beta$を得る。二つを仮定除去変換で含意にし、(C4) を適用すると$K$から$\beta$を得る。よって$K\to\beta$である。

連言の導入では、$\alpha,\beta$を仮定する。(C1) から$\neg\neg\beta$を得る。(A) を$A=\alpha$、$B=\neg\beta$とした式と、(C3) を$A=\alpha\to\neg\beta$、$B=\neg\beta$とした式を推移で結ぶと$\alpha\to(\neg\neg\beta\to\neg(\alpha\to\neg\beta))$を得る。二回の modus ponens の後に二つの仮定を外せば$\alpha\to(\beta\to\alpha\land\beta)$となる。

(3)は、$\alpha\leftrightarrow\beta$が$(\alpha\to\beta)\land(\beta\to\alpha)$の略記であることと、(2)の二つの射影および導入を、それぞれ$\alpha\to\beta$と$\beta\to\alpha$へ適用して得る。

(4)の否定の場合には、$\alpha\leftrightarrow\beta$を仮定する。(3)の二つの射影と (C3) から$\neg\alpha\to\neg\beta$と$\neg\beta\to\neg\alpha$を得て、(3)の導入で$\neg\alpha\leftrightarrow\neg\beta$にまとめる。仮定を外せば表示した図式を得る。

含意の場合には$\alpha\leftrightarrow\alpha'$と$\beta\leftrightarrow\beta'$を仮定する。(3)から四方向の含意を取り出す。さらに$\alpha\to\beta$を仮定し、$\alpha'\to\alpha$、$\alpha\to\beta$、$\beta\to\beta'$を(1)の推移で結ぶ。追加した仮定を外すと$(\alpha\to\beta)\to(\alpha'\to\beta')$となる。逆に$\alpha'\to\beta'$を仮定し、$\alpha\to\alpha'$、$\alpha'\to\beta'$、$\beta'\to\beta$を結んで仮定を外すと、逆向きの含意を得る。(3)で双条件にまとめ、最初の二つの仮定を外すと表示した含意の合同図式を得る。

(5)では$\alpha,\neg\alpha$を仮定する。(C2) を二回用いて$\rho$と$\neg\rho$を得て、(2)の連言導入から$\bot_\rho$を得る。二つの仮定を外すと(5)の最初の式になる。$\bot_\rho$を仮定した場合には、(2)の射影から$\rho$と$\neg\rho$を得る。(C2) と二回の modus ponens により$\alpha$を得て仮定を外せば$\bot_\rho\to\alpha$となり、$\alpha$を$\neg\alpha$に置き換えれば最後の式も得る。

すべての仮定除去は冒頭の有限変換であり、量化公理、一般化規則、および完全性定理を用いていない。▨

証明. Q1 の二つの例

と補題 2.1 (1)にある弱化、共通前件の modus ponens、および含意の推移から

を得る。$C:=\forall x(\alpha\to\beta)$、$D:=\forall x\alpha$と置くと、この定理は$\vdash C\to(D\to\beta)$である。定理全体を$x$で一般化して$\vdash\forall x(C\to(D\to\beta))$を得る。$x\notin FV(C)$なので、Q2 と modus ponens により$\vdash C\to\forall x(D\to\beta)$である。また$x\notin FV(D)$なので、Q2 の例

は公理である。補題 2.1 (1)で二つの含意を合成すると

を得る。▨

証明. 最初に、α 同値の生成元である一つの安全な束縛変数改名を扱う。$z\notin FV(\eta)$とし、$\forall x\eta$の$x$に束縛された出現を$z$へ安全に改名して$\forall z\eta'$を得たとする。安全性の条件により、raw な通常代入として

が成り立ち、いずれの代入も捕獲を起こさない。Q1 から

を得る。この定理全体を$z$で一般化する。$z\notin FV(\forall x\eta)$なので、Q2 と modus ponens によって

を得る。改名後には$x\notin FV(\eta')$であり、$x$は$\eta'$の自由な$z$に代入可能である。したがって、Q1 から$\vdash\forall z\eta'\to\eta$を得て、この定理全体を$x$で一般化し、 Q2 を適用すると

となる。補題 2.1 (3)で二方向をまとめれば、$\vdash\forall x\eta\leftrightarrow\forall z\eta'$である。

次に、この導出が α 同値を生成する同値閉包と合同閉包を保つことを示す。反射性は$\vdash\alpha\to\alpha$の二つのコピーを補題 2.1 (3)でまとめて得る。対称性と推移性は、双条件から二方向の含意を取り出し、補題 2.1 (1)で含意を合成してから、補題 2.1 (3)で再び双条件にまとめて得る。否定と含意に関する合同性は、補題 2.1 (4)そのものである。

全称量化子に関して$\vdash\alpha\leftrightarrow\beta$とする。補題 2.1 (3)から$\vdash\alpha\to\beta$と$\vdash\beta\to\alpha$を得る。それぞれを$x$で一般化し、補題 2.2を適用すると

となるので、補題 2.1 (3)によって$\vdash\forall x\alpha\leftrightarrow\forall x\beta$を得る。以上を、α 同値を生成する安全な一段改名、同値関係の三規則、および原始構成子の合同規則からなる生成列に関して帰納的に適用すれば、任意の α 同値な raw 論理式について結論が従う。▨

証明. 等号の関係合同公理で、原子式$z_1=z_2$の組$(t,t)$と$(u,t)$を比較すると、

を得る。$\vdash t=t$と補題 2.1 (2)および補題 2.1 (3)を用い、連言の導入と双条件の射影を展開すると$\vdash t=u\to u=t$が従う。

次に、原子式$z_1=z_2$の組$(t,u)$と$(t,v)$を比較すると、

を得る。$\vdash t=t$と補題 2.1 (2)および補題 2.1 (3)を用い、前提$t=u\land u=v$から$u=v$と$t=u$を取り出すと$t=v$を得る。基本派生則の証明冒頭にある仮定除去変換で前提を含意の左辺へ移すことができるため、表示した定理を得る。▨

証明.$\varphi$の高さに関する帰納法を用いる。最初に、任意の項$r(z_1,\ldots,z_n)$について

となることを項の構造に関する帰納法で示す。$r=z_i$の場合は、補題 2.1 (2)を繰り返して$E$から第$i$の連言肢$t_i=u_i$を取り出す。$r$が表示された変数以外の変数または定数なら、反射律と H1 を用いる。$r=f(r_1,\ldots,r_k)$の場合は、帰納法の仮定から得た$k$個の等式を$E$の下で補題 2.1 (1)にある共通前件の規則と補題 2.1 (2)の連言導入を繰り返し、連言にまとめてから$k$項関数記号$f$の合同公理を適用する。$k=0$では、結論は反射律そのものである。

原子式が等号$r=q$の場合は、項について得た二つの等式と、等号を二項関係として扱う合同公理を用いる。原子式が$R(r_1,\ldots,r_k)$の場合も、項について得た$k$個の等式を補題 2.1 (1)と補題 2.1 (2)によって$E$の下で連言にまとめ、$R$の合同公理を用いる。$k=0$では空の連言を前件とする零項関係の合同公理が同じ原子式どうしの双条件を与える。

$\varphi=\neg\psi$の場合は、帰納法の仮定$E\to(\psi(\bar t)\leftrightarrow\psi(\bar u))$と補題 2.1 (4)にある否定の合同図式を、補題 2.1 (1)の含意の推移で結ぶ。$\varphi=\psi\to\chi$の場合は、二つの帰納法の仮定と補題 2.1 (4)にある含意の二引数の合同図式へ、補題 2.1 (1)の共通前件の modus ponens を二回適用する。

$\varphi=\forall y\psi$の場合を考える。$w$を$\psi$、$E$、および代入するすべての項のいずれにも現れない新しい変数とし、束縛変数を安全に改名して

とする。改名は論理式の高さを変えないので、$\chi$には帰納法の仮定を適用することができる。$\chi(\bar t)$と$\chi(\bar u)$を、$\chi$への捕獲回避同時代入の raw な代表として選ぶ。帰納法の仮定と補題 2.1 (3)の二つの射影から、定理

と逆向きの定理をそれぞれ得る。最初の定理全体を$w$で一般化し、$w\notin FV(E)$を用いて Q2 を適用すると

となる。補題 2.2と補題 2.1 (1)を用いると

を得る。同じ議論を逆向きにも行う。補題 2.1 (3)にある双条件の導入図式へ、補題 2.1 (1)の共通前件の modus ponens を二回適用すると

を得る。§E16.7 定理 2.2により捕獲回避代入は α 同値類上で定まるので、元の raw 論理式$\forall y\psi$への二つの代入結果をそれぞれ$L_t,L_u$と書けば、

である。$A:=\forall w\chi(\bar t)$、$B:=\forall w\chi(\bar u)$と置く。補題 3.1と補題 2.1 (3)の射影から、

を得る。一時的に$E$を仮定する。直前に得た$\vdash E\to(A\to B)$へ modus ponens を適用して$A\to B$を得る。これを$L_t\to A$および$B\to L_u$と補題 2.1 (1)の含意の推移で合成すると$L_t\to L_u$となる。基本派生則の証明冒頭にある仮定除去変換で$E$を外せば$\vdash E\to(L_t\to L_u)$である。逆向きの$\vdash E\to(B\to A)$と残る二つの射影を用いると、同様に$\vdash E\to(L_u\to L_t)$を得る。最後に、補題 2.1 (3)にある双条件の導入図式へ補題 2.1 (1)の共通前件の modus ponens を二回適用すると

となる。この式は、元の raw な代表について求める結論である。以上で原始構成子のすべての場合を処理した。▨

証明. まず左から右を示す。$\Gamma\cup\{\theta\}$からの導出の長さに関する帰納法を用い、各行$(\chi,\Delta)$について$\Gamma\vdash\theta\to\chi$を構成する。行$\chi$が$\Gamma$の要素または公理なら、$\Gamma\vdash\chi$であり、補題 2.1 (1)にある弱化から$\Gamma\vdash\theta\to\chi$を得る。行が$\theta$自身なら、補題 2.1 (1)から$\Gamma\vdash\theta\to\theta$を得る。

$\chi$が$\eta\to\chi$と$\eta$への modus ponens から得られたとする。帰納法の仮定は$\Gamma\vdash\theta\to(\eta\to\chi)$と$\Gamma\vdash\theta\to\eta$を与える。H2 へ modus ponens を二回適用すると$\Gamma\vdash\theta\to\chi$を得る。

$\chi=\forall x\eta$が$(\eta,\Delta)$の一般化から得られたとする。$\theta\in\Delta$なら、一般化規則の条件から$x\notin FV(\theta)$である。帰納法の仮定$\Gamma\vdash\theta\to\eta$を一般化して$\Gamma\vdash\forall x(\theta\to\eta)$を得る。この一般化は、もとの$\Delta$から$\theta$を除いた前提だけに依存し、$x$は各前提に自由に現れないため適法である。Q2 により$\Gamma\vdash\theta\to\forall x\eta$を得る。

$\theta\notin\Delta$なら、$(\forall x\eta,\Delta)$までの実依存部分は$\Gamma$だけからの導出である。したがって$\Gamma\vdash\forall x\eta$であり、H1 から$\Gamma\vdash\theta\to\forall x\eta$を得る。

逆に$\Gamma\vdash\theta\to\varphi$とする。依存前提集合を保った同じ導出は$\Gamma\cup\{\theta\}$からの導出でもある。$\Gamma\cup\{\theta\}$では$\theta$が前提なので、 modus ponens により$\Gamma\cup\{\theta\}\vdash\varphi$を得る。▨

証明.$\Gamma$からの一つの導出を固定する。導出は有限列なので、その行として現れる$\Gamma$の要素も有限個である。導出に現れた前提の集合を$\Gamma_0$とする。同じ有限列の一般化条件は、より小さい前提集合$\Gamma_0$に対しても成立するので、同じ列が$\Gamma_0$からの導出になる。▨

証明. 導出の長さに関する帰納法を用い、各行$(\chi,\Delta)$について$M,s\models\Delta$なら$M,s\models\chi$となることを示す。前提の行は依存前提集合がその前提だけからなるので真である。H1 と H2 は含意の真理値規則を直接適用すると真である。H3 が偽なら、その前件$\neg\beta\to\neg\alpha$が真、$\alpha$が真、$\beta$が偽となるが、後二条件は前件を偽にするので矛盾する。

Q1 を考える。$M,s\models\forall x\varphi$なら、$a=\llbracket t\rrbracket_s^M$に対して$M,s[x\mapsto a]\models\varphi$である。$t$が$x$に自由に代入可能であるため、§E16.7 系 5.3から$M,s\models\varphi[x:=t]$を得る。したがって Q1 は妥当である。

Q2 を考える。$M,s\models\forall x(\varphi\to\psi)$かつ$M,s\models\varphi$とする。$x\notin FV(\varphi)$なので、§E16.6 定理 4.1により、任意の$a\in|M|$について$M,s[x\mapsto a]\models\varphi$である。Q2 の前件から同じ割当てで$M,s[x\mapsto a]\models\varphi\to\psi$であるから、$M,s[x\mapsto a]\models\psi$を得る。$a$は任意なので$M,s\models\forall x\psi$であり、Q2 は妥当である。

等号の反射公理は、等号が同一性として解釈されるため真である。関数合同公理では、各$\llbracket t_i\rrbracket_s^M=\llbracket u_i\rrbracket_s^M$なら、関数$f^M$を同じ引数列へ適用した値が一致する。関係合同公理では、同じ引数列が関係$R^M$に属するかどうかは一致する。$n=0$の場合は比較する引数が無く、同じ定数の値または同じ零項関係の真理値を比較するので妥当である。

modus ponens が真理を保存することは含意の意味から従う。$\chi$から$\forall x\chi$への一般化を考え、この行の依存前提集合を$\Delta$とする。$M,s\models\Delta$と仮定する。任意の$a\in|M|$について、一般化条件と§E16.6 定理 4.1により$M,s[x\mapsto a]\models\Delta$である。帰納法の仮定を割当て$s[x\mapsto a]$へ適用すると$M,s[x\mapsto a]\models\chi$を得る。したがって$M,s\models\forall x\chi$である。

導出の末尾の依存前提集合は$\Gamma$の部分集合である。$M,s\models\Gamma$を満たす任意の構造と割当てへ帰納法の結論を適用すると$M,s\models\varphi$を得る。したがって$\Gamma\models\varphi$である。▨

証明.$\bot$は$L$に属さない非論理記号を含まないので、以下の各行はすべて$\operatorname{Form}(L)$に属する。$\Gamma\vdash_L\chi$かつ$\Gamma\vdash_L\neg\chi$なら、補題 2.1 (5)を$\rho=\forall x_0\,x_0=x_0$として得る$\chi\to(\neg\chi\to\bot)$へ modus ponens を二回適用し、$\Gamma\vdash_L\bot$を得る。逆に$\Gamma\vdash_L\bot$なら、補題 2.1 (5)の$\bot\to\chi$と$\bot\to\neg\chi$へ modus ponens を適用して$\Gamma\vdash_L\chi$かつ$\Gamma\vdash_L\neg\chi$を得る。したがって二つの条件は同値である。▨

証明.$\Gamma\vdash_L\bot$なら、健全性により$\Gamma\models\bot$となる。しかし$\bot$はどの構造と割当てでも偽なので、$\Gamma$のモデルが存在することに反する。命題 7.2により$\Gamma$は$L$において構文的に無矛盾である。▨