数理論理学の基礎・命題論理
\(
\newcommand{\Pow}[1]{\mathcal{P}(#1)}
\newcommand{\nat}{\mathbb{N}}
\)
\(
\newcommand{\blank}{ {-} }
\)
命題論理
命題論理 (propositional logic) は数学に於ける命題 (proposition) を抽象化、あるいは記号化し、その命題と命題同士の関係性の記号化と言えるであろう論理結合子 (logical connectives) からなる論理である。
命題論理では論理式 $\varphi,\psi$ に対し以下の結合子を考える。
| 論理式 | 読み方 | 名称 |
|---|---|---|
| $\lnot \varphi$ | $\varphi$ ではない | 否定 (negation) |
| $\varphi \land \psi$ | $\varphi$ かつ $\psi$ | 連言 (conjunction) |
| $\varphi \lor \psi$ | $\varphi$ または $\psi$ | 選言 (disjunction) |
| $\varphi \to\psi$ | $\varphi$ ならば $\psi$ | 含意 (implication) |
また真偽を直接表す以下の記号も考える。
| 論理式 | 読み方 | 名称 |
|---|---|---|
| $\top$ | 真である | 真 (true) |
| $\bot$ | 偽である | 偽 (false) |
これらの記号を用いて命題論理の論理式 (logical formula, formula) は定義される。 注意しておくべきこととして論理式は単なる記号列でしかないということである。 まず記号列の中で「何が論理式であって、何が論理式でないのか」というのを定義する。 言語学において「何が文であって、何が文でないか」ということを扱う分野の用語として統語論 (syntax) あるいは構文論、統辞論という言葉がある。 数理論理学に於いても何が論理式で何が論理式でないか、ということを定めたり、あるいは記号列としての性質を言語学から用語を拝借し、命題論理の統語論という。 同じく、言語学に於いて文の意味に関する分野の用語として意味論 (semantics) があり、数理論理学に於いても言語学に倣い論理式の意味に関する分野として意味論という用語を用いる。こと命題論理の意味論としては 真理値 (truth value) というものを用いる。そして数学に於ける証明を形式化することによって形式的証明 (formal proof) を与える。形式的証明を与えることは統語論とも意味論とも捉えられることがある。
命題論理の統語論
定義 1 (命題論理の記号)
命題論理の記号 (symbol) は以下からなる。
- 命題変数 (propositional variable) $p,q,r,\ldots.$
- 命題定数 (propositional constant) $\top,\bot.$
- 論理結合子 (logical connectives) $\lnot,\land,\lor,\to.$
- 括弧 (brackets) $(,).$
以下 $p,q,r$ あるいはそれに添え字を付けたもので命題変数を表すものとする。
また命題変数の集合を $\mathrm{PropVar}$ と表す。$\mathrm{PropVar}$ の濃度は有限でも無限でもよいものとする。
定義 2 (命題論理の論理式)
命題論理の論理式 (logical formula, formula) は以下のように帰納的に定義される。
- $\mathrm{PropVar}$ の要素は論理式である。
- $\top$ と $\bot$ はともに論理式である。
- $\varphi,\psi$ が論理式であるとき、$(\varphi\land\psi),(\varphi\lor\psi),(\varphi\to\psi)$ は論理式である。
- $\varphi$ が論理式であるとき $(\lnot\varphi)$ は論理式である。
- 以上によって論理式と分かるもののみが論理式である[脚注 1]。
また命題論理の論理式の集合を $\mathrm{PropFml}$ とする。
例 3 (命題論理の論理式)
- $( (\lnot p)\land q),( (p\land q)\lor\bot),(p\to (q\to r)),(\lnot (\lnot p)),( ( (\lnot p)\to q)\land (q\lor\top)).$
定義 4 (命題論理に於ける論理式の省略記法)
さて上記の例を見れば分かる通り、このまま論理式を同じように表記すると括弧が多すぎて視認性を欠く。よって論理式の省略記法を定める。 まず論理結合子の結合順序は以下のようにする。
- $\lnot$ が一番強く、$\lor,\land$ がその次に強く、$\to$ が $\lor,\land$ の次に強いとする。つまり $\lnot \varphi \land\psi\to\chi$ は $( ( (\lnot\varphi)\land\psi)\to\chi) $を表す。
- $\land,\lor$ は左結合的であるとする。つまり $\varphi\land\psi\land\chi$ は $( (\varphi\land\psi)\land\chi)$ を、$\varphi\lor\psi\lor\chi$ は $( (\varphi\lor\psi)\lor\chi)$ を表すものとする。
- $\land,\lor$ に結合の強さは設けない。つまり $\varphi\lor\psi\land\chi$ とは書かず適宜 $(\varphi\lor\psi)\land\chi,\varphi\lor(\psi\land\chi)$ と書き分ける。
- $\to$ は右結合的であるとする。つまり $\varphi\to\psi\to\chi$ は $(\varphi\to(\psi\to\chi))$ を表すものとする。
- $\varphi\leftrightarrow\psi$ で $(\varphi\to\psi)\land(\psi\to\varphi)$ を表すこととする。また $\leftrightarrow$ の結合の強さは最弱であるとする。
命題論理の付値による意味論
以下では付値 (truth assignment) を用いた命題論理の意味論を与える。 付値は命題変数に対して $0,1$ の値を割り当てることによって定義される。 ここで $0$ は偽であることを表し、$1$ は真であることを表している。以下では順序数の定義に則り $2:=\{0,1\}$ とする。
定義 5 (付値)
関数 $\nu\colon\mathrm{PropVar}\to 2$ のことを付値 (valuation, truth assignment) という。
定義 6 (充足可能性関係)
論理式 $\varphi$ と付値 $\nu$ に対して充足関係 (satisfaction relation) 、$\nu\models\varphi$[脚注 2]を帰納的に定義する。
- $p\in\mathrm{PropVar}$ に対して $\nu\models p:\Leftrightarrow\nu(p)=1$ である。
- $\nu\models\top$ である。
- $\nu\models\bot$ ではない。
- $\nu\models\lnot\varphi$ であるのは $\nu\models\varphi$ ではないとき、またそれに限る。
- $\nu\models\varphi\land\psi$ であるのは、$\nu\models\varphi$ かつ $\nu\models\psi$ であるときであり、またそれに限る。
- $\nu\models\varphi\lor\psi$ であるのは、$\nu\models\varphi$ または $\nu\models\psi$ であるときであり、またそれに限る[脚注 3]。
- $\nu\models\varphi\to\psi$ であるのは、$\nu\models\varphi$ ではないか、または $\nu\models\psi$ であるときであり、またそれに限る。
また充足可能性に関する条件をいくつか定める。
- $\nu\models\varphi$ であるとき、$\nu$ は $\varphi$ を充足する (satisfy) という。
- ある付値 $\nu$ が存在して $\nu\models\varphi$ であるとき、論理式 $\varphi$ は充足可能 (satisfiable) であるという。
- 論理式の集合 $T$ を 公理系 (axiomatic system, axioms, axiomata) あるいは理論 (theory) という。
- 理論 $T$ と論理式 $\varphi$ に対して $T+\varphi$ で $T\cup\{\varphi\}$ を表す。
- 任意の $\varphi\in T$ に対し $\nu\models\varphi$ であるとき、$\nu$ は $T$ を充足するといい、$\nu\models T$ と表す。またこのとき $\nu$ を $T$ のモデル (model) という。
- ある付値 $\nu$ が存在して $\nu\models T$ であるとき、公理系 $T$ は充足可能であるという。
- 任意の付値 $\nu$ に対して $\nu\models\varphi$ であるとき、論理式 $\varphi$ は恒真 (logically valid, valid) であるという。
- 任意の付値 $\nu$ に対して、$\nu\models T$ ならば $\nu\models\varphi$ であるとき、$\varphi$ は $T$ の定理 (theorem) である、あるいは $\varphi$ は $T$ からの論理的帰結 (logical consequence) であるといい、$T\models\varphi$ と表す。また $T$ が空なとき単に論理的帰結であるといい $\models \varphi$ と表す。
- 理論 $T$ 論理式 $\varphi,\psi$ に対して $T\models\varphi\leftrightarrow\psi$ であるとき $\varphi,\psi$ は $T$ 上で論理的同値 (logically equivalent) または単に同値 (equivalent) であるという。また $T$ が空なとき単に論理的同値であるという。
与えられた論理式が充足可能であるか否かは以下の拡張された付値を用いることで計算することができる。また論理式に現れる命題変数は有限であることから、恒真であることも判定できる。
定義 7 (拡張された付値)
命題変数に対して定義された付値 $\nu$は以下のように論理式全体に拡張される。付値 $\nu$ に対して関数 $\overline{\nu}\colon\mathrm{PropFml}\to 2$ は以下のように帰納的に定義される。
- $p\in\mathrm{PropVar}$ に対して $\overline{\nu}(p):=\nu(p)$ である。
- $\overline{\nu}(\top):=1$ である。
- $\overline{\nu}(\bot):=0$ である。
- $\overline{\nu}(\lnot\varphi):=1-\overline{\nu}(\varphi)$ である。
- $\overline{\nu}(\varphi\land\psi):=\min\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ である。
- $\overline{\nu}(\varphi\lor\psi):=\max\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$である。
- $\overline{\nu}(\varphi\to\psi):=\max\{1-\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$である。
命題 8 (拡張された付値と充足可能性の同値性)
任意の論理式 $\varphi$ と付値 $\nu$ に対して $\nu\models\varphi$ であることの必要十分条件は $\overline{\nu}(\varphi)=1$ であることである。
Proof.
論理式の構成に関する帰納法で示す。$p\in\mathrm{PropVar},\bot,\top$ に対して同値であるのは定義より明らかである。
$\overline{\nu}(\varphi)=1$ と $\nu\models\varphi$ が同値であると仮定しよう。 定義から $\overline{\nu}(\lnot\varphi)=1-\overline{\nu}(\varphi)$ であり、$1-\overline{\nu}(\varphi)=1$ となるのは $\overline{\nu}(\varphi)=0$ であるときであり、またそれに限る。 帰納法の仮定から $\overline{\nu}(\varphi)=0$ であるのは、$\nu\models\varphi$ ではないとき、またそれに限り、この条件は $\nu\models\lnot\varphi$ と同値である。
$\overline{\nu}(\varphi)=1$ と $\nu\models\varphi$ が同値であり、$\overline{\nu}(\psi)=1$ と $\nu\models\psi$ が同値であるとしよう。 $\overline{\nu}(\varphi\land\psi)=\min\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ であり、$\min\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}=1$ が成り立つのは $\overline{\nu}(\varphi)=1$ かつ $\overline{\nu}(\psi)=1$ であるときであり、またそれに限るから、帰納法の仮定を適用すれば良い。
$\overline{\nu}(\varphi)=1$ と $\nu\models\varphi$ が同値であり、$\overline{\nu}(\psi)=1$ と $\nu\models\psi$ が同値であるとしよう。 $\overline{\nu}(\varphi\lor\psi)=\max\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ であり、$\max\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}=1$ が成り立つのは $\overline{\nu}(\varphi)=1$ または $\overline{\nu}(\psi)=1$ であるときであり、またそれに限るから、帰納法の仮定を適用すれば良い。
$\overline{\nu}(\varphi)=1$ と $\nu\models\varphi$ が同値であり、$\overline{\nu}(\psi)=1$ と $\nu\models\psi$ が同値であるとしよう。 $\overline{\nu}(\varphi\to\psi)=\max\{1-\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ であり、$\max\{1-\overline{\nu}(\varphi),\overline{\nu}(\psi)\}=1$ が成り立つのは $\overline{\nu}(\varphi)=0$ または $\overline{\nu}(\psi)=1$ であるときであり、またそれに限るから、帰納法の仮定を適用すれば良い。
□命題 9 (充足可能性と論理的帰結の関係)
$T\models\varphi$であるための必要十分条件は$T\cup\{\lnot\varphi\}$が充足不能であることである。
Proof.
$\nu\models T\cup\{\lnot\varphi\}$ であるためには、$\nu\models T$ かつ$ \nu\models \varphi$ でないことであることが必要十分であるため明らかである。
□例 10 (恒真な論理式の例)
恒真な例としては以下のようなものが考えられる。
- $\land,\lor$ に関する代数的性質。
- 結合律 (associative law) $( (\varphi\land\psi)\land\chi)\leftrightarrow(\varphi\land(\psi\land\chi))$ 及び $( (\varphi\lor\psi)\lor\chi)\leftrightarrow(\varphi\lor(\psi\lor\chi))$ 。
- 可換律 (commutative law) $(\varphi\land\psi)\leftrightarrow(\psi\land\varphi)$ 及び $(\varphi\lor\psi)\leftrightarrow(\psi\lor\varphi)$ 。
- 吸収律 (absorptive law) $(\varphi\land(\varphi\lor\psi))\leftrightarrow\varphi$ 及び $(\varphi\lor(\varphi\land\psi))\leftrightarrow\varphi$ 。
- 冪等律 (idempotent law) $(\varphi\land\varphi)\leftrightarrow\varphi$ 及び $(\varphi\lor\varphi)\leftrightarrow\varphi$ 。
- 分配律 (distributive law) $(\varphi\lor(\psi\land\chi))\leftrightarrow( (\varphi\lor\psi)\land(\varphi\lor\chi))$ 及び $(\varphi\land(\psi\lor\chi))\leftrightarrow((\varphi\land\psi)\lor(\varphi\land\chi))$ 。
- $\to$ に関する順序的性質。
- 反射律 (reflexive law) あるいは同一律 (identity law) $\varphi\to\varphi$ 。
- 比較可能性 (compatibility) 、Dummettの法則 (Dummett's law) あるいは前線形性 (prelinearlity) $(\varphi\to\psi)\lor(\psi\to\varphi)$ 。
- 推移律 (transitive law) あるいは三段論法 (syllogism) $(\varphi\to\psi)\land(\psi\to\chi)\to(\varphi\to\chi)$ 。
- 反対称性 (antisymmetric law) $((\varphi\to\psi)\land(\psi\to\varphi))\leftrightarrow(\varphi\leftrightarrow\psi)$ 。
- 有名な論理的性質。
- De Morganの法則 (De Morgan's law) $(\lnot(\varphi\land\psi))\leftrightarrow(\lnot\varphi\lor\lnot\psi)$ 及び $(\lnot(\varphi\lor\psi))\leftrightarrow(\lnot\varphi\land\lnot\psi)$ 。
- 対偶律 (law of contraposition) $(\varphi\to\psi)\leftrightarrow(\lnot\psi\to\lnot\varphi)$ 。
- 二重否定導入 (double negation introduction) と二重否定除去 (double negation elimination) $(\lnot\lnot\varphi)\leftrightarrow\varphi$ 。
- 排中律 (law of excluded middle, tertium non datur) $\varphi\lor\lnot\varphi$ 。
- Peirceの法則 (Pierce's law) $((\varphi\to \psi)\to\varphi)\to\varphi$ 。
- 無矛盾律 (law of non-contradiction) [脚注 4]$\lnot(\varphi\land\lnot\varphi)$ 。
- 前件肯定 (modus ponens) $\varphi\land(\varphi\to\psi)\to\psi$ 。
- 爆発律 (law of explosion, ex falso quodlibet) $\bot\to\varphi$ 。
- また以下のような随伴構造も知られている。
- 指数随伴 (exponential adjunction) $(\varphi\land\psi\to\chi)\leftrightarrow(\varphi\to\psi\to\chi)$ 。
- 特に名称はないが以下の $\to,\lor,\lnot$ の関係は重要である。
- $(\varphi\to\psi)\leftrightarrow(\lnot\varphi\lor\psi)$ 。
以下ではDe Morganの法則の片方が恒真であることを真理表 (truth table) を用いて確かめよう。
まず $\overline{\nu}(\varphi\leftrightarrow\psi)=1$ となるのは $\overline{\nu}(\varphi)=1$ かつ $\overline{\nu}(\psi)=1$ であるか、もしくは $\overline{\nu}(\varphi)=0$ かつ $\overline{\nu}(\psi)=0$ であることを確かめよう。 これを調べるためには $\overline{\nu}(\varphi)$ が $0,1$ どちらを取るか、$\overline{\nu}(\varphi)$ が $0,1$ どちらを取るかの $2\cdot 2=4$ 通りを考えれば良い。 まず $\varphi\leftrightarrow\psi$ は $(\varphi\to\psi)\land(\psi\to\varphi)$ のことであった。よって下の表の $\varphi,\psi$ に $4$ 通りの $0,1$ を書き込む。
| $(\varphi$ | $\to$ | $\psi)$ | $\land$ | $(\psi$ | $\to$ | $\varphi)$ |
|---|---|---|---|---|---|---|
| $1$ | $1$ | $1$ | $1$ | |||
| $1$ | $0$ | $0$ | $1$ | |||
| $0$ | $1$ | $1$ | $1$ | |||
| $0$ | $0$ | $0$ | $1$ |
次に $\overline{\nu}(\varphi\to\psi)=\max\{1-\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ と $\overline{\nu}(\psi\to\varphi)=\max\{1-\overline{\nu}(\psi),\overline{\nu}(\varphi)\}$ を計算して $\to$ の下に書き込むと、
| $(\varphi$ | $\to$ | $\psi)$ | $\land$ | $(\psi$ | $\to$ | $\varphi)$ |
|---|---|---|---|---|---|---|
| $1$ | $1$ | $1$ | $1$ | $1$ | $1$ | |
| $1$ | $0$ | $0$ | $0$ | $1$ | $1$ | |
| $0$ | $1$ | $1$ | $1$ | $1$ | $1$ | |
| $0$ | $1$ | $0$ | $0$ | $0$ | $1$ |
となる。$\overline{\nu}(\varphi\land\psi)=\min\{\overline{\nu}(\varphi),\overline{\nu}(\psi)\}$ であるから、計算し $\land$ の 下に書き込むと、
| $(\varphi$ | $\to$ | $\psi)$ | $\land$ | $(\psi$ | $\to$ | $\varphi)$ |
|---|---|---|---|---|---|---|
| $1$ | $1$ | $1$ | $1$ | $1$ | $1$ | $1$ |
| $1$ | $0$ | $0$ | $0$ | $0$ | $1$ | $1$ |
| $0$ | $1$ | $1$ | $0$ | $1$ | $1$ | $1$ |
| $0$ | $1$ | $0$ | $1$ | $0$ | $0$ | $1$ |
となり、確かめたいことが分かった。
同様に $(\lnot(\varphi\land\psi))\leftrightarrow(\lnot\varphi\lor\lnot\psi)$ が恒真であるかを調べるためには $\overline{\nu}(\varphi)$ が $0,1$ どちらを取るか、$\overline{\nu}(\varphi)$ が $0,1$ どちらを取るかの $2\cdot 2=4$ 通りを考えて真理表に書き込む。
| $(\lnot$ | $(\varphi$ | $\land$ | $\psi))$ | $\leftrightarrow$ | $(\lnot$ | $\varphi$ | $\lor$ | $\lnot$ | $\psi)$ |
|---|---|---|---|---|---|---|---|---|---|
| $1$ | $1$ | $1$ | $1$ | ||||||
| $1$ | $0$ | $1$ | $0$ | ||||||
| $0$ | $1$ | $0$ | $1$ | ||||||
| $0$ | $0$ | $0$ | $0$ |
| $(\lnot$ | $(\varphi$ | $\land$ | $\psi))$ | $\leftrightarrow$ | $(\lnot$ | $\varphi$ | $\lor$ | $\lnot$ | $\psi)$ |
|---|---|---|---|---|---|---|---|---|---|
| $1$ | $1$ | $1$ | $0$ | $1$ | $0$ | $1$ | |||
| $1$ | $0$ | $0$ | $0$ | $1$ | $1$ | $0$ | |||
| $0$ | $0$ | $1$ | $1$ | $0$ | $0$ | $1$ | |||
| $0$ | $0$ | $0$ | $1$ | $0$ | $1$ | $0$ |
| $(\lnot$ | $(\varphi$ | $\land$ | $\psi))$ | $\leftrightarrow$ | $(\lnot$ | $\varphi$ | $\lor$ | $\lnot$ | $\psi)$ |
|---|---|---|---|---|---|---|---|---|---|
| $0$ | $1$ | $1$ | $1$ | $0$ | $1$ | $0$ | $0$ | $1$ | |
| $1$ | $1$ | $0$ | $0$ | $0$ | $1$ | $1$ | $1$ | $0$ | |
| $1$ | $0$ | $0$ | $1$ | $1$ | $0$ | $1$ | $0$ | $1$ | |
| $1$ | $0$ | $0$ | $0$ | $1$ | $0$ | $1$ | $1$ | $0$ |
| $(\lnot$ | $(\varphi$ | $\land$ | $\psi))$ | $\leftrightarrow$ | $(\lnot$ | $\varphi$ | $\lor$ | $\lnot$ | $\psi)$ |
|---|---|---|---|---|---|---|---|---|---|
| $0$ | $1$ | $1$ | $1$ | $1$ | $0$ | $1$ | $0$ | $0$ | $1$ |
| $1$ | $1$ | $0$ | $0$ | $1$ | $0$ | $1$ | $1$ | $1$ | $0$ |
| $1$ | $0$ | $0$ | $1$ | $1$ | $1$ | $0$ | $1$ | $0$ | $1$ |
| $1$ | $0$ | $0$ | $0$ | $1$ | $1$ | $0$ | $1$ | $1$ | $0$ |
と $\leftrightarrow$ の下が全て $1$ となり恒真であることが分かる。
定義 11 (否定標準形)
論理式 $\varphi$ が否定標準形 (negation normal form, NNF) であるということ帰納的に定義する。
- 命題変数 $p$ とその否定 $\lnot p$ は否定標準形である。
- $\top,\bot$ は否定標準形である。
- $\varphi,\psi$ が否定標準形であるとき、$\varphi\land\psi,\varphi\lor\psi$ は否定標準形である。
つまり否定標準形は否定が命題変数にしか掛かっていなく、また $\to$ が使われていない論理式のことを指す。
定理 12 (否定標準形定理)
任意の論理式 $\varphi$ に対して、ある否定標準形 $\varphi^*$ が存在して $\models\varphi\leftrightarrow\varphi^*$ となる。
Proof.
まず $\leftrightarrow$ が推移的であることに注意する。論理式の構成に関する帰納法で示す。命題変数 $p$ に対しては自身が否定標準形で $\models p\leftrightarrow p$ であり良い。
$\lnot p$ であるときは $\lnot p$ 自身が否定標準形であり良い。
$\lnot\lnot\varphi_0$ であるときは二重否定除去から $\models(\lnot\lnot\varphi_0)\leftrightarrow\varphi_0$ であり $\varphi_0$ に帰納法の仮定を用いて $\models\varphi\leftrightarrow\varphi_0^*$ となる否定標準形 $\varphi_0^*$ を取れば $\models (\lnot\lnot\varphi_0)\leftrightarrow\varphi_0^*$ となり良い。
$\lnot(\varphi_0\lor\varphi_1)$ に対しDe Morganの法則から $\models (\lnot(\varphi_0\lor\varphi_1))\leftrightarrow(\lnot\varphi_0\land\lnot\varphi_1)$ であり $\lnot\varphi_0,\lnot\varphi_1$ に帰納法の仮定を適用し $\models(\lnot\varphi_0)\leftrightarrow(\lnot\varphi_0)^*,\models(\lnot\varphi_1)\leftrightarrow(\lnot\varphi_1)^*$ となる否定標準形 $(\lnot\varphi_0)^*,(\lnot\varphi_1)^*$ を取れば $\models(\lnot\varphi_0\land\lnot\varphi_1)\leftrightarrow((\lnot\varphi_0)^*\land(\lnot\varphi_1)^*)$ であり、よって $\models(\lnot(\varphi_0\lor\varphi_1) )\leftrightarrow( (\lnot\varphi_0)^*\land(\lnot\varphi_1)^*)$ となる。
$\lnot(\varphi_0\land\varphi_1)$ に対しDe Morganの法則から $\models (\lnot(\varphi_0\land\varphi_1))\leftrightarrow(\lnot\varphi_0\lor\lnot\varphi_1)$ であり $\lnot\varphi_0,\lnot\varphi_1$ に帰納法の仮定を適用し $\models(\lnot\varphi_0)\leftrightarrow(\lnot\varphi_0)^*,\models(\lnot\varphi_1)\leftrightarrow(\lnot\varphi_1)^*$ となる否定標準形 $(\lnot\varphi_0)^*,(\lnot\varphi_1)^*$ を取れば $\models(\lnot\varphi_0\lor\lnot\varphi_1)\leftrightarrow((\lnot\varphi_0)^*\lor(\lnot\varphi_1)^*)$ であり、よって $\models(\lnot(\varphi_0\land\varphi_1) )\leftrightarrow( (\lnot\varphi_0)^*\lor(\lnot\varphi_1)^*)$ となる。
$\lnot(\varphi_0\to\varphi_1)$ に対し $\models(\varphi_0\to\varphi_1)\leftrightarrow(\lnot\varphi_0\lor\varphi_1)$ であり、よって $\models(\lnot(\varphi_0\to\varphi_1))\leftrightarrow(\lnot(\lnot\varphi_0\lor\varphi_1))$、De Morganの法則、及び二重否定除去から $\models (\lnot(\lnot\varphi_0\lor\varphi_1))\leftrightarrow(\varphi_0\land\lnot\varphi_1)$ であり $\varphi_0,\lnot\varphi_1$ に帰納法の仮定を適用し $\models\varphi_0\leftrightarrow\varphi_0^*,\models(\lnot\varphi_1)\leftrightarrow(\lnot\varphi_1)^*$ となる否定標準形 $\varphi_0^*,(\lnot\varphi_1)^*$ を取れば $\models(\varphi_0\land\lnot\varphi_1)\leftrightarrow(\varphi_0^*\land(\lnot\varphi_1)^*)$ であり、よって $\models(\lnot(\varphi_0\to\varphi_1))\leftrightarrow(\varphi_0^*\land(\lnot\varphi_1)^*)$ となる。
$\varphi_0\lor\varphi_1$ に対して帰納法の仮定から $\models\varphi_0\leftrightarrow\varphi_0^*,\models\varphi_1\leftrightarrow\varphi_1^*$ となる否定標準形 $\varphi_0^*,\varphi_1^*$ が存在する。 よって$\models(\varphi_0\lor\varphi_1)\leftrightarrow(\varphi_0^*\lor\varphi_1^*)$ となり $\varphi_0^*\lor\varphi_1^*$ は否定標準形である。
$\varphi_0\land\varphi_1$ に対して帰納法の仮定から $\models\varphi_0\leftrightarrow\varphi_0^*,\models\varphi_1\leftrightarrow\varphi_1^*$ となる否定標準形 $\varphi_0^*,\varphi_1^*$ が存在する。 よって$\models(\varphi_0\land\varphi_1)\leftrightarrow(\varphi_0^*\land\varphi_1^*)$ となり $\varphi_0^*\land\varphi_1^*$ は否定標準形である。
$\varphi_0\to\varphi_1$ に対して$\models(\varphi_0\to\varphi_1)\leftrightarrow(\lnot\varphi_0\lor\varphi_1)$ であり $\lnot\varphi_0,\varphi_1$ に帰納法の仮定を適用し $\models(\lnot\varphi_0)\leftrightarrow(\lnot\varphi_0)^*,\models\varphi_1\leftrightarrow\varphi_1^*$ となる否定標準形 $(\lnot\varphi_0)^*,\varphi_1^*$ が存在する。 よって$\models(\varphi_0\to\varphi_1)\leftrightarrow((\lnot\varphi_0)^*\lor\varphi_1^*)$ となり $(\lnot\varphi_0)^*\lor\varphi_1^*$ は否定標準形である。
□命題論理の形式的証明
命題論理には形式的証明 (formal proof) というのが考えられる。形式的証明にはさまざまな流儀が知られている。 例えばG. Gentzen12 による自然演繹 (natural deduction) や推件計算 (sequent calculus) やD. HilbertによるHilbert流 (Hilbert style) がある。 以下ではGentzenによる推件計算をW.W. Tait 3が改良したTait計算 (Tait calculus) を用いる。
形式的証明を定義するときは命題論理の論理式の定義を少し変えることによって簡易化できる。 まず論理結合子のいくつかは他の論理結合子を用いて表現することができる。例えば $\varphi\to\psi$ が $\lnot\varphi\lor \psi$ と同値であることを用いることで、$\varphi\to\psi$ を $\lnot\varphi\lor\psi$ の記法としての省略として考えることができるからである。Tait計算では論理結合子として $\land,\lor$ のみを用いて命題変数 $p\in\mathrm{PropVar}$ に対して、その補 (complement) $\overline{p}$ が $\mathrm{PropVar}$ に含まれていると仮定する。 $\overline{p}$ は $\lnot p$ を表している、つまりTait計算では命題変数に対してしか否定は定義されない。この定義の背景には否定標準形定理に基づく。
定義 13 (論理式の再定義)
命題変数の集合 $\mathrm{PropVar}$ は偶数個の要素を持つ、あるいは無限集合であるとし、写像 $\overline{\blank}:\mathrm{PropVar}\to\mathrm{PropVar}$ があり $p\neq\overline{p},\overline{\overline{p}}=p$ を満たすとする。 $p\in\mathrm{PropVar}$ に対して、$\overline{p}$ をその補 (complement) といい、これは $\lnot p$ を意図している。
- $\mathrm{PropVar}$ の要素は論理式である。
- $\top$ と $\bot$ はともに論理式である。
- $\varphi,\psi$ が論理式であるとき、$(\varphi\land\psi),(\varphi\lor\psi)$ は論理式である。
また論理式 $\varphi$ に対して否定 $\lnot\varphi$ を以下のように帰納的に定義する。
- $\lnot p:=\overline{p}$ とする。
- $\lnot \top:=\bot$ とする。
- $\lnot \bot:=\top$ とする。
- $\lnot(\varphi\land\psi):=\lnot\varphi\lor\lnot\psi$ とする。
- $\lnot(\varphi\lor\psi):=\lnot\varphi\land\lnot\psi$ とする。
また $\varphi\to\psi:=\lnot\varphi\lor\psi$ とする。
定義 14 (推件)
論理式の有限集合を推件 (sequent) といいギリシャ文字の大文字 $\Gamma,\Delta,\Theta,\ldots$ などで表す[脚注 5]
また $\Gamma,\Delta$ で$\Gamma\cup\Delta$ を、$\Gamma,\varphi$ で$\Gamma\cup\{\varphi\}$ を表すものとする。
注意 15 (推件に対する注意)
推件は有限集合と定義されていることから $\Gamma:=\{\varphi,\varphi\},\Delta:=\{\varphi\}$ としたとき $\Gamma=\Delta$ となる。また $\Gamma:=\{\varphi,\psi\},\Delta=\{\psi,\varphi\}$ としたときも $\Gamma=\Delta$ となる。
定義 16 (Tait計算)
理論 $T$ 、推件 $\Gamma$ に対して証明可能性関係 (provability relation) $T\vdash\Gamma$[脚注 6]を以下のように帰納的に定義する。
- $(\mathsf{id})$ 任意の推件 $\Gamma$ 、命題変数 $p$ に対して $T\vdash\Gamma,\overline{p},p$ である。
- $(\mathsf{\top})$ 任意の推件 $\Gamma$ に対して $T\vdash\Gamma,\top$ である。
- $(T)$ 任意の推件 $\Gamma$ 、任意の $\varphi\in T$ に対し $T\vdash\Gamma,\varphi$ である。
- $(\land)$ 任意の推件 $\Gamma$ 、任意の論理式 $\varphi_0,\varphi_1$ に対して、 任意の $i\in 2$ に対して $T\vdash\Gamma,\varphi_0\land\varphi_1,\varphi_i$ であるとき $T\vdash\Gamma,\varphi_0\land\varphi_1$である。
- $(\lor)$ 任意の推件 $\Gamma$ 、任意の論理式 $\varphi_0,\varphi_1$ に対して、 ある $i\in 2$ に対して $T\vdash\Gamma,\varphi_0\lor\varphi_1,\varphi_i$ であるとき $T\vdash\Gamma,\varphi_0\lor\varphi_1$である。
- $(\mathsf{cut})$ 任意の推件 $\Gamma,\Delta$ 、任意の論理式 $\varphi$ に対して、 $T\vdash\Gamma,\varphi$ かつ $T\vdash\lnot\varphi,\Delta$ であるとき $T\vdash\Gamma,\Delta$ である[脚注 7]。
ここで1,2,3を始件 (initial sequent, axiom) といい、4,5,6を推論規則 (inference rule) という。
また各始件での主論理式 (major formula, principal formula) と副論理式 (minor formula, arbitrary formula) を以下のように定める。
| 始件/推論規則 | 主論理式 | 副論理式 |
|---|---|---|
| $(\mathsf{id})$ | $\overline{p}$ 及び $p$ | $\blank$ |
| $(\top)$ | $\top$ | $\blank$ |
| $(T)$ | $\varphi$ | $\blank$ |
| $(\land)$ | $\varphi_0\land\varphi_1$ | $\varphi_0$ 及び $\varphi_1$ |
| $(\lor)$ | $\varphi_0\lor\varphi_1$ | $\varphi_i$ |
| $(\mathsf{cut})$ | ${-}$ | ${-}$ |
また $(\mathsf{cut})$ に於ける $\varphi$ をカット論理式 (cut formula) という。 主論理式、副論理式、カット論理式はどの論理式に対して始件あるいは推論規則を明示するために用いられる。 また始件と推論規則の区別は証明の定義に関する帰納法を回す場合にベースケースと帰納法の仮定を用いるところ、すなわち自然数での帰納法に於いて「$0$ に於いて成り立つことを示す部分」と「$k$ に対して成り立つことを仮定し、$k+1$ に対して成り立つことを示す部分」を区別するときに重要になる。
$\vdash$ に関していくつかの用語を定める。
- $T\vdash\Gamma$ であるとき $T$ から $\Gamma$ は証明可能 (provable) であるという。また $\emptyset\vdash\Gamma$ であるとき単に証明可能であるといい、$\vdash\Gamma$ と表す。
- $T\vdash\varphi$ であるとき $T$ から $\varphi$ は証明可能であるという。
- $T\vdash\lnot\varphi$ であるとき $T$ から $\varphi$ は反証可能 (disprovable, refutable) であるという。
- $\mathrm{Th}(T):=\{\varphi\in\mathrm{PropFml}\mid T\vdash\varphi\}$ とする。
例 17 (Tait計算による証明の例)
例として $\vdash p\to q\to p$ を確かめてみる。 まず $p\to q\to p$ は $\lnot p\lor(\lnot q\lor p)$ の省略であった。
- $(\mathsf{id})$ により $\vdash \lnot p\lor(\lnot q\lor p),\lnot q\lor p,\lnot p, p$ 。ここで主論理式は $\lnot p, p$ 。
- 1と $(\lor)$ により $\vdash\lnot p\lor(\lnot q\lor p),\lnot p,\lnot q\lor p$ 。ここで主論理式は $\lnot q\lor p$ 、副論理式は $p$ である。
- 2と $(\lor)$ により $\vdash\lnot p\lor(\lnot q\lor p),\lnot p$ 。ここで主論理式は $\lnot p\lor(\lnot q\lor p)$ 、副論理式は $\lnot q\lor p$ である。
- 3と $(\lor)$ により $\vdash\lnot p\lor(\lnot q\lor p)$ 。ここで主論理式は $\lnot p\lor(\lnot q\lor p)$ 、副論理式は $\lnot p$ である。
定義 18 (証明木)
形式的証明をグラフィカルに表示したいときしばし用いられる、証明木 (proof tree) を紹介する。 証明木は名前の通り木構造を持ち、葉に始件がラベルされ、根に証明する推件がラベルされ、隣接するノードの間は推論規則で結ばれている。また根を下に、葉を上に書く。 例えば \begin{prooftree} \AxiomC{\(\Gamma_0\)} \AxiomC{\(\Gamma_1\)} \BinaryInfC{\(\Delta\)} \end{prooftree} のように表したとき \(\Gamma_0\) と \(\Gamma_1\) から \(\Delta\) が導かれたことを表す。 推論規則 \((\land)\) は \begin{prooftree} \AxiomC{\(\Gamma,\varphi_0\land\varphi_1,\varphi_0\)} \AxiomC{\(\Gamma,\varphi_0\land\varphi_1,\varphi_1\)} \RightLabel{\((\land)\)} \BinaryInfC{\(\Gamma,\varphi_0\land\varphi_1\)} \end{prooftree} と表される。 推論規則 \((\lor)\) は \begin{prooftree} \AxiomC{\(\Gamma,\varphi_0\lor\varphi_1,\varphi_i\)} \RightLabel{\((\lor)\)} \UnaryInfC{\(\Gamma,\varphi_0\lor\varphi_1\)} \end{prooftree} と表される。
一般的に始件と推論規則が与えられたとき証明木は以下のように定義される。
- 始件は証明木である。
- \(\mathcal{D}_0,\ldots\mathcal{D}_n\) が証明木で各証明木 \(\mathcal{D}_i\) の一番下にある推件が、推論規則 \((I)\) の上件と一致し、\(I\) の下件を \(\Gamma\) とするとき、
\begin{prooftree}\AxiomC{\(\mathcal{D}_0\)}\AxiomC{\(\cdots\)}\AxiomC{\(\mathcal{D}_n\)}\RightLabel{\((I)\)}\TrinaryInfC{\(\Gamma\)}\end{prooftree}は証明木である。
例 19 (証明木の例)
\((\lnot p\lor q)\lor(p\land \lnot q)\) の証明木は以下の通りである。 \begin{prooftree} \AxiomC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q,(p\land \lnot q),\lnot p,p\)} \RightLabel{\((\lor)\)} \UnaryInfC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q,(p\land \lnot q),p\)} \AxiomC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q,(p\land \lnot q),\lnot q,q\)} \RightLabel{\((\lor)\)} \UnaryInfC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q,(p\land \lnot q),\lnot q\)} \RightLabel{\((\land)\)} \BinaryInfC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q,(p\land \lnot q)\)} \RightLabel{\((\lor)\)} \UnaryInfC{\((\lnot p\lor q)\lor(p\land \lnot q),\lnot p\lor q\)} \RightLabel{\((\lor)\)} \UnaryInfC{\((\lnot p\lor q)\lor(p\land \lnot q)\)} \end{prooftree}
命題 20 (証明論的コンパクト性 (proof-theoretic compactness))
$T\vdash\varphi$ であるならば、ある $T$ の有限部分集合 $T'$ が存在して $T'\vdash\varphi$ である。
Proof.
証明に現れる始件 $(T)$ の個数は有限個であり、その主論理式全体の集合を $T'$ とし、$(T)$ の代わりに $(T')$ を用いれば良い。正確にはTait計算の定義に関する帰納法で示す必要があるが推論規則を用いて導出された場合は明らかである。
□命題 21 (弱化補題 (weakening lemma))
$T\vdash\Gamma$ ならば $T\vdash\Gamma,\Delta$ である。
Proof.
Tait計算の定義に関する帰納法で示す。まず始件の場合 $T\vdash\Gamma$ が始件なら $T\vdash\Gamma,\Delta$ も始件になるため良い。 推論規則を用いて $T\vdash\Gamma$ から $T\vdash\Gamma'$ が導出されたとする。$T\vdash\Gamma$ に帰納法の仮定を用いることで $T\vdash\Gamma,\Delta$ であり、同じ推論規則を適用することで $T\vdash\Gamma',\Delta$ となる。
□命題 22 (トートロジー (tautology-lemma))
任意の論理式 $\varphi$ に対して $T\vdash \lnot\varphi,\varphi$ である。
Proof.
論理式の定義に関する帰納法で示す。まず原子論理式 $p$ に対しては $(\mathsf{id})$ から良い。$\varphi$ が $\varphi_0\land\varphi_1$ の場合、帰納法の仮定と弱化補題から $T\vdash\lnot\varphi_0,\varphi_0,\lnot\varphi_1,\varphi_0\land\varphi_1,\lnot\varphi_0\lor\lnot\varphi_1$ かつ $T\vdash\lnot\varphi_1,\varphi_1,\lnot\varphi_0,\varphi_0\land\varphi_1,\lnot\varphi_0\lor\lnot\varphi_1$ であり $(\land)$ から $T\vdash\lnot\varphi_0,\lnot\varphi_1,\varphi_0\land\varphi_1,\lnot\varphi_0\lor\lnot\varphi_1$ であり $(\lor)$ を二回適用して $T\vdash\varphi_0\land\varphi_1,\lnot\varphi_0\lor\lnot\varphi_1$ となる。$\varphi$ が $\varphi_0\lor\varphi_1$ の場合も同様に示せる。
□命題 23 ($\land$-遡及補題 ($\land$-inversion lemma))
$T\vdash\Gamma,\varphi_0\land\varphi_1$ ならば任意の $i\in 2$ に対し $T\vdash\Gamma,\varphi_i$ である。
Proof.
Tait計算の定義に関する帰納法で示す。まず $(\mathsf{id}),(\top)$ によって $\Gamma,\varphi_0\land\varphi_1$ が始件である場合、$\overline{p},p\in\Gamma,$ あるいは $\top\in\Gamma$ であり、よって同じ始件から $T\vdash\Gamma,\varphi_i$ となる。 また $\varphi_0\land\varphi_1\in T$ から $(T)$ によって始件となる場合を考える。この場合トートロジー補題、弱化補題から $T\vdash\varphi_i,\lnot\varphi_i,\lnot\varphi_0\lor\lnot\varphi_1$ であり $(\lor)$ から $T\vdash\varphi_i,\lnot\varphi_0\lor\lnot\varphi_1$ であり、$T\vdash\Gamma,\varphi_0\land\varphi_1$ から $(\mathsf{cut})$ を用いることで $T\vdash\Gamma,\varphi_i$ を得る。
$(\land)$ 以外の推論規則の場合は帰納法の仮定から明らかである。よって $(\land)$ で $T\vdash\Gamma,\varphi_0\land\varphi_1$ が導けたとする。ここで $\varphi_0\land\varphi_1$を主論理式としよう。 $(\land)$ を用いていて $\varphi_0\land\varphi_1$ が主論理式であることから $T\vdash\Gamma,\varphi_i,\varphi_0\land\varphi_1$ である。よって帰納法の仮定から $T\vdash\Gamma,\varphi_i$ となる。
□命題 24 ($\lor$-遡及補題 ($\lor$-inversion lemma))
$T\vdash\Gamma,\varphi_0\lor\varphi_1$ ならば $T\vdash\Gamma,\varphi_0,\varphi_1$ である[脚注 8]。
Proof.
Tait計算の定義に関する帰納法で示す。まず $(\mathsf{id}),(\top)$ によって $\vdash\Gamma,\varphi_0\lor\varphi_1$ が始件である場合、$\overline{p},p\in\Gamma,$ あるいは $\top\in\Gamma$ であり、よって同じ始件から $T\vdash\Gamma,\varphi_0,\varphi_1$ となる。 また $\varphi_0\lor\varphi_1\in T$ から $(T)$ によって始件となる場合を考える。この場合トートロジー補題、弱化補題から $T\vdash\varphi_i,\lnot\varphi_i,\varphi_{1-i},\lnot\varphi_0\land\lnot\varphi_1$ であり $(\land)$ から $T\vdash\varphi_0,\varphi_1,\lnot\varphi_0\land\lnot\varphi_1$ であり、$T\vdash\Gamma,\varphi_0\lor\varphi_1$ から $(\mathsf{cut})$ を用いることで $T\vdash\Gamma,\varphi_0,\varphi_1$ を得る。
$(\lor)$ 以外の推論規則の場合は帰納法の仮定から明らかである。よって $(\lor)$ で $T\vdash\Gamma,\varphi_0\lor\varphi_1$ が導けたとする。ここで $\varphi_0\lor\varphi_1$を主論理式としよう。 $(\lor)$ を用いていて $\varphi_0\lor\varphi_1$ が主論理式であることからある $i\in 2$ に対して $T\vdash\Gamma,\varphi_i,\varphi_0\lor\varphi_1$ である。よって帰納法の仮定から $T\vdash\Gamma,\varphi_0,\varphi_1$ となる。
□命題 25 (演繹定理 (deduction theorem))
任意の理論 $T$ と推件 $\Gamma$ 、論理式 $\varphi$ に関して以下は同値である。
- $T+\varphi\vdash\Gamma$ である。
- $T\vdash\lnot\varphi,\Gamma$ である。
Proof.
まず $T+\varphi\vdash\Gamma$ を仮定したとき、$T\vdash\lnot\varphi,\Gamma$ が成り立つことをTait 計算の定義に関する帰納法で示す。始件の場合 $(T+\varphi)$ によって $\varphi\in\Gamma$ に対し $T+\varphi\vdash\Gamma$ となるとき以外は明らかである。 $(T+\varphi)$ によって $T+\varphi\vdash\Delta,\varphi$ としよう。ここで$\Delta:=\Gamma\setminus\{\varphi\}$ とする。トートロジー補題、弱化補題から $T\vdash\Delta,\lnot\varphi,\varphi$ であり良い。
推論規則によって $T+\varphi\vdash \Gamma'$ から $T+\varphi\vdash \Gamma$ が導かれた場合帰納法の仮定から $T\vdash \lnot\varphi,\Gamma'$ であり同じ推論規則を適用することで $T\vdash \lnot\varphi,\Gamma$ である。
次に $T\vdash\lnot\varphi,\Gamma$ を仮定して $T+\varphi\vdash\Gamma$ を示す。明らかに$T+\varphi\vdash\lnot\varphi,\Gamma$ であり、$(T+\varphi)$ から $T+\varphi\vdash\varphi$ であるから $(\mathsf{cut})$ から $T+\varphi\vdash\Gamma$ である。
□系 26 (演繹定理 (deduction theorem))
任意の理論 $T$ と推件 $\Gamma$ 、論理式 $\varphi$ に関して以下は同値である。
- $T+\varphi\vdash\psi$ である。
- $T\vdash\varphi\to\psi$ である。
Proof.
$T\vdash\varphi\to\psi$ であることと $T\vdash\lnot\varphi,\psi$ であることが同値であることと演繹定理から従う。$T\vdash\varphi\to\psi$ ならば $T\vdash\lnot\varphi,\psi$ であることは $\varphi\to\psi$ が $\lnot\varphi\lor\psi$ の略記であったことと $\lor$-遡及補題による。逆は弱化補題によって $T\vdash\lnot\varphi\lor\psi,\lnot\varphi,\psi$ であり、$(\lor)$ を二回用いれば良い。
□完全性とコンパクト性
命題論理の基本的性質である完全性定理とコンパクト性定理に関して述べる。一般に証明可能性関係 $\vdash$ と論理的帰結関係 $\models$ が与えられたとき「 $T\vdash\varphi$ ならば $T\models\varphi$ 」という形をした主張を健全性 (soundness) といい、逆「 $T\models\varphi$ ならば $T\vdash\varphi$ 」という形をした主張を完全性 (completeness) という。完全性、及び健全性が成り立てば異なるが同値となる二つの関係 $\vdash$ 、$\models$ から論理を分析することができ、とても扱いやすい。 以下では上述した証明可能性関係と論理的帰結関係に対して完全性定理と健全性定理が成り立つことを示し、その帰結としてコンパクト性定理 (compactness theorem) を示す。
証明の方針を大まかに説明する。定理の主張自体は、理論 $T$ に対し、無矛盾性、すなわち $\bot$ の証明不能性と、モデルの存在性から即座に導かれる。よって無矛盾な理論に対してモデルの存在を示せば良い訳であるが、モデルを存在することを示すために、任意の論理式 $\varphi$ に対して $U\vdash\varphi$ か $U\vdash\lnot\varphi$ が成り立ち、かつ無矛盾であるという条件を満たす理論、極大無矛盾理論という概念を定義する。極大無矛盾理論さえ存在すればその理論から自然に付値、モデルの存在が言えるので極大無矛盾理論への拡大が寛容である。この拡大は理論の包含関係が帰納的半順序を成すことに気づけばZornの補題を用いることで取ることができる。よって完全性定理が示される訳だ。
定理 27 (健全性定理 (soundness theorem))
Proof.
任意の理論 $T$ に対して、$T\vdash\varphi$ ならば $T\models\varphi$ である。 Tait計算の定義に関する帰納法で $T\vdash\Gamma$ ならば、ある $\varphi\in\Gamma$ が存在して $T\models\varphi$ となることを示す。
始件 $(\mathsf{id})$ によって $T\vdash\Gamma,\lnot p,p$ の場合、任意の付値 $\nu$ に対して明らかに $\nu(p)=1$ か $\nu(\lnot p)=1$ となるため良い。
始件 $(\top)$ によって $T\vdash\Gamma,\top$ となる場合、任意の付値 $\nu$ に対して $\nu(\top)=1$ となり良い。
始件 $(T)$ によって $\varphi\in T$ に対して $T\vdash\Gamma,\varphi$ となる場合、 $T$ を充足する任意の付値に対して $\nu(\varphi)=1$ となり良い。
推論規則 $(\land)$ によって $i\in 2$ に対して $T\vdash\Gamma,\varphi_0\land\varphi_1,\varphi_i$ から $T\vdash\Gamma,\varphi_0\land\varphi_1$ になる場合、帰納法の仮定から、任意の $i\in 2$ に対して、ある$\psi_i\in\Gamma\cup\{\varphi_0\land\varphi_1,\varphi_i\}$ が存在して $T\models\psi_i$ である。 $\psi_i$ が $\varphi_i$ と等しいとき以外は明らかであるためその場合を考える。$T\models\varphi_0$ かつ $T\models\varphi_1$ であり、よって $\nu\models T$ を満たす付値 $\nu$ を任意に取ると $\nu\models\varphi_0$ かつ $\nu\models\varphi_1$ であり $\models$ の定義から $\nu\models\varphi_0\land\varphi_1$ である。よって $T\models\varphi_0\land\varphi_1$ である。
推論規則 $(\lor)$ によって、ある $i\in 2$ に対して $T\vdash\Gamma,\varphi_0\lor\varphi_1,\varphi_i$ から $T\vdash\Gamma,\varphi_0\lor\varphi_1$ になる場合、帰納法の仮定から、ある $i\in 2$ に対して、$\psi_i\in\Gamma\cup\{\varphi_0\lor\varphi_1,\varphi_i\}$ が存在して $T\models\psi_i$ である。 $\psi_i$ が $\varphi_i$ と等しいとき以外は明らかであるためその場合を考える。$T\models\psi_i$ であり、よって $\nu\models T$ を満たす付値 $\nu$ を任意に取ると $\nu\models\varphi_i$ であり、$\models$ の定義から $\nu\models\varphi_0\lor\varphi_1$ である。よって $T\models\varphi_0\lor\varphi_1$ である。
推論規則 $(\mathsf{cut})$ によって $T\vdash\Gamma,\varphi$ かつ $T\vdash\lnot\varphi,\Delta$ から $T\vdash\Gamma,\Delta$ になる場合、帰納法の仮定から、ある $\psi\in\Gamma\cup\{\varphi\}$ に対して $T\models\psi$ かつ ある $\chi\in\Delta\cup\{\lnot\varphi\}$ に対して $T\models\chi$ である。 $\psi\in\Gamma$ か $\chi\in\Delta$ の場合、$\Gamma\subseteq\Gamma\cup\Delta$ と $\Delta\subseteq \Gamma\cup\Delta$ から明らかである。よって問題になるのは $psi$ が $\varphi$ で $\chi$ が $\lnot\varphi$ である場合だが、これはありえない。 なぜなら任意の付値 $\nu$ に対して $\nu\models\varphi$ かつ $\nu\models\lnot\varphi$ は $\nu\models\varphi\land\lnot\varphi$ と同値であり、これは命題1.2.4から $\overline{\nu}(\varphi\land\lnot\varphi)=1$ と同値であり、つまり $\min\{\nu(\varphi),1-\nu(\varphi)\}=1$ であるが、$\nu(\varphi)$ が $0$ であろうが $1$ であろうがこれはありえない。 また $\nu\models T$ なる $\nu$ が存在しない場合は、無内容的[脚注 9]に任意の論理式 $\varphi$ に対して $T\models\varphi$ であり良い。
□定義 28 (無矛盾と矛盾)
理論 $T$ が矛盾 (inconsistent) するとは $T\vdash\bot$ となることであり、無矛盾 (consistent) であるとは $T\nvdash\bot$ となることである。
命題 29 (矛盾の同値性)
任意の理論 $T$ に対して以下は互いに同値である。
- ある論理式 $\varphi$ に対して $T\vdash\varphi\land\lnot\varphi$ である。
- $T\vdash\emptyset$ である。
- $T\vdash\bot$ である。
- 任意の論理式 $\varphi$ に対して $T\vdash\varphi$ である。
Proof.
1を仮定して2を示す。$\land$-遡及補題から $T\vdash\varphi$ かつ $T\vdash\lnot\varphi$ であり $(\mathsf{cut})$ によって $T\vdash\emptyset$ となる。
2を仮定して3,4を示す。仮定から弱化補題を用いれば良い。
3を仮定して2を示す。仮定から $T\vdash\bot$ であり $(\top)$ から $T\vdash\top$ となり $(\mathsf{cut})$ から $T\vdash\emptyset$ である。
4から1は明らかである。
□系 30 (無矛盾の同値性)
任意の理論 $T$ に対して以下は互いに同値である。
- 任意の論理式 $\varphi$ に対して $T\nvdash\varphi\land\lnot\varphi$ である。
- $T\nvdash\emptyset$ である。
- $T\nvdash\bot$ である。
- ある論理式 $\varphi$ に対して $T\nvdash\varphi$ である。
Proof.
矛盾の同値性から明らかである。
□命題 31 (矛盾と証明可能性の関係)
任意の理論 $T$ 、論理式 $\varphi$ に対して以下は互いに同値である。
- $T+\lnot\varphi$ が矛盾する。
- $T\vdash\varphi$ である。
Proof.
命題 32 (無矛盾性と証明可能性の双対性)
- $T+\lnot\varphi$ が無矛盾である。
- $T\nvdash\varphi$ である。
Proof.
矛盾と証明可能性の関係から明らか。
□定義 33 (極大無矛盾性)
理論 $T$ が極大無矛盾 (maximally consistent) であるとは無矛盾であり、極大性 (maximality) 、$\mathrm{Th}(T)\subsetneq\mathrm{Th}(S)$ なる無矛盾な理論 $S$ が存在しないことである。
命題 34 (極大無矛盾な理論の証明可能性)
理論 $T$ が極大無矛盾であると仮定する。このとき任意の論理式 $\varphi$ に対して $T\vdash\varphi$ または $T\vdash\lnot\varphi$ である。
Proof.
背理法で示す。 ある論理式 $\varphi$ に対して $T\nvdash\varphi$ かつ $T\nvdash\lnot\varphi$であるとしよう。 $T\nvdash\lnot\varphi$ から $\lnot\varphi \notin\mathrm{Th}(T)$ であり、$\mathrm{Th}(T)\subsetneq\mathrm{Th}(T+\lnot\varphi)$ であるが、$T\nvdash\varphi$ と無矛盾性と証明可能性の双対性から $T\cup\{\lnot\varphi\}$ は無矛盾であり、よって極大性に矛盾する。
□定義 35 (極大無矛盾な理論に伴う付値)
極大無矛盾な理論 $U$ に対して付値 $\nu_U$ 以下のように定める。
$ \nu_U(p):=\begin{cases} 1 & U\vdash p\\ 0 & U\vdash \lnot p \end{cases}$。
命題 36 (極大無矛盾な理論に伴う付値と証明可能性の関係)
極大無矛盾な理論 $U$ に対して以下が成り立つ。
- 任意の論理式 $\varphi$ に対して $\nu_U\models\varphi$ と $U\vdash\varphi$ は同値である。
- $\nu_U\models U$ である。
- $\mathrm{Th}(T)\subseteq\mathrm{Th}(U)$ を満たす任意の理論 $T$ に対して $\nu_U\models T$ である。
Proof.
1を論理式の構成に関する帰納法で示す。命題変数 $p$ に対して $\nu_U\models p$ と $U\vdash p$ が同値なのは定義より明らかである。
$\nu_U\models \varphi_0\land\varphi_1$ と $U\vdash\varphi_0\land\varphi_1$ の同値性は帰納法の仮定から、任意の $i\in 2$ に対して $\nu_U\models \varphi_i$ と $U\vdash\varphi_i$ は同値であり、また 任意の $i\in 2$ に対して $U\vdash\varphi_i$ であることと $U\vdash\varphi_0\land\varphi_1$ であることが同値なことが弱化補題と $\land$-遡及補題から従うため良い。
$\nu_U\models \varphi_0\lor\varphi_1$ と $U\vdash\varphi_0\lor\varphi_1$ の同値性は互いの否定、 $\nu_U\models \lnot\varphi_0\land\lnot\varphi_1$ と $U\nvdash\varphi_0\lor\varphi_1$ を考えると極大無矛盾な理論の証明可能性から $U\nvdash\varphi_0\lor\varphi_1$ と $U\vdash\lnot\varphi_0\land\lnot\varphi_1$ が同値であることから上と同じ議論から従う。
2は1から、3は2から明らかである。
□補題 37 (極大無矛盾理論への拡大)
任意の無矛盾な理論 $T$ に対して ある極大無矛盾な理論 $U$ が存在し $T\subseteq U$ が成り立つ。
Proof.
$T\subseteq S$となる無矛盾な理論 $S$ 全体からなる集合を $\mathcal{B}_T$ とする。 まず $T\in \mathcal{B}_T$ から $\mathcal{B}_T$ は空ではない。また $\mathcal{B}_T$ 上の順序を$\leq_{\mathcal{B}_T}$ を
$$A\leq_{\mathcal{B}_T} B:\Leftrightarrow A\subseteq B$$
とすれば、包含関係 $\subseteq$ が半順序になることから $\langle\mathcal{B}_T;\leq_{\mathcal{B}_T}\rangle$ は半順序である。Zornの補題を用いて示すため、$\langle\mathcal{B}_T;\leq_{\mathcal{B}_T}\rangle$ が帰納的半順序であることを示したい。すなわち $\langle\mathcal{B}_T;\leq_{\mathcal{B}_T}\rangle$ の鎖、すなわち $X\subseteq\mathcal{B}_T$ を $\langle X,\leq_{\mathcal{B}_T}\!\restriction\! X\rangle$ が全順序になるように任意に取り、$T_X:=\bigcup X$ と定めたとき、これが $\mathcal{B}_T$ 上の $X$ の上界となることを示したい。 ここで $X$ が空なときは自明に上界を持つためは空でないとして良い。 $T\subseteq T_X$ は明らかであるから $T_X\in\mathcal{B}_T$ であることを示すためには $T_X$ が無矛盾であることを示せば良い。
$T_X$ が無矛盾であることを背理法で示そう。矛盾するとすれば $T_X\vdash\emptyset$ であり、証明論的コンパクト性から、ある有限集合 $T_X'\subseteq T_X$ が存在し $T_X'\vdash\emptyset$ である。ここで $T_X'$ は空でないとして良い。もし空なら自明な公理 $\top$ を考える、すなわち $T_X\vdash\emptyset$ ならば $\{\top\}\vdash\emptyset$ となることから $T'_X:=\{\top\}$ としてしまえば良いからである。 任意の $\varphi\in T_X'$ に対して $\varphi\in T_\varphi$ なる理論 $T_\varphi\in X$ が存在するため、それを一つずつ固定する。$X$ は全順序集合であったから、ある $\psi\in T_X'$ が存在し $T_\psi$ が $\{T_\varphi\mid\varphi\in T_X'\}$ に於いて最大となる。すなわち任意の $\varphi\in T_X'$ に対して $T_\varphi\subseteq T_\psi$ となるような $\psi\in T_X'$ が取れる。 よって $T_X'\subseteq T_\psi$ であり、$T_X'\vdash\emptyset$ であるから $T_\psi\vdash\emptyset$ となる。しかし $T_\psi\in \mathcal{B}_T$ で $\mathcal{B}_T$ の元は無矛盾な理論であるため矛盾する。
上の議論から $\langle\mathcal{B}_T;\leq_{\mathcal{B}_T}\rangle$ は帰納的半順序、すなわち Zornの補題の仮定を満たす。よって [[Zorn の補題]]から極大元 $U$ を持つ。これは $A\subseteq B$ が $\mathrm{Th}(A)\subseteq\mathrm{Th}(B)$ を含意するため明らかに極大無矛盾な理論である。
□定理 38 (モデル存在性定理 (model existence theorem))
任意の理論 $T$ に対し以下は同値である。
- $T$ は無矛盾である。
- $\nu\models T$ となる付値 $\nu$ が存在する。
Proof.
1を仮定して2を示す。極大無矛盾理論への拡大から $T$ の極大無矛盾拡大 $U$ を取る。極大無矛盾な理論に伴う付値と証明可能性から $\nu_U\models T$ となり良い。
2を仮定して1を示す。対偶 $T$ が矛盾するならば、任意の付値 $\nu$ に対して $\nu\models T$ とならないことを示そう。 $T$ が矛盾することから $T\vdash\bot$ であり、健全性定理から $T\models\bot$ である。しかし $\bot$ を充足する付値は存在しないため $T$ を充足する付値も存在しない。
□定理 39 (完全性定理 (completeness theorem))
任意の理論 $T$ 論理式 $\varphi$ に対して $T\models\varphi$ ならば $T\vdash\varphi$ である。また健全性定理と合わせると
- $T\vdash\varphi$ である。
- $T\models\varphi$ である。
は同値となる。
Proof.
対偶を示そう。無矛盾性と証明可能性の双対性から $T\nvdash\varphi$ ならば $T+\lnot\varphi$ は無矛盾であり、モデル存在性定理から $\nu\models T+\lnot\varphi$ となる付値 $\nu$ が存在する。 よって[[#relationship-between-extended-valuation-and-satisfiability-relation]充足可能性と論理的帰結の関係]から $T\models \varphi$ にはなりえない。
□命題 40 (証明論的コンパクト性と無矛盾性)
任意の理論 $T$ に対し以下は同値である。
- $T$ が無矛盾である。
- $T$ の任意の有限部分集合 $T'$ は無矛盾である。
Proof.
証明論的コンパクト性から明らかである。
□定理 41 (コンパクト性定理)
任意の理論 $T$ に対し以下は同値である。
- $\nu\models T$ なる付値 $\nu$ が存在する。
- 任意の有限集合 $T'\subseteq T$ に対し、ある付値 $\nu$ が存在して $\nu\models T'$ となる。
Proof.
証明論的コンパクト性と無矛盾性、及び完全性定理から明らかである。
□脚注
- ↑ 論理式は帰納的に定義されているが、その(包含関係に於ける)最小性を要求するために「以上によって論理式と分かるもののみが論理式である」と記述している。しかし帰納的に定義をする際、毎回同じようなことを書いていても諄いので以降省略する。
- ↑ $\models$ はダブルターンスタイル (double turnstile)という記号である。
- ↑ 「または」は包含的 (inclusive) なものであることに注意すべきである。すなわち $\nu\models\varphi,\nu\models\psi$ どちらも成り立つときも正しいとする。
- ↑ ややこしいことに、無矛盾律のことを矛盾律 (law of contradiction) ということもある。
- ↑ 推件の定義は有限多重集合や有限列、あるいは有限木とされる場合もある。その場合は構造規則 (structural rule) という規則を後述する形式的証明に追加しなければならない。またそのとき追加する規則を制限して得られる論理を部分構造論理 (substructural logic) という。
- ↑ $\vdash$ はターンスタイル (turnstile)という記号である。
- ↑ 三段論法 (syllogism) と言われることもある。
- ↑ 「$T\vdash\Gamma,\varphi_0\lor\varphi_1$ ならばある $i\in 2$ に対して $T\vdash\Gamma,\varphi_i$ である。」という命題を選言特性 (disjunction property) という。選言特性は古典論理に於いて一般的に成り立たないことが知られている。例えば $T$ 空としたとき、原子論理式 $p$ に対して $\lnot p\lor p$ は明らかに証明可能である。 一方 $p$ と $\lnot p$ はどちらも証明不能となる。一方、直観主義論理や線形論理などの非古典論理では成り立つ場合があることが知られている。
- ↑ "vacuously"の訳として「無内容的」という語を用いた。
出典
- 3 W. W. Tait. "Normal derivability in classical logic". The syntax and semantics of infinitary languages. Springer, Berlin, Heidelberg (1968): 204–236.
