数理論理学：ノート3 - クッキーの日記

読んでいる本（出典）：数理論理学 | 戸次大介 |本 | 通販 | Amazon

前回：ノート2 ／次回：ノート4
目次：数理論理学

第4章は一階命題論理の応用としての論理回路の話で、ノートは省略。
以下、第5章前半の自分の理解。第5章は一階述語論理。今回のノートは統語論まで。

前回までのあらすじ

「妥当な証明とは何か」を打ち立てるために、まず一階命題論理という体系を考えた。
- 個々の命題を論理式（原子命題を表す命題記号 or 論理式を真理関数に代入したもの）で表し、 $2$ 原子命題の数通りの解釈の上に個々の論理式の真偽 $\{1,0\}$ を定めた。
- ある解釈の下で、前提の命題たちを表す論理式列が全て $1$ で、帰結の命題を表す論理式が $0$ になる場合、その推論は妥当でないとした（どんな解釈の下でもそうならない場合、その推論は妥当であるとした）。

一階命題論理で表現できないこと

一階命題論理では個々の原子命題の中身には立ち入らず、各々の原子命題が真のパターンの解釈・偽のパターンの解釈を考える。
他方、我々は直観的には以下のように無数につくれる原子命題が全部真であることがわかる。
　　　 $P_1 \equiv$ 「西暦2019年は平成ではない」
　　　 $P_2 \equiv$ 「西暦2020年は平成ではない」
　　　 $P_3 \equiv$ 「西暦2021年は平成ではない」
　　　 $\cdots$
もし真ということにしておきたい論理式があれば真と仮定しておけばよいのだが、一階命題論理で「無数の論理式がすべて真」という知見は一気に表せない。と無数につなげた論理式を真と仮定したいところだが、無限の長さをもつ論理式は認められていない（25ページ）。
- 認められていないというか、論理式の定義が再帰的なので、無限の長さをもつ形式が論理式かどうか確かめようがない。
あるいは $P \equiv$ 「西暦2019年以降のすべての年は平成ではない」を真と仮定したところで、 $P, P_1, P_2, P_3, \cdots$ たちは互いに別々の赤の他人の原子命題なので、 $P_1, P_2, P_3, \cdots$ の真偽について何も示唆できていない。
このように、一階命題論理では「すべての $x$ について～」のような論理式から直観的に得られる知見を表現できていない。証明の妥当性を論じたいのに、数学の証明でよくつかう形式の直観を表現できていないのは具合が悪い。
これの解決に向けては、原子命題の中身に立ち入って分解するしかない。例えば $P_1$ は、「西暦2019年は平成ではない」のように名前 $a$ と述語 $F$ からなる $P_1=F(a)$ とする。さらに、 $\forall$ や $\exists$ といった量化子を導入し、「すべての $x$ について $F(x)$ 」「ある $x$ が存在して $F(x)$ 」のような論理式をそれぞれ $\forall x(F(x)), \; \exists x(F(x))$ と表すことにする。

一階述語論理の統語論

一階述語論理の述語は項という形式を $n$ 個取る。
以下の形式を満たさないものは一回述語論理の論理式ではない。
命題記号が基本述語になった点と、量化論理式が加わった点が一階命題論理と異なる。

一階述語論理における項 $\tau$	$a, \; x,$ 　名前は項、変項も項 $f(a_1, a_2, x_1, x_2, x_3), \; g(f(a_1, a_2, x_1, x_2, x_3), a_3, x_4)$ 　項を $n$ 項演算子に入れても項
一階述語論理における論理式	$\theta(\tau_1, \cdots, \tau_n),$ 　項を $n$ 項述語に入れたら論理式（基本述語） $\rho(\varphi_1, \cdots, \varphi_n),$ 　論理式を $n$ 項真理関数に入れても論理式（複合論理式） $\forall \xi \varphi, \; \exists \xi \varphi$ 　量化子 + 変項 + 論理式は論理式（量化論理式）

量化子により、一回命題論理ではそれ以上分析しようがなかった命題が、もっと細かい要素からかける。
- 例： 5は素数である（＝5は1ではない自然数であって、5を割り切れる自然数は1と5のみである）。
  $(5 \in \mathbb{N}) \land \lnot (5 = 1) \land \forall x \biggl( (x \in \mathbb{N}) \land \exists a \Bigl( (a \in \mathbb{N}) \land (x \times a = 5) \to (x = 1) \lor (x = 5) \Bigr) \biggr)$
量化論理式の部分論理式の集合には、束縛変項 $\xi$ に任意の項を代入したものが含まれるので（89ページ）、（任意の項が可算個あれば）部分論理式の集合の元の個数が可算個になりそう。

Q：記号集合 $\mathcal{A}=\{ (, \; ), \; ,, \; {\rm true}, \; {\rm false}, \; \lnot, \; \land, \; \lor, \; \to, \; \leftrightarrow, \; \forall, \; \exists, \; a_1, \; x_1, \; f_1, \; F_1, \; a_2, \; x_2, \; f_2, \; F_2, \; \cdots \}$ のもとでの一階述語論理の項と論理式全体に自然数のインデックスをふることはできるでしょうか。
A：できる。 $\mathcal{A}$ が可算集合でもOK。以下のように記号列 $s_1 s_2 \cdots s_n$ に自然数を対応させる写像がつくれる。
ただし ${\rm Pr}(n)$ は $n$ 番目の素数、 $i(s)$ は記号 $s$ の記号集合 $\mathcal{A}$ 内でのインデックスとする。
　　　 $g(s_1 s_2 \cdots s_n) = {\Pr}(1)^{i(s_1)} \times {\Pr}(2)^{i(s_2)} \times \cdots {\Pr}(n)^{i(s_n)}$ 　 $s_1 s_2 \cdots s_n$ のゲーデル数

練習問題5.15　一部略。

どの自然数にも、それより大きな自然数が存在する。
$\forall x \biggl( (x \in \mathbb{N}) \to \exists y \Bigl( (y \in \mathbb{N}) \land (x < y) \Bigr) \biggr)$
数列は発散する。
$\forall \varepsilon \biggl( (\varepsilon \in \mathbb{R}^+) \to \exists n_0 \Bigl( (n_0 \in \mathbb{N}) \land \forall n \bigl( (n_0 < n) \to (|\alpha - a_n| < \varepsilon) \bigr) \Bigr) \biggr)$
$\forall \varepsilon \biggl( (\varepsilon \in \mathbb{R}^+) \to \exists n_0 \Bigl( (n_0 \in \mathbb{N}) \land \forall n \bigl( (n_0 < n) \to (|\alpha - a_n| < \varepsilon) \bigr) \Bigr) \biggr)$
- 上記のどちらでもよい。緑色の部分は「数列 $(a_n)_{n \in \mathbb{N}}$ は $\alpha$ に収束する」。
  上の回答は「どの $\alpha$ にも収束しない」。下の解答は「ある $\alpha$ に収束するということはない」。

練習問題5.20　論理式から自由変項の集合と束縛変項の集合を抜き出す問題。一部略。

${\rm fv} \bigl( F(x, a, f(x)) \bigr) = {\rm fv} (x) \cup {\rm fv} (a) \cup {\rm fv} \bigl(f(x) \bigr) = \{ x \} \cup \{\} \cup {\rm fv} (x) = \{x\}$
${\rm bv} \bigl( F(x, a, f(x)) \bigr) = {\rm bv} (x) \cup {\rm bv} (a) \cup {\rm bv} \bigl(f(x) \bigr) = \{\} \cup \{\} \cup {\rm bv} (x) = \{\}$
${\rm fv} \bigl( \exists x \forall y F(y, x) \land \forall x \exists z F(z, y) \bigr) = {\rm fv} \bigl( \exists x \forall y F(y, x) \bigr) \cup {\rm fv} \bigl( \forall x \exists z F(z, y) \bigr)$
　　　 $= \Bigl( {\rm fv} \bigl( \forall y F(y, x) \bigr) - \{x\} \Bigr) \cup \Bigl( {\rm fv} \bigl( \exists z F(z, y) \bigr) - \{x\} \Bigr)$
　　　 $= \Bigl( \bigl( \{y, x\} - \{y\} \bigr) - \{x\} \Bigr) \cup \Bigl( \bigl( \{z, y\} - \{z\} \bigr) - \{x\} \Bigr) = \{\} \cup \{y\} = \{y\}$
${\rm bv} \bigl( \exists x \forall y F(y, x) \land \forall x \exists z F(z, y) \bigr) = {\rm bv} \bigl( \exists x \forall y F(y, x) \bigr) \cup {\rm bv} \bigl( \forall x \exists z F(z, y) \bigr)$
　　　 $= \Bigl( {\rm bv} \bigl( \forall y F(y, x) \bigr) \cup \{x\} \Bigr) \cup \Bigl( {\rm bv} \bigl( \exists z F(z, y) \bigr) \cup \{x\} \Bigr)$
　　　 $= \Bigl( \bigl( \{\} \cup \{y\} \bigr) \cup \{x\} \Bigr) \cup \Bigl( \bigl( \{\} \cup \{z\} \bigr) \cup \{x\} \Bigr) = \{x, y\} \cup \{x, z\} = \{x, y, z\}$

練習問題5.27　変項への代入の問題。これでいいのかな。

$(\forall x (F(f(x),y)))[y/x] = \forall x (F(f(x),y))$ 　 $x$ が束縛変項なので $x$ には代入できないパターン。
$(\forall y (F(f(x),y)))[z/x] = \forall y (F(f(z),y))$ 　 $y$ が束縛変項なので $x$ には $y$ が入っていない項は代入できる。
$(\forall x (F(f(y),z)))[y/x] = \forall x (F(f(y),z))$ 　 $x$ が束縛変項なので $x$ には代入できないパターン。
$(\forall y (F(f(y),z)))[y/x] = \forall y (F(f(y),z))$ 　 $x$ に代入しようとしても $x$ がない…。
$(\forall y (F(f(y),z)))[z/x] = \forall y (F(f(y),z))$ 　 $x$ に代入しようとしても $x$ がない…。
$(\forall y (F(f(x),y)))[y/x] = (\forall v (F(f(x),v)))[y/x] = \forall v (F(f(y),v))$ 　束縛変項を別の変項に回避するパターン。

練習問題5.30　項から部分項を抜き出す問題

${\rm Sub}\bigl( (1 + 2) \times ( x + (1 \times 2)) \bigr) = {\rm Sub}\bigl( 1 + 2 \bigr) \cup {\rm Sub}\bigl( x + (1 \times 2) \bigr) = \{1, 2, x\}$

練習問題5.32　面倒なので略。

練習問題5.36　面倒なので略。

練習問題5.39　面倒なので略。

練習問題5.40

任意の変項 $\xi,$ 項 $\tau, \, \sigma$ について以下が成り立つことを示せ。
${\rm fv}(\sigma [ \tau / \xi ])=\begin{cases} ({\rm fv}(\sigma) - \{ \xi \}) \cup {\rm fv}(\tau) & (\xi \in {\rm fv}(\sigma)) \\ {\rm fv}(\sigma) & (\xi \notin {\rm fv}(\sigma)) \end{cases}$

項 $\sigma$ の深さ $d$ に関する帰納法で証明する。

のとき：以下より、成り立つ。
- $\sigma$ が名前 $\alpha$ のとき： $\xi \notin {\rm fv}(\sigma) = \{\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\alpha [ \tau / \xi ])={\rm fv}(\alpha)={\rm fv}(\sigma)$
- $\sigma$ が変項 $\xi$ のとき： $\xi \in {\rm fv}(\sigma) = \{\xi\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\xi [ \tau / \xi ])={\rm fv}(\tau)=({\rm fv}(\sigma) - \{\xi\}) \cup {\rm fv}(\tau)$
- $\sigma$ が変項 $\zeta \neq \xi$ のとき： $\xi \notin {\rm fv}(\sigma) = \{\zeta\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\zeta [ \tau / \xi ])={\rm fv}(\zeta)={\rm fv}(\sigma)$
$1 < d$ のとき：深さ $d$ 未満の項 $\sigma$ については問題の式が成り立つと仮定する。
深さ $d$ の項 $\sigma$ については、 $\sigma = o(\sigma_1, \cdots, \sigma_n)$ とすると、
　　　 ${\rm fv}(\sigma)={\rm fv}(o(\sigma_1, \cdots, \sigma_n))={\rm fv}(\sigma_1) \cup \cdots \cup {\rm fv}(\sigma_n)$
　　　 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(o(\sigma_1, \cdots, \sigma_n) [ \tau / \xi ])={\rm fv}(\sigma_1 [ \tau / \xi ]) \cup \cdots \cup {\rm fv}(\sigma_n [ \tau / \xi ])$
${\rm fv}(\sigma_1), \cdots , {\rm fv}(\sigma_n)$ のいずれにも $\xi$ が含まれていないなら、 $\xi \notin {\rm fv}(\sigma)$ で、
　　　 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\sigma_1 [ \tau / \xi ]) \cup \cdots \cup {\rm fv}(\sigma_n [ \tau / \xi ])={\rm fv}(\sigma_1) \cup \cdots \cup {\rm fv}(\sigma_n)={\rm fv}(\sigma)$
${\rm fv}(\sigma_1), \cdots , {\rm fv}(\sigma_n)$ のいずれかに $\xi$ が含まれているなら（最初の $k$ 個としてもよい）、 $\xi \in {\rm fv}(\sigma)$ で、
　　　 ${\rm fv}(\sigma [ \tau / \xi ])=({\rm fv}(\sigma_1) - \{ \xi \}) \cup \cdots \cup ({\rm fv}(\sigma_k) - \{ \xi \}) \cup {\rm fv}(\sigma_{k+1}) \cup \cdots \cup {\rm fv}(\sigma_n) \cup {\rm fv}(\tau)$
　　　　　　　　 $\; =({\rm fv}(\sigma)-\{ \xi \}) \cup {\rm fv}(\tau)$

練習問題5.41　面倒なので略。

練習問題5.43　面倒なので略。