而して

ノートとかメモとか。

融合原理の健全性と完全性

真偽値の変数  x, およびその否定  \overline{x}リテラルという。リテラル, およびリテラル論理和  \lor で繋げた論理式をという。さらに, 節, および節を論理積  \land で繋げた論理式を節形式という。例えば, 

変数  \{x_1, \dots, x_k\} からなる節形式  \phi があるとき, 写像  \{ x_1, \dots, x_k \} \to \{0,1\} \phi割当という。どんな割当についても真となる節形式  \phi恒真であるという。また,  \phi が真となるような割当が存在するとき, 節形式  \phi充足可能であるという。例えば,

  • 節形式  x_1 \lor \overline{x_1} は恒真である。
  • 節形式  (\overline{x_1} \lor \overline{x_3}) \land (\overline{x_1} \lor x_2 \lor x_3) \land (\overline{x_2} \lor x_3) は充足可能である。実際,  x_2 \mapsto 1,  x_3 \mapsto 1,  x_1 \mapsto 0 という割当は  \phi を充足する。
  • しかし, 節形式  (x_1 \lor \overline{x_2}) \land \overline{x_1} \land x_2 は充足可能でない。後ろの二つのリテラルをいずれも真にするためには,  x_1 \mapsto 0,  x_2 \mapsto 1 とする他ないが, すると  x_1 \lor \overline{x_2} 0 となってしまう故。このように充足可能でない, すなわち充足不可能な節形式が存在する。

ある節形式が充足可能かどうかを判定する問題を, 節形式の充足可能性問題  \textit{CNF-SAT} という。これは理論と実用の両面から重要な問題として広く知られている。融合原理は, この問題を解くための論拠の一つとして知られる。

融合とは, 二つの節  x \lor \cdots_{\,1} \overline{x} \lor \cdots_{\,2} から, 節  \cdots_{\,1} \lor \cdots_{\,2} を作ることをいう。次の命題は明らか。

[命題1]節形式  \phi の二つの節  C = x \lor \cdots_{\,1},  C' = \overline{x} \lor \cdots_{\,2} を融合して  \varphi = \cdots_{\,1} \lor \cdots_{\,2} を作ったとき, 同じ割当  \sigma C \land C' \varphi を充足できる。すなわち, 

 \forall \sigma.  \sigma C \land C' を充足する  \iff  \sigma \varphi を充足する.

いま, 節形式  \phi = C_1 \land \dots \land C_m が与えられたとして, 次の手続き RES を繰り返す:

(1)節形式  \phi から  C_i = x \lor \cdots_{\,i} C_j = \overline{x} \lor \cdots_{\,j} を選んで( i = j でもよい), これらを融合し  C = \cdots_{\,i} \lor \cdots_{\,j} を作る。なお, 融合後の節  C に重複するリテラルがあればひとつだけ残す。また,

  •  C \in \phi, もしくは
  • あるリテラル  x について  x \overline{x} のどちらも  C に含まれている

ならば融合失敗として, 融合を選び直す。どのように融合を選んでも失敗するなら文字列 "SAT" を出力して停止する。うまく融合を選べたら(2)へ。

(2)もし, 節  C が空節  \{\} ならば, 文字列 "UNSAT" を出力して停止する。そうでなければ, 節  C \phi に加えた節を, 改めて  \phi と更新して(1)へ。

なお, この手続き RES は必ず停止する。なぜなら, この手続きは  \phi C \notin \phi となる新しい節  C を加えていくが, この新しい節の種類は高々有限個しか存在しないからである。実際, 節形式  \phi がもともと  k 種類の変数でできているなら, 節の種類はぜんぶで  \sum _ {r = 0} ^ {k} { _{k}\text{C}_{r} 2^r} (= 3^k) 個となって有限である。

この記事では, この手続き RES \textit{CNF-SAT} を決定すること, すなわち, 節形式  \phi を入力とした RES の出力について,

  • (健全性) RES が "UNSAT" を出力するならば,  \phi は充足不可能であり, 
  • (完全性)  \phi が充足不可能ならば, RES は "UNSAT" を出力する, 

ことを証明する。

(証明)先の[命題1]から, RES における  \phi の更新前と更新後で充足同値が保たれる。すなわち, 更新前の  \phi が充足可能であることと, 更新後の  \phi が充足可能であることは同値である。したがって, RES が停止する直前の  \phi について主張を証明すれば, 入力の  \phi についても同じ主張がしたがう。

健全性のほうがたやすい。 RES が "UNSAT" を出力するということは, 空節  \{\} が導かれたということになり, この空節を導いた節形式  \phi の二つの節  C_i, C_j が存在する。あるリテラル  x について  C_i = x,  C_j = \overline{x} としてよい。すると  \phi = \cdots \land x \land \cdots \land \overline{x} \land \cdots とかけるが,  x \overline{x} のどちらか一方は必ず偽だから, この  \phi は充足不可能である。

完全性については対偶を示す。すなわち, 次の主張:

RES が "SAT" を出力するならば,  \phi は充足可能である

を,  \phi に含まれる変数の種類  k に関する帰納法で示す。

まず  k = 1 として, この変数を  x とかけば, 論理的に  \phi は ①  x, ②  \overline{x}, ③  x \land \overline{x} の三通りに限られる。①なら  x \mapsto 1, ②なら  x \mapsto 0 とすれば  \phi を充足できる。そして③は起こり得ない;この  \phi からは空節を導けるので, RES が "SAT" を出力するという仮定に反するからである。よって,  \phi は充足可能である。

次に, RES が "SAT" を出力する直前の  \phi について,  \phi x_1, \dots, x_k からなる節形式ならば,  \phi の節の形は次の三通りに分けられる( RES の定義から,  \phi の任意の節  C について,  x \overline{x} の両方が同じ節  C に現れる場合は除かれることに注意):

  1.  K_i^1 = x_1 \lor \varphi_{i}(x_2, \dots, x_k),
  2.  K_j^2 = \overline{x_1} \lor \psi_{j}(x_2, \dots, x_k)
  3.  K_l^3 = \xi_{l}(x_2, \dots, x_k).

以下,  \phi を充足する割当  \sigma を構成する。すなわち:

  • 2の形が現れない場合。まず, 3の形の節  K_l^3 のみによる節形式  \phi' を入力として RES を走らせると, 仮定からこの出力も "SAT" になるので(why?), 帰納法の仮定によってある割当 \sigma'\mathpunct{:} \{x_2,\dots,x_k\} \to \{0,1\} が存在してこの  \phi' を充足する。したがって,  \sigma = \sigma' \lbrack 1 / x_1 \rbrack, すなわち  x_1 \mapsto 1,  x_r \mapsto \sigma'(x_r)  (r = 2, \dots, k) とすれば,  \sigma \phi を充足する。
  • 1の形が現れない場合。上と同様にして示せる。
  • 1と2の形がどちらも現れる場合。このとき, やはり上と同様に, 3の形の節のみからなる節形式  \phi' を充足する割当  \sigma' をとれば, この割当のもとで ①  \forall i. \varphi_{i} = 1 または ②  \forall j. \psi_{j} = 1 が成立つ;背理法によって示す。ある  i, j がとれて  \varphi_{i} = 0 かつ  \psi_{j} = 0 だったとすれば,  K_i^1 K_j^2 の融合である  K = \varphi_i \lor \psi_j 0 となる. しかるに  \sigma' の作り方から, この融合による節  K \phi' に現れないことがわかる。ゆえに残る可能性はあるリテラル  x について  x \overline{x} がともに  K に含まれる場合, すなわち恒真である場合しかないが, これは  K 0 となったことに反する。よって, ① ならば  \sigma = \sigma'\lbrack 0/x_1\rbrack, ② ならば  \sigma = \sigma'\lbrack 1/x_1\rbrack とすれば,  \sigma \phi を充足する。

Setsのcoequalizer (Awodey, 3.5.11)

Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.

概要

集合  R から生成する最小の同値関係を  \langle R \rangle とかく.  f, g:A \rightrightarrows B のcoequalizerが,  R \triangleq \{ x \in A; f(x) = g(x) \} とするとき  B \overset{\pi}{\twoheadrightarrow} B / \langle R \rangle であることを示せ.

 R を包む最小の同値関係  \langle R \rangle

問にはさらに, この  \langle R \rangle

 \langle R \rangle \triangleq \bigcap \{ C \in B \times B; C\text{ is eq.rel. on }B\,\&\,C \supseteq R \}

と定めよ, とある. これは確かに,  R を包む  B 上の同値関係であって, かつそのなかで最小の集合である. このことを示しておく.

同値関係であること.

反射律. 任意に  x \in B をとる. いま任意に,  R を包む  B 上の同値関係  C をとると,  C の反射律から  (x,x) \in C となるから  (x,x) \in  \langle R \rangle.

対称律.  (x,y) \in  \langle R \rangle をとれば, 任意の  C について  (x,y) \in C となって,  C の対称律から  (y,x) \in C となる.  C は任意だったから  (y,x) \in \langle R \rangle.

推移律. 対称律と同様.

 R を包むこと.  x \in R とすれば, 任意の  C について  x \in R \subseteq C より  x \in C.  C は任意だったから  x \in \langle R \rangle.

最小であること. 任意に  C をとれば,  \langle R \rangle の定義から  \langle R \rangle \subseteq C.

よって示せた. しかしこの定義は今回の問で使いにくいと思うので, より構造の分かりやすいやり方でこの「最小の同値関係」を定めるのがよいだろう. すなわち,  \Delta_B \triangleq \{ (b,b); b\in B \}, かつ

 F(X) \triangleq \underline{\{ (y,x); (x,y) \in X \}}_{(1)} \cup \underline{\{ (x,z); (x,y), (y,z) \in X \}}_{(2)}

として  \langle R \rangle' \triangleq \bigcup _ {n \in \omega} F^n (R \cup \Delta_B) とする.

同値関係であること.

反射律. 任意に  x \in B をとれば  (x,x) \in R \cup \Delta_B \subseteq \langle R \rangle'.

対称律.  (x,y) \in  \langle R \rangle' をとれば, ある  n があって  (x,y) \in F^n (R \cup \Delta_B) となるので,  (1)より (y,x) \in F^{n+1} (R \cup \Delta_B) \subseteq \langle R \rangle'.

推移律. 対称律と同様.

 R を包むこと.  R \subseteq R \cup \Delta_B \subseteq \langle R \rangle' 故.

最小であること. いま任意に  R を包む  B 上の同値関係  C をとるとき, 任意の  n について

 F^n(R \cup \Delta_B) \subseteq C

となることを示せば十分. 帰納法で示す.  n = 0 なら明らか.  (x,y) \in F^{n+1}(R \cup \Delta_B) をとるとき,

 (x,y) F(F^n(R \cup \Delta_B)) (1)由来なら  (y,x) \in F^n(R\cup\Delta_B) \subseteq C で,  C の対称律から  (x,y) \in C.

 (x,y) (2)由来としても同様.

よって示せた. なお,  \langle R \rangle \langle R \rangle' は同じ集合となる(最小性から,  \langle R \rangle \langle R \rangle' よりも小さいので  \langle R \rangle \subseteq \langle R \rangle', 逆も同様). 以下,  \langle R \rangle' \langle R \rangle とかく.

(ところで,

 F(X) \triangleq \Delta_B \cup \{ (y,x); (x,y) \in X \} \cup \{ (x,z); (x,y), (y,z) \in X \}

として  \langle R \rangle' \triangleq \bigcup _ {n \in \omega} F^n (R) としてもよい. Why?)

解答

 \pi f = \pi g はたやすい(こうなるように作ったのだから). あとは  A \rightrightarrows B \overset{\varphi}{\rightarrow} S,  \varphi f = \varphi g なる  \varphi をとるとき  \varphi = \psi \pi と一意に分解できることを示せばよい. これには,  \psi: \lbrack z \rbrack \mapsto \varphi z と定めればよいが, この  \psi がwell-definedであることを示す部分が問題である. すなわち,  x, y \in \lbrack z \rbrack について  x \neq y でも  \varphi(x) = \varphi(y) か?

ここで先の  \langle R \rangle帰納的な定義が活きてくる.  (x,y) \in \langle R \rangle \Longrightarrow \varphi(x) = \varphi(y) をいうのに,  \forall n \in \omega. (x,y) \in F^n (R \cup \Delta_B) \Longrightarrow \varphi(x) = \varphi(y) をいえば十分だからである.

 n帰納法.  n = 0 のとき,  (x,y) \in \Delta_B なら自明で,  (x,y) \in R なら, 定義からある  a \in A がとれて  x = f(a), y = g(a) となって,  \varphi(x) = \varphi(f(a)) = \varphi(g(a)) = \varphi(y) を得る.  (x,y) \in F^{n+1}(R \cup \Delta_B) をとる.  (x,y) (1)由来なら  (y,x) \in F^n(R\cup \Delta_B) ゆえ  \varphi(y) = \varphi(x).  (2)由来なら, ある  z がとれて  (x,z), (z,y) \in F^n(R \cup \Delta_B) となり  \varphi(x) = \varphi(z) = \varphi(y).

一意性は, かかる分解  \varphi = \psi \pi = \psi' \pi があれば  \psi(\lbrack z \rbrack) = \psi\pi(z) = \psi' \pi(z) = \psi' (\lbrack z \rbrack) ゆえ  \psi = \psi', と示せる.

Principles of Model Checking: Lemma 3.27

Reference: Baier, Christel, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 2008.

Lemma 3.27の証明は, もう少し見通しよくできると思う。

Def.  \text{Start}(\hat{\sigma}) := \{\sigma \in (2 ^ {AP}) ^ {\omega};\,\hat{\sigma} \in \text{pref}(\sigma)\}. 直感的には  \text{Start}(\sigma) \hat{\sigma} を prefix にもつword  \sigma 全体の集合である. この記法から, LT property  P が safety property であるという定義は,

 (\forall \sigma \in (2 ^ {AP}) ^ {\omega} \backslash P)(\exists \hat{\sigma} \in \text{pref}(\sigma))(P \cap \text{Start}(\hat{\sigma}) = \emptyset)

とかける. また, 定義より

 \sigma \in \text{Start}(\hat{\sigma}) \iff \hat{\sigma} \in \text{pref}(\sigma).

Lemma.  P \cap \text{Start}(\hat{\sigma}) \neq \emptyset \iff (\exists \sigma \in P)(\hat{\sigma} \in \text{pref}(\sigma) ).

証明 (左辺) \iff  (\exists \sigma)(\sigma \in P \cap \text{Start}(\hat{\sigma}))  \iff  (\exists \sigma)(\sigma \in P \land \sigma \in \text{Start}(\hat{\sigma}))  \iff  (\exists \sigma)(\sigma \in P \land \hat{\sigma} \in \text{pref}(\sigma))  \iff(右辺).

 \text{closure}(P) = \{\sigma \in (2 ^ {AP}) ^ \omega;\,\text{pref}(\sigma) \subseteq \text{pref}(P)\} \text{cl}(P) と略記する. なお, ここに  \text{pref}(P) = \bigcup _ {\sigma \in P} \text{pref}(\sigma).

Lemma 3.27.  P is a safety property  \iff \text{cl}(P)=P.

証明  P \subseteq \text{cl}(P) は成立つから, 右辺は  \text{cl}(P) \subseteq P と同値である. いま,  (2 ^ {AP}) ^ \omega \backslash A A ^ {c} とかくことにすれば,

 P is safety

 \iff  (\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )(P \cap \text{Start}(\hat{\sigma}) = \emptyset)

 \iff  (\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )(\forall \tilde{\sigma} \in P)(\hat{\sigma} \notin \text{pref}(\tilde{\sigma}) )

 \iff   (\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma) )\left( \hat{\sigma} \notin \bigcup _ {\tilde{\sigma} \in P} {\text{pref}(\tilde{\sigma})} \right)

 \iff   (\forall \sigma \in P ^ {c})(\exists \hat{\sigma} \in \text{pref}(\sigma))(\hat{\sigma} \notin \text{pref}(P))

 \iff  (\forall \sigma \in P ^ {c})(\text{pref}(\sigma) \nsubseteq \text{pref}(P))

 \iff  P ^ {c} \subseteq \text{cl}(P) ^ {c}.

が従う. 最右辺は  \text{cl}(P) \subseteq P と同値.

the epis among posets are the surjections (Awodey, 2.8.9)

Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.

解答にsurjection ⇒ epi の証明しかなかったので, epi ⇒ surjection 側のメモをしておく(解答はおそらくepi ⇒ surjection を not epi ⇒ not surjection で取り違えている;つまり、解答はsurjection ⇒ epiの証明を二度与えていた)。この問題は、epi ⇒ surjection が本質的なので残念だった。

問題:objectがposetで, arrowがmonotone function(二つのposet  (P, \leq _ {P}), (Q, \leq _ {Q})に関する集合間の写像  m:\,P \rightarrow Q であって,  \forall a, b \in P\ \text{s.t.}\ a \leq _ {P} b ならば  m(a) \leq _ {Q} m(b) を満たすもの;単調関数)であるようなcategory  \mathbf{Pos} 上で, arrow  f がepicならばsurjective (on elements)か?

この問題の意義のために, 考えているcategoryが  \mathbf{Sets} の場合の epi ⇒ surjective の証明を書くと次のようになる:

(証明)arrow つまり function  f:\,A \rightarrow B がnot surjectiveとすると  \exists b \in B\ \text{s.t.}\ b \notin f(A). いま  \mathbf{2} = \{0,1\} へのarrows  g, h:\,B \rightarrow \mathbf{2} として,  g = 0 _ {\mathbf{2}}! つまり  x \mapsto 0 および  h(x) = 1 \ \text{iff}\ x = b x = b だけ  1 をとって,  x \neq b なら  0)とすれば  g(b) \neq h(b) だから  g \neq h であるが,  x \neq b なら  g(x) = h(x) だから  gf = hf となって,  f はnot epic.

対偶をとり, not surjectiveと仮定して得られる  b \in B \backslash f(A) を元手に反例を構成していく流れで,  g, h b を入力したときだけ値が異なるように作ることでうまくいく。このように  \mathbf{Sets} なら反例が作りやすいのだが,  \mathbf{Pos} では上の証明の  g, h をmonotoneであるように取る必要があるため, 少し工夫を凝らす。

(証明)arrow  f:\, (A, \leq _ {A}) \rightarrow (B, \leq _ {B}) がnot surjectiveとすると  \exists b \in B\ \text{s.t.}\ b \notin f(A). いま  (\mathbf{2}, \leq) (なお  \leq := \{(0,0),(0,1),(1,1)\})へのarrows  \varphi, \psi:\,(B, \leq _ {B}) \rightarrow (\mathbf{2}, \leq) を以下のように定める(ここからがこの問題の意義):

 B _ {b} = \{x;\,x \leq _ {B} b\} とすると  b \in B _ {b}. このもとで  \varphi(x) = 0\ \text{iff}\ x \in B _ {b} および  \psi(x) = 0 \ \text{iff}\ x \in B _ {b} \backslash \{b\} とおく( b 以下/未満なら  0 へ, そうでなければ  1 へ飛ぶようにしてある;そう考えればこれはmonotoneにみえる). 実際にこれらはmonotoneか?

 x \leq _ {B} y なる  x, y \in B をとる.  \varphi(x) = 1 \land \varphi(y) = 0 とすると  x \notin B _ {b} かつ  y \in B _ {b} ゆえ  y \leq _ {Q} b だが  x \leq _ {Q} y だから  x \leq _ {Q} b となって  x \in B _ {b} で不合理. したがって  \varphi(x) \leq _ {Q} \varphi(y).

 \psi(x) = 1 \land \psi(y) = 0 とすると  x \notin B _ {b} \backslash \{b\} かつ  y \in B _ {b} \backslash \{b\} つまり  x \notin B _ {b} \lor x = b かつ  y \leq _ {Q} b \land y \neq b ゆえ  y \leq _ {Q} b x \leq _ {Q} y から  x \leq _ {Q} b より  x \in B _ {b} だから  x = b であるしかない. これを代入して  y \leq _ {Q} b かつ  b \leq _ {Q} y ゆえ  y = b が得られるが, これは  y \neq b に不合理. したがって  \psi(x) \leq _ {Q} \psi(y).

作り方から  \varphi(b) \neq \psi(b) ゆえ  \varphi \neq \psi. いま  x \neq b とする.  \varphi(x) = 0 なら  x \in B _ {b} ゆえ仮定を併せて  x \in B _ {b} \backslash \{b\} だから  \psi(x) = 0.  \varphi(x) = 1 なら  x \notin B _ {b} だから  x \notin B _ {b} \backslash \{b\} \psi(x) = 1. よって  x \neq b \Longrightarrow \varphi(x) = \psi(x) ゆえ  \varphi f = \psi f. よって  f はnot epic.

ブール代数

Def. Boolean algebra とは, poset  (B, \leq) と, その二つの要素  0, 1 \in B の組である. また,  B 上の二項演算 join:  a \lor b, meet:  a \land b, および単項演算 complementation:  \lnot b が定義されており, これらは以下の要請を満たす:

 a, b, c \in B とするとき,

 0 \leq a

 a \leq 1

 a \leq c and  b \leq c  \Longleftrightarrow  a \lor b \leq c

 c \leq a and  c \leq b  \Longleftrightarrow  c \leq a \land b

 a \leq \lnot b  \Longleftrightarrow  a \land b = 0

 \lnot \lnot a = a.

Remark. poset  (B, \leq) とは, 集合  B と,  B 上の半順序  \leq の組である.  B 上の半順序  \leq とは,  B 上の二項関係, つまり直積の部分集合  \leq\,\subseteq B \times B であって,  a, b, c \in B として, 以下の要請:

(反射律) a \leq a

(推移律) a \leq b and  b \leq c  \Longrightarrow  a \leq c

(反対称律) a \leq b and  b \leq a  \Longrightarrow  a= b

を満たすものである.

ブール代数と聞くと集合  \{0,1\}, もしくは  \{ \text{true}, \text{false} \} 上の演算を思い浮かべてしまうのだが, 順序を含めて拡張してもこれだけの公理でうまく定義できているので驚いた。ここから諸定理を示すのはそこまで難しくないが, ファインマン三角関数よろしく, 一通りまとめてみようと思う。

Lem.  \lor,  \land の基本公式)  a \leq a \lor b,  b \leq a \lor b および  a \land b \leq a,  a \land b \leq b.

proof.  \leq の反射律から  a \lor b \leq a \lor b だから, ③より  a \leq a \lor b and  b \leq a \lor b. 後者は④から従う.

Lem.  \lor,  \land の可換則)  a \lor b = b \lor a および  a \land b = b \land a.

proof. 基本公式より  b \leq a \lor b and  a \leq a \lor b が成り立つので, ③から  b \lor a \leq a \lor b. 同様にして( a, b を入れ替えると考えてもよい),  a \lor b \leq b \lor a.  \leq の反対称律から  a \lor b = b \lor a. 後者は④から従う.

Lem.  \lnot \leq の関係)  a \leq b  \Longleftrightarrow  \lnot b \leq \lnot a.

proof. ⑤⑥から  a \leq b  \Longleftrightarrow  a \leq \lnot \lnot b  \Longleftrightarrow  a \land \lnot b = 0.  \land の可換則からこれらは  \lnot b \land a = 0 と同値で, ⑤から  \lnot b \leq \lnot a と同値.

Lem. (De Morganの法則)  \lnot (a \lor b) = \lnot a \land \lnot b および  \lnot (a \land b) = \lnot a \lor \lnot b.

proof. 基本公式から  a \leq a \lor b より, 両辺で  \lnot をとり  \lnot (a \lor b) \leq \lnot a.  a, b を入れ替え, 可換則から  \lnot (a \lor b) \leq \lnot b. ④から  \lnot (a \lor b) \leq \lnot a \land \lnot b.

一方, 基本公式から  \lnot a \land \lnot b \leq \lnot a で, 両辺で  \lnot をとり⑥から  a = \lnot \lnot a \leq \lnot (\lnot a \land \lnot b). 同様に  b \leq \lnot (\lnot a \land \lnot b). ③から  a \lor b \leq \lnot (\lnot a \land \lnot b). 再び両辺で  \lnot をとって  \lnot a \land \lnot b \leq \lnot (a \lor b). よって  \leq の反対称律から結論の前者が従う. 後者は, 前者の  a, b が任意であることから,  a \lnot a に,  b \lnot b に置き換え  \lnot (\lnot a \lor \lnot b) = \lnot \lnot a \land \lnot \lnot b が得られるので, 両辺で  \lnot をとって⑥により(「二重否定」を除去することで)従う.

Lem. (無矛盾律排中律  a \land \lnot a = 0 および  a \lor \lnot a = \lnot 0.

proof. ⑤で  b = \lnot a とすると, ⑥から  a \leq \lnot \lnot a = a \leq の反射律から成立つので,  a \land \lnot a = 0. De Morganの法則と  \lor の可換則, および⑥から  \lnot (a \land \lnot a) = \lnot a \lor \lnot \lnot a = a \lor \lnot a = \lnot 0.

ex1.  0 \neq 1 として  \mathbf{2} = \{0,1\}. おなじみの二値集合である.

ここで  \leq の指定がないのは, もろもろの条件によって自然に定まるからである. すなわち, この集合がboolean algebraとなり得るように  \mathbf{2} 上の半順序  \leq\,\subseteq \mathbf{2} \times \mathbf{2} を定義する場合,  \leq が半順序であることから, 反射律より  (0,0), (1,1) \in\,\leq. また公理の要請①②から  (0,1) \in\,\leq. ここで  (1,0) \in\,\leq とすると  0 \leq 1 かつ  1 \leq 0 と反対称律から  0 = 1 となって仮定に反するので  (1,0) \notin\,\leq でなければならない. したがって,  \leq\,= \{(0,0),(0,1),(1,1)\} と一意に定まり, 逆にこの  \leq は半順序である.

また, 実は  \lnot 0 = 1 かつ  \lnot 1 = 0 であるしかない:⑤と \land の可換則から  a \leq \lnot b  \Longleftrightarrow  a \land b = 0  \Longleftrightarrow  b \land a = 0  \Longleftrightarrow  b \leq \lnot a だから, もし  \lnot c = c なる  c が存在すれば, 任意の  a について  a \leq \lnot a となり,  a \lnot a で置き換え⑥を使えば  \lnot a \leq \lnot \lnot a = a ゆえ, 任意の  a について  \lnot a = a が従う. しかるに, これにより先の同値は  a \leq b  \Longleftrightarrow  b \leq a とかけるので, 反対称律から任意の  a, b につき  a=b となり, これは  0 \neq 1 に反する. 従って, 任意の  c につき  \lnot c \neq c でなければならない.

つまり 0 \neq 1 として  \mathbf{2} = \{0,1\}」という言明だけで, 他の言及がなくとも, 半順序と単項演算  \lnot は自然に定まっているのである. 特に, 以上の流れから分かるように,  0 \neq 1 という点が本質的である.

いわゆる「真理値表」を作ってみよう.  \lnot は先に見たとおり.

 \land については⑤より  0 \land 0 = 0,  0 \land 1 = 1 \land 0 = 0. また  1 \leq 1 より, ④から  1 \leq 1 \land 1. 逆に②から  1 \land 1 \leq 1 ゆえ  1 \land 1 = 1.

 \lor についてはDe Morganの法則から, それぞれ  1 \lor 1 = 1,  1 \lor 0 = 0 \lor 1 = 1,  0 \lor 0 = 0 が従う.

ex2. 集合  X の冪集合  2 ^ {X}.  \leq\,=\,\subseteq,  0 = \emptyset,  1 = X,  \lor = \cup,  \land = \cap,  \lnot A = A ^ {c} = X \backslash A とすれば,  2 ^ X はboolean algebraとなる. 特に,  \mathbf{2} \mathbf{1} = \{\ast\} (一元集合)の冪集合とみなせる: \mathbf{2} \cong 2 ^ {\mathbf{1}}.

Reference. Awodey, S. (2010) Category Theory, Oxford: Oxford University Press, 2nd ed. 2011.

チェビシェフ多項式①

 c _ {k}(x)=\cos\left(k\cos ^ {-1}{x}\right) なる関数  c _ k:\,[-1,1] \rightarrow \mathbb{R} を考える  (k \in \mathbb{R})

同時に  s _ {k}:\,[-1,1] \rightarrow \mathbb{R},\,x \mapsto \sin\left(k\sin ^ {-1}{x}\right) を考え, 

 e _ k(x) = c _ {k} (x) + i s _ {k} (x)

を定めると, これは極形式になっているから, 

 e _ k(x) = (\cos\left(\cos ^ {-1}{x}\right)+i\sin\left(\cos ^ {-1}(x)\right)) ^ {k}
 = (x + i \sqrt{1-x ^ 2}) ^ {k}

となり, かつ  \overline{e _ k(x)} = (x - i \sqrt{1-x ^ 2}) ^ {k} だから, 

 c _ k(x) = \frac{e _ k(x) + \overline{e _ k(x)}}{2} = \frac{(x+\sqrt{x ^ 2 - 1}) ^ k + (x - \sqrt{x ^ 2 - 1}) ^ k}{2}

が従う。この右辺は  x \in \mathbb{R} \backslash [-1,1] でも実数値で定義される。分子を二項定理で展開すると, 二項係数を  (n,k) などと横向きに書けば,

 (x+\sqrt{x ^ 2 - 1}) ^ k + (x - \sqrt{x ^ 2 - 1}) ^ k
 = \sum _ {j = 0} ^ {k} (k,j) x ^ {k-j}(x ^ 2 - 1) ^ {j/2} + \sum _ {j = 0} ^ {k} (k,j) x ^ {k-j}(-1) ^ {j}(x ^ 2 - 1) ^ {j/2}

 = \sum _ {j = 0} ^ {k} {(k,j) x ^ {k-j} (1 + (-1) ^ {j}) (x ^ 2 - 1) ^ {j/2}}

 = \sum _ {j = 0 \\ \exists m,\,j = 2m} ^ {k} {(k,j) x ^ {k-j}(x ^ 2 - 1) ^ {m}}

となるから,  k 次実係数多項式である。これを  k 次のChebyshev多項式という。