記号論理入門
https://images-na.ssl-images-amazon.com/images/I/41hcMwe9CbL._SX354_BO1,204,203,200_.jpg
読書メモ.
第一章 論理記号による命題の表現法
命題とは，真偽値が決まっているもの．
変数を含む命題を，命題関数，と称する．
概念や条件といった言葉も全て「述語(predicate)」で表される．
$ F(x)のとき$ F()は述語．$ xは要素(element).
⇔ ∈ ∧ などの記号は命題結合記号．複数の命題を結合して一つの命題を生成できる．
集合
$ F(x)のとき，$ xは集合$ Fに属する．
$ e \in Fと$ F(e)は表記法の問題で，同じ命題を指す．
集合を要素として扱うこともできる．その時は$ G \subset Fのような表記法を用いる．
伝統的な論理学においては，ある<性質>と，その性質をもつもの全体からなる<集合>とを，同一の<概念>の2つの側面と考え，性質のことを，その概念の内包(intension), 集合のことを外延(extension)とよび，上記のことを
概念の内包と外延とは反対の方向に増減す
などと表現しました．
条件
$ \forall x (x \in F \to x \in G)は$ F \subset Gと同じ．
「すべてのFな人はGである」なら「FはGに含まれる」．
このときFはGの十分条件(sufficient condition)であり，GはFの必要条件(necessary condition)．
$ (*)$ \forall x(F(x) \Leftrightarrow G(x))は$ F = Gと同じ．
このときFはGの必要十分条件(necessary and sufficient condition).
ただし，$ =という記号については注意が必要
いまのわれわれは，<集合>と<もの>とを区別して考えているのですが...
そうして，<もの>一般について，$ =というものがあらかじめ定義されてしまっているようなときには，この$ (*)はもはやけっして自明ではなくなります．少なくとも，$ =の定義から明らか，というわけにはいかぬ場合が起こります．(略)
この$ (*)を集合に対する1つの公理と考え，それを外延性の公理(axiom of extensionality)とよびます．
外延性の公理が真である系においては，$ F = Gなら集合F,Gは全ての要素がどちらにも含まれる．
和集合の定義
$ \forall x[x \in F \cup G \Leftrightarrow (x \in F \lor x \in G)]
積集合の定義
$ \forall x[x \in F \cap G \Leftrightarrow (x \in F \land x \in G)]
補集合(または余集合complementary set)の定義
$ \lnot F
$ F^c
$ \forall x(x \in F^c \Leftrightarrow x \notin F)
ある命題関数(条件)を満たすもの全体からなる集合
$ \{x | F(x)\}
集合$ Fと同じ．集合の定義を示すときに便利
$ F = \{x | x > 0\}のように書ける
差集合の定義
$ F - G = F \cap G^c \equiv \{|x| x\in F \land x \notin G\}
命題結合記号の使用法に関する注意点
たとえば，2つの述語$ F, Gに対しての<FならばG>という命題をわれわれは
$ \forall x (F(x) \to G(x))
と書くことにしたのですが，時として，われわれは，この命題を単に
$ F \to G
と書きたいような衝動にかられることがあります．かく申す私も記号論理の専門家でありながら，このような記法を用いることがしばしばあります．しかしそれは，現在の記号論理における論理記号の使用法にかなうものではありません．(略）記号論理の枠内において
$ F \to G
という表現が用いられるとすれば，それは，$ Fと$ Gがともに命題であるときに限ります．
$ Fや$ Gが述語とか性質とかのときには，このような記法を用いません．
述語に対する演算子が未定義になるから，用いないのかな?nikezono.icon
述語や性質同士では，$ F + Gや$ F \cup Gなどが未定義．
関数なら，$ F+Gは$ \forall x ((F+G)(x) = (F(x) + G(x))とできるが，「男である」とかだと難しい．
集合と考えれば出来る．
集合と考えた場合，$ F\lor G, F \land G, \lnot Fは$ F \cup G, F \cap G, F^cと対応している
ので，命題結合記号はあまり使わない
しかし，$ \to については難しい議論を含む．
さて，$ \toに対しても，
$ \forall x ((F \to G)(x) \Leftrightarrow (F(x) \to G(x))
として，$ F \to Gというものを定義することができないわけではありません．しかし，この<$ F \to G> はけっして命題ではなく，ひとつの述語であることに注意していただきたいのです．(中略) $ Fや$ Gを述語とした場合，<$ F or $ G>とか<$ F and $ G>あるいは<not $ G>というのは，それらはみな，それぞれ1つの述語として考えることもできるのに，<$ Fならば$ G>というのだけはかならず命題として理解され，それは，日本語(あるいは，日常語)の言語感覚として，ほとんど述語とは考えられないのであります．ちょうどこれは，集合$ F, Gに対して，
$ F \cup G, $ F \cap G, $ F^c
がすべて集合であるのに，
$ F \subset G
だけは命題である，というのに相当しているのでしょう．
以上の言語感覚上の理由から，この本では$ F \to Gといった表記はされない．$ F, Gが述語なのか集合なのか不明瞭になるからである．
多変数の命題関係
2変数の命題関数を関係と呼ぶ．
$ F(x, y)のことを$ xFyと書くこともある．
3変数の命題関数を3項関係と呼ぶ．
n変数の命題関数をn項関係と呼ぶ．
1項関係とは<性質>のことで，0項関係とは，それは<命題>ということになります．
n変数の命題関数はn変数の述語と呼ばれる．以後は「述語」を用いる．
要するに，<命題関数> とか<関係> とか<述語>という言葉は全て同義語とし，時に応じて適当に使い分けようというのです．
これが，$ \forall, \existsを研究する範囲を述語論理と呼ぶ理由．
これらの限量子はn変数を扱うため．
これに対して，$ \to, \land, \lor, \lnotだけを研究する範囲を命題論理という．
命題を主語と述語に分離し，主語を変数として考える必要がないから．
ある命題が真か偽かだけを考えれば良い．
命題論理は述語論理のサブセットとして扱うのが一般的．
$ \forall x \exists yと$ \exists x \forall yは別の命題を示す．
前者は「すべてのxについていずれかのyが存在する」後者は「いずれかのxについて全てのyが成り立つ」
$ \forall x \forall yと$ \forall y \forall xは同じ．
$ \exists x \exists yと$ \exists y \exists xも同じ．
これについては演繹の規則で表せる．
n変数の述語に限量子を適用すると，n-1変数の述語になる．
$ F(x,y,z)について$ \forall x F(x,y,z)とすると全てのxについて成立する2変数の述語になる．
0変数の述語 = 命題であることを思い出すと，以下の変換が出来る
$ F(x)は1変数の命題関数．「xがFの性質/条件であるか」
$ \forall x F(x)とすると0変数なので命題になる．「すべてのxはFである」
$ \forall x F(x,y)は1変数の命題関数．
$ \forall x \forall y F(x,y)とすると真偽の定まった命題となる．
限量子によって範囲が限定された変数は，実際には変数とは区別される．これを束縛変数と呼ぶ
束縛変数でない変数を自由変数とよぶ．
変数を含む命題
ここまで，真偽が確定しているものを命題とよび，それ以外は命題関数としてきた
しかしこれは実際的ではない
そこで，変数$ a_1, a_2, ..., a_n を含む命題を自由変数$ a_1, a_2, ..., a_nを含む命題とよぶ．
すなわち，「変数を含む命題」は成立する．
ここに含まれる自由変数は定数と考えるとよい．
変数を含む命題，たとえば，
$ ax^2 + bx +c >0
というのも，これを1つの命題の表現と考える限り，これは単にこれだけのものでしかありません．
しかし，もし$ xという変数に着目して，これを$ F(x)と表したとすれば，この$ Fは一つの命題関数ーまたは<述語>ーと考えられます．このように，<関数>とか<命題関数>とかいうものは，主としてわれわれの<態度>あるいは<心構え>というようなものに関係してきまるものであり，表現形式そのものから一意的に定まるものではありません．(中略)
でありますから
命題$ F(x)は，$ x以外の自由変数を含んでいるかもしれないし，また$ xという自由変数を含んでいないかもしれない
のであります．
「心の持ち方」とか「心構え」とか「態度」とかいう表現が連続していて辛いな...nikezono.icon
表記法によって一意に定まらない，というのは直感的に記号論理の存在意義から問題を感じる．
自由変数は定数でもあるし変数でもあるし，何でも良い
<自由変数>と名付けられた文字がそこにあるだけ
束縛変数は違う．束縛変数は範囲が限定されており，まさしく<変数>である．
<$ x=1は$ x^2 = 1となるための十分条件である>というとき$ xは変数である
これは記号論理で表記すると$ \forall x(x=1 \to x^2 = 1)であり，$ x = 1 \to x^2 = 1ではない
自由変数は，任意の値をとってもよいし，定数でもよい，命題関数に対する入力とは異なるもの，つまり命題の一部と考えればよい．
用例
aはbより大きい: $ a < b \equiv \exists x(a+b =b)
aはbで割り切れる: $ a | b \equiv \exists x (ax = b)
素数:$ Prim\ a \equiv \forall x(x|a \to (x=1 \lor x=a) )
ユークリッドの定理(素数は無限にある): $ \forall x \exists y(x < y \land Prim\ y)
無限集合$ F: $ \forall x \forall y(x < y \land y \in F)
ある集合が無限集合であるか，という命題は「述語の述語」なので第2階の述語にあたる．
第二章 演繹
規則から結論を導く論理
個々の事実から規則を導く帰納とは異なる
数学において論理といわれるとき常に演繹である
演繹において仮定と証明済みの公理をわけて考える．
仮定が含まれる演繹は推論という．
大前提(公理?)を用いて推論を行い，仮定を除去できる
仮定がすべて取り除かれた演繹を証明という．
たとえば$ A, A \to B, Bは演繹．命題$ Aから命題$ Bを導いている．
$ Aが真かつ $ A \to Bより$ Bも真，を構成仮言的三段論法という
これは$ \to を除去する論法である．
命題結合記号の導入・除去を通じて，記号論理の式を変換できる．これによって大前提から結論を導ける．
この論法によって，$ A が大前提であるなら，命題結合記号$ \to を除去し，$ Bを成立させられる．
他にも$ \land,\lorの導入/除去，$ \lnotの導入/除去についてもそれぞれ論法がある
たとえば以下は$ \lorの除去．
$ \underline{ A \lor B, A \to C, B \to C}
$ C
これを単純構成的両討論または「ジレンマ」と呼ぶ．
AまたはB...だが，どちらにせよ(どちらも真のときも)同じ結論が成立する，ということ
AもBもCの十分条件なので，AとBがどちらも偽であるならCを結論できない
「AでもBでもCは成り立つ」かつ大前提が「A」なら，「B」がなくとも「C」は単独で真となる命題である．
$ \lnotについて
否定を示す$ \lnot Aは論理的にどう導くのだろうか．
Aは間違っているという矛盾を示せばよい．
論理的な矛盾とは?
$ Aと$ \lnot Aとが同時に導かれること
$ Aを大前提としたとき$ \lnot Aが導かれること
と考えると循環論法が存在する
<否定> の定義には<矛盾> の概念が用いられ，<矛盾> の定義には<否定>という概念が用いられているからです．
確かに，$ \lnotは矛盾を意味していて，矛盾は$ \lnotを意味している，というのは困る．
これの明確な定義はあとでやるらしい
$ \forallについて
導入にあたっては，該当する変数がまったく任意でなければならない．つまり変数が自由変数でなければならない．
たとえば，$ F(x))が
$ a = x
を表しているならば，
$ F(a)すなわち $ a =a
は正しいでしょうが，
$ \forall x F(x)すなわち$ \forall x(a=x)
は一般には<もの>が2つ以上あれば正しくはないでしょう．
ですから，$ F(x)が$ aを含む場合には，$ F(a)が証明されたからといって，$ \forall xF(x)が証明されるというわけにはいきません．
除去にあたっては，任意のものであればよい．
導入例:
$ F(a): ソクラテスは死ぬ
$ \forall xF(x): $ xは死ぬ
$ xがまったく任意の性質/条件/集合なら，$ aのみをもって導入はできない
$ xが生物という大前提があれば除去できる
除去例:
$ \forall xF(x): $ xは死ぬ
$ F(t): $ tは死ぬ
任意の自由変数が死ぬ，という命題に変化する．
$ \existsについて
難しい．飛ばす
<矛盾>について
まず，否定の導入と除去に関する推論規則
$ \lnot導入:
$ (A)
$ \underline{\Rightarrow\!\Leftarrow}
$ \lnot A
latexが分からんので$ \Rightarrow\!\Leftarrowを矛盾とする
Aを仮定して矛盾が導かれるなら，$ \lnot Aを導入できる．
$ \lnot除去:
$ \underline{A, \lnot A}
$ \Rightarrow\!\Leftarrow
Aとnot Aがともに導かれたなら，矛盾記号を導き，否定を除去できる．
このことから否定は矛盾という概念によって成り立ち，矛盾もまた否定によって導かれる概念である．
つまり「否定ならば矛盾」「矛盾ならば否定」であり，$ \toの除去/導入規則のみで議論している．
これは循環論法的であり，"矛盾"の定義を説明できていない．
このため，論理体系に矛盾という概念を持ち込むのは批判の向きもあるようだ．
矛盾には「爆発律」とよばれるものがある．
$ I: ((A \lor B) \land \lnot B) \to Aという命題があるとする
「AまたはBで，かつ，Bでないなら，Aである」
これは言語感覚的には正しい命題と感じる
しかしここまでの論理だと，この命題$ Iは証明できない
演繹してみよう
$ \underline{B, B \to \Rightarrow\!\Leftarrow}: Bが真かつBならば矛盾という仮定をおく
$ \underline{B, \Rightarrow\!\Leftarrow}: つまりBが真という大前提で，Bと矛盾が存在する
$ \underline{B, \lnot B}: 否定の導入規則より，否定を導入できる．
$ \underline{A \lor B, \ }: $ \lorの導入規則(p43)より，Bが真なことから$ A \lor Bを導入できる
$ \underline{(A \lor B) \land \lnot B, \ \ \ (A \lor B) \land \lnot B \to A}: これで$ \toの除去規則まで持っていける
$ \underline{\ \ \ A\ \ \ } :Aが真であることを導ける．
$ \underline{\ \ \ B \to A\ \ \ } : $ \toの導入規則を適用する．Bを仮定してAが真なので$ B \to Aである
$ \underline{\ \ (B \to \Rightarrow\!\Leftarrow) \to (B \to A) \ \ }: もう一度$ \toの導入規則．$ Bならば矛盾という仮定から$ B \to Aを導ける．
もともと関係がなかったAとBについて，$ Bが成り立つなら$ Aも成り立つ，という論理を成立させてしまった．
原因は「$ Bでない，かつ，$ Bである」という仮定(大前提/公理)を置いたことにある．
このことより，
矛盾を導く命題からは任意の命題が導かれる．
任意の命題を矛盾命題に置き換え可能であり，なんでもありとなる．
すなわち，
<矛盾> とは，それから任意の命題が導かれるものである．
これが矛盾/否定の定理．
矛盾を含む命題を論理体系として許容しないことを矛盾律(無矛盾律)という．
矛盾律: $ \neg (A\wedge \neg A)
矛盾律は証明不可能．
矛盾律と言う言葉はいろいろな場所でいろいろな使われ方をしている．
先ほどの「否定」の導入・除去原則がもっともミニマルで正確だと思う(そこから他の表記を導ける)
否定の導入・除去原則からいえるのは，以下
矛盾に関する推論規則:
$ \underline{\ \ \ \ \Rightarrow\!\Leftarrow\ \ \ \ }
$ \ \ \ \ \ A \ \ \ \
これによって「矛盾からは任意の命題を導ける」ことを明に示す．
矛盾律なしで，これまで扱った命題結合記号のみを使う論理を最小論理という．
最小論理に矛盾律を含むものを直観論理とよぶ．
爆発律の扱いはともかくとして，矛盾を許容する論理体系を矛盾許容論理という．
排中律について
排中律: $ A \lor \lnot A
Aかnot Aのどちらか，あるいはどちらも真
矛盾律と組み合わせると，どちらも真の(つまり矛盾がある)とき，どちらか片方が成り立っていることを示せる
つまり言い換えると，重要なのは，「どちらも偽」が成立しなくなることかな．nikezono.icon
これは日常の言語感覚からすると成立する．
これは背理法(帰謬法)の基礎を与えているもの．
1. $ \lnot A \to \Rightarrow\!\Leftarrowまで結論したとする
2. 否定の導入原則より，$ \lnot A \to \Rightarrow\!\Leftarrowは$ \lnot \lnot Aである
3. ここまでの結論より，$ \lnot A, \lnot \lnot A．
4. 否定の除去原則より， $ \Rightarrow\!\Leftarrow
5. 矛盾の推論規則より，$ A
6. 排中律を足して，$ (A \lor \lnot A), \ \ A
7. ここで$ \lor 除去規則を使って$ A
8. つまりこれは$ \lnot \lnot A \to A．
これを二重否定の除去の法則という．
!!A == Aが成立するのは二重否定の除去の法則が存在する論理体系だけである．
排中律，二重否定の除去は証明不可能．
というより，↑の5.でやっている矛盾の推論規則がぶっ飛んでいる気がする．
矛盾からはあらゆる命題が導かれることから，$ \lnot Aで矛盾しているとき，その矛盾から$ Aを導く，という飛び級感
つまり背理法は爆発律を使って任意の命題を導いている．
矛盾律・爆発律が証明不可能なのだから，それをベースラインにした排中律も背理法も証明不可能で当然．
よって排中律と二重否定の除去を公理として扱う．
この論理体系を古典論理とよぶ．
最小論理 ⊂ 直観論理 ⊂ 古典論理
第3章 真理値
これまで命題ならびに結合された命題については，仮定を用いて演繹を進めてきた．
命題の真偽は議論の範疇外にあったため，演繹を用いて論理式を変換することはできたが，WIP
命題の真偽を表すために真理値という記号を導入する．
正しい命題(true): $ \top
誤っている命題(false): $ \bot
true，falseという概念の定義を論じると哲学に踏み込む．
よって，真とは何か，偽とは何かはおいといて，こういう公理をいったんおいてみる．
(I) 第2章で述べた演繹法で証明される命題の真理値は$ \topである．
これは，演繹法によって証明される命題はすべて正しい，ということでもあります．
(II) 2つの命題$ A および$ A \to Bの真理値がともに$ \topであるならば，$ Bという命題の真理値も$ \topである．
同じことを言っている気もするが，命題結合記号$ \toは命題の真理値に関する演算子である，と読み替えられる
(III) $ Aの否定 $ \lnot Aの真理値が$ \topのとき，および，そのときにかぎって，$ Aの真理値は$ \botである．
これは排中律+無矛盾律と同義かな...つまり最小論理/直観論理では真理値という概念は定義出来ない．
(I)と(II)はそれぞれtrueつまり$ \topについての公理であり，(III)が唯一$ \botについて規定している．
この3つの条件は「あらゆる命題に真理値がある」ことを意味しない．
「(I)(II)(III)によって一部の命題について真理値を定義できる」ことを意味する．
真理値が定かでない命題(たとえば変数を含むもの)も存在する．
真理値と(i)(ii)(iii)を用いれば，複数の命題を命題結合記号によって結合した命題についても，議論できる．
一旦，命題結合記号を用いた命題(ex. $ A \to B)を忘れ，入力となったそれぞれの命題の真偽に応じて真理値が決定する．
N個の命題が存在する場合それぞれの入力の真偽によって$ 2^nの組み合わせをとりえる．
この各命題の真偽値の入力が定まれば，$ \to, \lor, \landなどの命題結合記号を用いた結合命題の真偽値も定まる．
<真理値>と<演繹>の接触点は，(中略)，基本性質の(I)のみであります．
しかも，上記の真理表を得るに要しました演繹は全て直観主義論理に属するものばかりで，排中律は一度も用いませんでした． のみならず，$ \botに関する推論を用いたのもただの一度，(中略． $ \toの真理表を得るために用いた．)
つまり，矛盾命題$ \botの性質をぜひとも必要とするのは$ A, B, A \to BでA，Bの真理値が$ \botであるとき，$ A \to Bが$ \topであることを導くためのみ．
他はすべて最小論理の範囲で十分であるのであります． 限量子と真理値
真理値というものとの関連において$ \forallや$ \existsの性質を調べようとすると，これまでとは全く異なった様相が現れます．その最も大きな理由といえば，$ \lnot, \to, \lor, \landという命題結合記号がすべて，与えられた1つまたは2つの命題から新しい命題を作り出す演算を表しているのに反し，$ \forall xおよび$ \exists xという演算が命題関数$ F(x)に作用して新しい命題$ \forall x F(x)および$ \exists xF(x)を作るものと考えられる，というところにあるのです． 新しい命題をつくる，というところがポイント．
命題関数$ F(x)というものを真理値との関連において調べる場合，$ F(x)に真($ \top)あるいは偽($ \bot)というような1つの値を対応させるのは一般論として適当ではありません．
一般論として，ということは，これが適当になる公理系もあるのか?
最も自然な考え方としては，$ F(x)に対応しているのは，真理値を関数値としてもつ$ xの関数である，とすべきでありましょう．
さて，そのような関数を考えるとすれば，是非とも，その独立変数$ xの変域ーそれを対象領域とよびますがーを明示しなければならなくなります． 対象領域が有限か無限か，が重要．
有限なら:
$ \forall xF(x)は$ F(x_1) \land F(x_2) \land F(x_3)...というふうな命題結合記号を生成するものと考えられる.
$ \existsについても同じ
無限なら:
↑のような処理は不可能．真理表が無限に長い表となる．
対象領域が無限，ということは，あらゆる個々の対象領域を包含する，ということであり，そこで使われる論理は超越的な論法となる． 真理値を用いた記号論理の限界はここにある．真理値は対象領域が無限であるとき用いることができない．
第4章 トートロジー
$ A \lor \lnot A: 排中律
$ (( A \to B ) \to A ) \to A: パースの法則(否定を使わない排中律のようなものらしい) BがなんであれAが真ならば$ A \to Aになる
Aが偽であっても$ (A \to B)がなんであれ$ \bot \to \botになりこれも真
つまりBがなんであれ途中でAを結論した時点で$ A \to Aか$ \lnot A \to \lnot Aに結論される
そこに現れる命題の真理値が何であっても，その真理値がつねに$ \topとなるものを，われわれは常に真な命題結合(immer richtige Aussagenverbindung)またはトートロジー(tautology, 同語反復)とよびます．
以下は全てトートロジー．
すなわち$ A, Bが真であろうと偽であろうと，以下の結合命題の真理値は常に真．
$ A \to A# 同一律
$ \lnot (A \land \lnot A) # (無)矛盾律
$ (\lnot \lnot A) \leftrightarrow A # 二重否定の除去
$ \lnot (A \lor B) \leftrightarrow (\lnot A \land \lnot B) # ド・モルガンの法則 $ \lnot (A \land B) \leftrightarrow \lnot A \lor \lnot B # ド・モルガンの法則 $ (A \to B) \leftrightarrow (\lnot A \lor B)
Aが真でBが偽つまり$ A \land \lnot Bを仮定すると左の命題が偽．右も偽なので$ \bot \to \botになる
それ以外の仮定では全て$ A \to Bは真．$ (\lnot A \lor B)も真．
直観論理では，Aを偽と仮定すると爆発律より任意の命題を真と導けるので，Aが偽なら$ (A \to B)は真．
もしくは，$ \lorの導入規則を使って演繹できる．Bが真なら$ (A \to B)は常に真．
つまり，$ \lnot Aか$ Bのどちらかを満たせば$ (A \to B)は成立する．
$ (A \leftrightarrow B) \leftrightarrow ((A \land B) \lor (\lnot A \land \lnot B))
AとBが同値なら，AとBどちらも真あるいはAとBどちらも偽．
$ (( A \to B) \to B) \leftrightarrow (A \lor B)
先に見たように$ (A \to B) \leftrightarrow (\lnot A \lor B)である．
つまり左の命題が真ならばBは必ず真．$ \lorの除去規則より$ B \to Bにできるのでトートロジー．
論理式
われわれは， $ A \lor \lnot Aという命題のことを排中律とよびました．
しかしそれは，じつは1つの命題ではないのです．Aとしていろいろな命題を考えてみれば，いろいろな排中律ができるのです．要するに，排中律というのは，1つの命題につけられた名前ではなくて，ある形をした一群の命題につけられた名称であり，または<命題の形>そのものにつけられた名称とも考えられます．
Aを自由変数とする命題関数のことを排中律，と言っている．．ということ?
ここまで示した演繹や公理はすべて「命題の形」や「推論の形」の一般形式のみを取り扱った．
つまり，具体的に命題がどのようなものであるかは議論しなかった．代わりに，代数を用いた．
$ A, B, C...を任意の命題とし，
$ F(), G(, )を任意の述語と表した．
命題変数と述語変数を用いて表された命題の形式を論理式という． つまり，これまで示された命題というのは，特定の命題ではなく命題変数をのみ用いている以上，全て論理式であった．
さらに分類があって，$ \forall,\existsの二つの限量子を含まないものは命題論理の論理式とよぶ． 論理式の真偽値
ある論理式が与えられたとして，それ自体には真偽値が対応できない．
それ自体は命題ではないからである．
入力となる命題変数の真偽値を仮定することで演繹を行い，等価な命題を結論することはできるが，それは仮定にすぎない...という意味?
命題論理の論理式というものを一応はっきりさせておきましょう．
まず，そこで用いられる命題記号は，つぎの2種類だけであるとします．
命題定数 $ \bot
命題変数 $ A, B, C, ...
そこで，この2種類の命題記号に，
$ \to, \lor, \land, \lnot
という論理演算を有限回ほどこして得られるところの命題の表現を<命題論理の論理式>というのです．
で，
命題定数$ \botの真理値は$ \botであるとします．
つぎに命題変数のおのおのに，$ \topあるいは$ \botを，それぞれ1つずつに任意に対応させ，それを命題変数の真理値とします．
この時点で無矛盾律と排中律を暗黙の前提としている気がする．
つまり最小論理では真偽値を求めることはできない，という先ほどの議論に帰結する．
まあ矛盾の概念を許容したら真偽値の概念は無理か．
すると，第3章の$1-$4に述べました
$ \lnot, \to, \land, \lor
に関する真理表にしたがって計算することにより，すべての論理式(=命題論理の論理式)の真偽値が定まります．
これを，もっと精密に表現いたしますならば，命題論理のある論理式が与えられたとき，その論理式に現れるすべての命題変数の真理値を任意に定めさえすれば，それでその論理式の真理値は定まるのであります．
さきほど論理式(というか命題と結合命題)から真理表を作っていたわけで，入力が定まれば出力も一意に定まる，というのはまあ，そうかな，という感じ．
命題変数への真偽値の定め方は前述の通り$ 2^n通りある．
この$ 2^nの全ての入力について論理式の出力が$ \topであることをトートロジーという． 論理式の真理値と真理値の基本性質
論理式の真理値と，3章で述べた真理値の定義はまったく異なるもの．
3章においての真理値は，「予め命題に対して定められた値」である．
論理式の真理値は，
おのおのの命題変数の真理値というものをわれわれがかってに与えることによって，はじめて定まるものであります．
これを考えると，3章で述べた真理値の性質も違った意味合いを帯びてくる．
再掲:
(I) 第2章で述べた演繹法で証明される命題の真理値は$ \topである．
これは，演繹法によって証明される命題はすべて正しい，ということでもあります．
(II) 2つの命題$ A および$ A \to Bの真理値がともに$ \topであるならば，$ Bという命題の真理値も$ \topである．
(III) $ Aの否定 $ \lnot Aの真理値が$ \topのとき，および，そのときにかぎって，$ Aの真理値は$ \botである．
これをs/命題/論理式/g とする．
と，この3つの条件は，3章においてはとりあえずの仮定といったものだったのが，証明可能なものとなる．
(II)は，Aを大前提としたときの命題結合記号$ \toの除去規則から導ける．
(III)は排中律+無矛盾律のこと．古典論理の公理と同じ．
(I)については説明が長くなるらしい．付録にされている．以下を証明している
命題論理の論理式でしかも演繹法によって証明される論理式は，いかなる真理値の与え方に対してもつねに $ \topという真理値をもつ，ということを証明する．それは，演繹によって証明される命題論理の論式はすべてトートロジーに限られるということを意味するから，このことからただちに，矛盾命題を表す命題定数$ \botは演繹によっては証明され得ないという，いわゆる<演繹法の無矛盾性>が導かれる．
具体的には以下の定理を証明している
定理
1つも仮定をもたないか，または，仮定があるとしても，仮定として用いられている論理式の真理値がすべて$ \topであるような演繹によって導かれる論理式の真理値は$ \topである．
数学的帰納法により，n個の推論が存在するとき，全ての推論(命題結合記号の除去と導入)において，真理値がすべて$ \topであれば推論結果も$ \topとなることを場合分けして証明している．
えーと仮定として用いられる論理式の真理値のいずれかが$ \botである演繹の結論はどうなるのだろう?
それが$ \botでありうるならこの定理では足りない...気がする
あー，真理値の仮定がない論理式は，「真理値の入力が未」ということなので，$ \topの場合$ \botの場合それぞれを演繹して，ともに$ \topとなることを示せばよいのか．
そうすると，最大の問題は $ Aという論理式で仮定が$ Aは$ \botという状況のみで，これを除外すると．
上記の話は要するに:
ある論理式が与えられた時，命題変数を任意に定めれば，演繹法を用いることで真理値が$ \topとなる場合は証明できる．
つまり，ある論理式が真である，入力の組み合わせを探索/計算できる，ということ．
ただし，命題定数$ \botについては異なる．
矛盾命題を表す命題定数$ \botは純粋な演繹法のみによっては証明することはできません．
ということ．これを<無矛盾性>という．
無矛盾性といえば一般に $ \lnot (A \land \lnot A)とされる．これと同じ意味．
「演繹によって$ A, \lnot Aを同時に証明することはできない」ことは，証明できる．
つまり，演繹法を公理に取り入れたとき，無矛盾律は証明できる．
(I)の話は付録とされているが，この話が混みいってくる理由についてさらにこの後記述される．
無矛盾性はなぜ必要か
演繹法は，トートロジーである論理式を変形させる処理である．
つまり$ \topの仮定から$ \topを導く効果しかもたない．$ \botを仮定した際の挙動は証明できない．$ \botを結論することもできない．
すなわち$ \lnot (A \land \lnot A)となる．
この性質をわざわざ述べた理由は，無矛盾律を前提においていることを説明したかったからである． まわりくどいな... 最初の「命題の真理値」(III)の時点で無矛盾律を前提におくことはわかったが...
たびたび述べてられている通り，無矛盾律は証明されていないし，根拠のない主張である．
直観主義や最小論理では，無矛盾律も排中律も採用していない．
ある命題について，必ず真か偽が求まり，かつどちらかである，という公理は証明できない．
とはいえ，この本では古典論理を扱うので，無矛盾律と排中律は公理となる．
しかし，演繹法は公理ではない．
すなわち，無矛盾律と排中律と最小論理を用いて，演繹法の演繹によって証明される命題が全て$ \topであることを証明しなければならない．
なぜなら，演繹法をそういう要件を持つ道具立てとして作ったのだから．
なので演繹法の性質を証明する必要がある．
ここでは背理法を使う．
すなわち，「演繹法の演繹によって$ A \land \lnot Aとなる命題が証明されない」ことを証明すれば二重否定の除去でいける． ここで付録1の定理に行きつくというわけ．
無矛盾性証明の指針 命題の真理値に関する基本性質を認めることは，われわれの演繹法をそのまま信ずることであります．したがって，演繹法が矛盾を導かないことを示すのに命題の真理値の基本性質を用いたのでは何にもなりません．
演繹法では，個々の命題の内容を一切考慮しておりません．そこでは，命題の形式のみを問題にしています．ですから，命題の代わりに論理式を用いて無矛盾性を証明すれば，それで十分であります．
つまり，命題の真理値をリフレインして s/命題/論理式/g したのはそれなりに意味があって，この二つは別物である．
論理式を演繹して結論される命題が常に(命題変数に$ \botを仮定しない限りにおいて)$ \topであることを証明できれば，命題の真理値に関する基本性質が得られる，というわけ．
命題論理の完全性
この章では，どんな真理値を各命題変数に与えても，つねに$ \topという真理値をもつものをトートロジーといった．
そして，演繹法は，論理式を変形させる演算であり，与えられる命題変数の真理値とは関係ないことも見た．
ということは，命題の基本性質である，「演繹法によって証明される論理式は真理値が$ \topのものに限る」とは，
命題論理の論理式で演繹法によって証明されるものはすべてトートロジーである
トートロジーはすべて演繹法によって証明することができる
ということになる．つまり，演繹法はトートロジーについてのみ使える道具立てだ．
与えられる命題変数の真理値が変わると，結合された論理式の真理値が変わる...という場合には，演繹はできない．
述語論理についての話はここではしていない．
第5章 命題の同値
$ (A \to B) \land (B \to A)のとき$ \leftrightarrowという記号で「同値」を表現した．
この記号は古典命題論理や最小論理の議論であって，述語論理の議論ではなかった．
ここでは述語論理における同値の概念について見る．
まず，同値記号$ \leftrightarrowのセマンティクスとして置換法則(law of replacement)が成り立つ． $ A \leftrightarrow B, F(A) \vdash F(B)
$ (A \leftrightarrow B) \to (F(A) \leftrightarrow F(B))
命題関数 $ F が他の命題結合記号だったらどうか?
$ (A \leftrightarrow A') \vdash (\lnot A \leftrightarrow \lnot A')とか，$ (A \land A', B \land B') \vdash ((A \land B ) \leftrightarrow (A' \land B'))とか．
これらすべての命題結合記号が証明可能(演繹によってトートロジーであることが導出される)．
さらに，限量子についても同様で，
$ (\forall x (F(x) \leftrightarrow F'(x))) \vdash (\forall x F(x) \leftrightarrow \forall x F' (x))
$ (\forall x (F(x) \leftrightarrow F'(x))) \vdash (\exists x F(x) \leftrightarrow \exists x F' (x))
が証明可能．
ただし，命題$ F(A)は必ずAのみによって真偽が定まらなければならない．
他の束縛変数によって値が変わるときは$ F(A,B,...)と記述されなくてはならない．
そして，$ F(A) \leftrightarrow F(B)とは何か，を考えると，上述したように，Fが単独の変数によって真偽が決定され，かつ，どちらも$ F()が真を返す，ということになる．
このような$ Fを真理関数(truth-value function)とよぶ．
ところが，$ Fが真理関数であることを演繹法(置換法則)の上では表現できない．
置換法則が成り立つなら$ Fは真理関数だ，ということは定義できる．ところが置換法則ぬきに真理関数は定義できない．
与えられた$ Fが真理関数であるか否かを決定せよ，という問題を一般的に解決することは，原理的な困難性を含んでおります．(中略) $ Fが与えられるということは，じつのところ，一般的には何が与えられるのかよくわからない．そのことの意味がよくわからない以上，われわれは，$ Fの与えられ方をある程度限定した上で，その問題を解決する以外に方法はないということなのであります．
じゃあなんで真理関数という概念を出してきたんだろう？
置換定理(replacement theorem): $ \to, \land, \lor, \lnot, \forall, \existsと命題$ Aを用いて表される$ F(A)については，置換法則が成り立つという定理．
これを証明するには，
$ A \leftrightarrow B \vdash F(A) \leftrightarrow F(B)を導出すればいい．あれ，さっきやんなかったっけそれ．
これは場合分けすると，
$ F(X)が$ Xのとき(F(X)が「AはAである」みたいな命題のとき)
$ F(X)が$ CというXを含まない異なる命題のとき(F(X)が「人はみな死ぬ」みたいな命題関数のとき)
$ F(X)が命題結合記号で表される場合(「Aならば$ F_2(A)である」みたいな命題関数のとき)
となる．これらは演繹法と置換法則によって導出可能．
導出できないのは，$ F(X)が↑の命題結合記号・限量子，命題以外の変数ないし要素ないしナニガシに左右されるとき．
述語の同値
述語つまり$ F()についても同値という概念の定義がある．
すなわち$ F(X) \leftrightarrow G(X)が結論される命題が存在する．
それは$ \forall x (F(x) \leftrightarrow G(x)).
集合と考えるとわかりやすい
これは2変数以上の述語についても成立する．
第六章 ド・モルガンの法則と双対の原理
ド・モルガンの法則についてはある程度知っているので飛ばす．
二重否定の除去を公理として採用すると(==古典論理だと)証明が簡易化するらしい．
まあ， !A || !B と !(A && B) が等価とするには，!!(!A || !B)を演繹で経由すると楽．
せっかくなので「問」を見てみる
$ \lnot A \lor \lnot B \leftrightarrow \lnot (A \land B)の証明:
$ A, Bを仮定.
$ A, B \vdash A \land B # $ \land導入規則
$ \lnot (A \land B)を仮定．
$ A \land B, \lnot (A \land B) \vdash \bot
$ \vdash \lnot Aこれにより仮定$ Aを除去．# 無矛盾律より$ A \to \botなので$ \lnot A
$ \lnot A \vdash (\lnot A \lor \lnot B) # $ \lor導入規則．最初の命題に戻る
$ \lnot(\lnot A \lor \lnot B)を仮定．
$ \vdash \bot
$ \vdash \lnot B これにより仮定$ Bを除去．# 無矛盾律
$ \vdash (\lnot A \lor \lnot B), \lnot(\lnot A \lor \lnot B)# また?
$ \vdash \bot
$ \vdash \lnot \lnot (\lnot A \lor \lnot B) # 無矛盾律より仮定$ \lnot (\lnot A \lor \lnot B)を除去．
$ \vdash \lnot A \lor \lnot B # 二重否定除去．
$ A, B，$ \lnot(A \land B)が真と仮定して$ \lnot A \lor \lnot Bを導けた．
別解
$ \lnot A, \lnot Bを仮定
$ A \land Bを仮定
$ A \land B \vdash A, B # $ \land除去規則
$ A, B, \lnot A, \lnot B \vdash \bot, \bot
$ (\lnot A \lor \lnot B, \bot, \bot )\vdash \bot # $ \lor除去規則．$ \lnot A, \lnot Bどちらにせよ$ \botが成り立っているので$ \bot.
$ \vdash \lnot (A \land B) # 無矛盾律より．$ A \land Bの仮定は除去．
$ \lnot A \lor \lnot B \to \lnot (A \land B) # $ \to導入規則．$ \lnot A \lor \lnot Bを仮定から除去しても$ \lnot (A \land B)が成り立っている．
あれ，$ \lnot A, \lnot Bの仮定は除去しなくていいのか?
矛盾が導かれた時点で無矛盾律より$ A, Bが結論できて，仮定は除去?
残る仮定$ A \land Bのとき必ず$ A, Bであることを結論していて，この仮定が除去できれば(トートロジーだと証明できれば)A,Bを除去する必要はないのか．
ちなみに，以下もド・モルガンの法則と呼ばれている
$ \lnot \exists x F(x) \leftrightarrow \forall x \lnot F(x): いずれかのxがF(x)で偽なら，全てのxがF(x)で真ではない
$ \lnot \forall x F(x) \leftrightarrow \exists x \lnot F(x): すべてのxでF(x)が偽なら，いずれかのxがF(x)で偽
3.ド・モルガンの法則の一般化
ド・モルガンの法則から，より重要な双対という概念を導く．
<論理式>の定義
(1) 個々の命題変数は，それ自身で論理式であると考えます．
また，$ Pを任意の$ n変数の述語変数とするとき，任意の対象式$ t_1, t_2, ..., t_nに対して$ P(t_1, t_2, ..., t_n)は論理式であります．
(2) $ Aおよび$ Bが論理式であるとき，$ A \to B, A \land B, A \lor Bはすべて論理式です．また，$ Aが論理式ならば$ \lnot Aも論理式であるとします．
(3)$ F(a)が論理式で$ aが自由変数であるとき，$ F(a)に含まれない任意の束縛変数$ xを用いて作られる$ \forall x F(x)および$ \exists x F(x)は論理式であります．
そうして，ここでは，上の (1)におけるような論理式をもとにして， (2)や (3) の操作を有限回ほどこして得られる論理式だけを考えようというのであります．
ある論理式が $ \toという記号を含まないとき，以下の操作を行うと双対(dual)と呼ばれる論理式が得られる．
1. $ \landという記号をすべて$ \lorに変える
2. $ \lorという記号をすべて$ \landに変える
3. $ \existsという記号をすべて $ \forallに変える
4. $ \forallという記号をすべて$ \existsに変える
対偶とどう違うんだ?
あー，限量子が入ると対偶では表現できないか.
これはド・モルガンの法則から得られる(つまり演繹によって結論可能なトートロジーの)論理式である．
定理
論理式 $ F(P_1, ..., P_m)が$ P_1, ..., P_m以外の述語変数・命題変数を含まず，さらに， $ \toという論理記号を含まない場合，その双対を$ F*(P_1,..., P_m)と表せば，
$ \lnot F(P_1, ..., P_m) \leftrightarrow F* (\lnot P_1, ..., \lnot P_m)
という論理式が証明できます(ド・モルガンの法則の一般化)．
また，論理式が$ \toを含む場合でも，以下の置換定理を用いて演繹すれば双対が得られる
$ (A \to B) \leftrightarrow (\lnot A \lor B)
この置換定理の証明は排中律を用いる．
ここまでの双対という概念について一般化したものが双対の原理． 定理1. $ Aが論理記号$ \toを含まぬ論理式であるとき，$ Aの双対を$ A*と表せば，つぎの(I), (II)が成立します:
I) $ Aが証明できれば，$ \lnot A*も証明できる．
II) $ \lnot Aが証明できれば， $ A*も証明できる．
定理2. $ Aおよび$ Bが論理記号$ \toを含まぬ論理式で，それらの双対をそれぞれ$ A*および$ B*とするとき，もし$ A \to Bが証明できれば，$ B* \to A*も証明できます．
定理3. $ Aおよび$ Bが論理記号$ \toを含まぬ論理式で，それらの双対をそれぞれ$ A*および$ B*とするとき，もし$ A \leftrightarrow Bが証明できれば，$ A* \leftrightarrow B*も証明できます．
具体的には，束縛変数を用いて，すべての入力に対してSerializableである，という論理式($ \forall x S(x))とする．
これの双対は，$ \forall を$ \existsとして，いずれかの入力に対してSerializableである($ \exists xS(x))，というもの．
双対の否定($ \lnot(\exists xS(x)) )が証明できれば$ \forall xS(x)が証明可能．
つまり，「いずれかの入力に対してSerializableである」が偽ならば，「すべての入力に対してSerializableである」が真．
あれ，なんかおかしい．考えなおす．
$ \forallと$ \existsはそれぞれ，$ \landや$ \lorを導入すれば除去できる．
すなわち$ \forall, \existsが双対であることは$ \land, \lorが双対であることを証明すれば等しい．
たとえば$ \forall x S(x)は$ S(x_1) \land S(x_2),...．
ド・モルガンの法則では，$ \lnot A \land \lnot B \leftrightarrow \lnot(A \lor B)
1. $ \lnot A \land \lnot Bの双対は$ \lnot A \lor \lnot B
2. 双対の否定は$ \lnot (\lnot A \lor \lnot B)
うーんん...
つまり$ \lnot S(x_1) \land \lnot S(x_2)... \leftrightarrow \lnot (S(x_1) \lor S(x_2)...)
すべてのxについてSが偽 == (いずれかのxについてSが真)が偽，と表現できる
あー，定理1. の(I) (II)と微妙に違う形を使っていたか？．
命題を論理式として表したとき、論理和 ∨ と論理積 ∧ とをすべて入れ替え、全称記号 ∀ と存在記号 ∃ とをすべて入れ替えたものをもとの論理式の双対といい、入れ替えて得られた命題をもとの命題の双対命題と呼ぶ。双対の双対はきっちり元に戻る。
元の論理式が証明可能ならばその双対の否定が証明可能であり、ある論理式の否定が証明可能ならば、その論理式の双対が証明可能になる。
ならば($ \to)，なので，ある双対の否定が証明できても，論理式が証明できるとは言えない?
まず、¬,∧,∨ だけを論理記号とする論理式 X を考える。ここで
• X 中の命題記号はすべてその否定に、
• X 中の ∨ はすべて ∧ に、
• X 中の ∧ はすべて ∨ に、
一斉に置き換えた論理式を X∗ とする。これを「X の双対（そうつい: dual）」と呼ぶ。
このとき、次が成り立つ：
双対原理：X と ¬X∗ は同値である。
と書いてある．述語論理と命題論理という違いはあるが，命題論理における双対とは否定も反転させるのか？
反転させて考えれば，双対$ A*が$ \exists x \lnot S(x)になり，$ \lnot(\exists x \lnot S(x))が双対の否定$ \lnot A*になる．
つまり「いずれかの入力がSerializableでない」が偽と証明できれば，「すべての入力がSerializable」となる．
こっちのほうが腑に落ちる．
でも$ Aを$ \lnot Aにすることが双対原理に含まれている．
というか$ A \land Bのとき$ \lnot (\lnot A \lor \lnot B)までいったものを双対と読んでいる．
$ \lnot A \lor \lnot Bを双対と呼んで，双対の否定としてさらに冠頭させるのだと思ってたが・・・
とりあえずブレてるようなのであまり気にしないことにしよう．
単純に，二重否定除去があれば導かれる演繹の公式のようなもの．
あらためて，
$ \forall x S(x): すべてのxについてSerializableが真
$ \lnot \lnot \forall x S(x): すべてのxについてSerializableでない，が偽
$ \lnot (\exists x \lnot S(x)): いずれかのxについてSerializableでない，が偽
がすべてトートロジーなので，３つめの式を証明すればよい．$ \lnot S(x)となる$ xの変数条件から．
第八章 補遺
といいつつ述語論理の観点からは重要な記述が多いと思う
特に，この本の序盤で議論から省かれていた(?)「限量子の変数条件」や「自由変数」という概念の深堀がある．
$ =に関する公理
$ =という記号を用いるときは，
$ t = t # 反射律
$ s = t \to (F(s) \to F(t)) # 置換法則
が成り立つものとする．
対称律，推移律なども成り立つ．
<=に関する反射律>はけっして1つの公理ではありません．$ t=tという形の命題はすべて公理である，といっているのです．しかし，もし
$ \forall x (x=x)
という1つの命題を公理として採用すれば，それからすべての反射律は導かれます($ \forall-除去)．
また，逆に，われわれが公理として採用してきた反射律を用いて，$ \forall x (x=x)という命題を証明することもできます．(中略)
以上のことから，我々は，つぎのことをも知り得たわけです:
(1) $ t=tという形の命題をすべて公理とすること
(2) $ \forall x (x=x)という1つの命題を公理とすること
(3) $ aという1つの自由変数を指定したうえで，$ a=aという1つの反射律だけを公理とすること
という3つのことは，すべて同等です．
高階の述語論理
$ \forall Fや$ \exists Fのように，述語に関する限量子が用いられるとき，2階の述語論理，と呼ぶ．
述語の述語に関する限量子が用いられるとき($ \forall F(\forall A)みたいな?)，3階の述語論理と呼ぶ．
このようなものを高階述語論理または型の理論とよぶ． コンピュータサイエンスの型の概念はここからきてる．
2階以上の高階の述語論理においては，$ a=bを命題
$ \forall F(F(a) \to F(b))
として定義することさえできます．そして，このような定義を下した時には，多くの場合，$ =に関する公理はもはや不要になるのです．
変数$ xの変域を自然数の全体とした場合，数学的帰納法の公理というものは
$ (F(1) \land \forall x (F(x) \to F(x+1))) \to \forall x(F(x))
と表されます．
なるほど〜
1階の述語論理においては，これは無限に多くの公理であると考えなければなりません．$ Fという述語を1つ指定するたびに，それぞれ1つずつの相異なる公理がそれに対応することになるからです．
しかし，2階の述語論理で考える場合には，数学的帰納法を
$ \forall F \{(F(1) \land \forall x (F(x) \to F(x+1))) \to \forall x(F(x)) \}
という一つの公理で代表させることができます．
$ =を用いると，以下のように，「ただひとつだけ存在する」を記述できる
$ \exists x (F(x) \land \forall y (F(y) \to y = x))
いずれかのxが，Fを満たし，かつ，すべてのyについて，F(y)を満たすyはxと同値である
同値でない場合はxかyが2つ以上存在する
この形の命題は
$ \exists ! xF(x)
という記号で表される．
対称領域
自由変数や束縛変数の記号については，変数条件という概念で区別してきたが，ここまでその実態は語られなかった．
ここではそれを語っている．
通常は，自由変数および束縛変数はすべて1つの共通な変域をもつものとします．
その共通の変域のことを対象領域といいます．そして対象と呼びましたものは，要するに，その対象領域に属するものー対象領域の<元>または<要素>ーのことをいうのであったのです．
述語論理を具体的な問題に応用する場合には，対象領域を1つは指定しなければならない．
それがなくては，$ \forall xや$ \exists yといった限量子の変域が不明となるし，意味がわからない．
ある限量子の変域を示すためには，部分領域(ここでは$ Dとする)を定義する．
部分領域を定義しなければ，その論理式は，暗黙に，すべての変数の変域が一種類ということになる．
つまり$ x, y, \forall zとだけ書いてあったりすると，すべての変数について「自然数」などの前提が入ってしまう
そこで以下のように示す．
束縛変数
$ \forall x(x \in D \to F(x)) # Dの全要素が$ Fを満たす
$ \exists x(x \in D \land F(x)) # $ F(x)を満たす要素がDの変域に存在する
また，1階述語論理においては，述語の定義域はすべて対象領域の全体でなければならない．
自由変数
$ F(a)とたんに書くことで，$ a \in D \to F(a)という命題を導くことを意味する．
また，$ F(a,b)はつまり$ (a \in D \land b \in D) \to F(a,b) である．
$ F(a)や$ F(a,b)は結論であれば議論が簡単だが，仮定である場合は注意．
その場合，$ a \in D \land F(a)を仮定しているのに等しい．
限量子の推論規則
ここで，限量子の推論規則を再び見直すと，
$ \forall- 導入: $ \frac{a \in D \to F(a)}{\forall x (x \in D \to F(x))}
$ \forall- 除去: $ \frac{t \in D, \forall x F(x \in D \to F(x)) }{F(t)}
$ \exists- 除去: $ \frac{t \in D \land F(t)}{\exists x (x \in D \land F(x))}
$ \exists- 除去: $ \frac{\exists x(x \in D \land F(x)), \{a \in D \land F(a) \} C }{C} # Dの任意の要素xがFを満たし，Dの変域の自由変数aがFを満たす
ただし，Dが空集合のときは議論がことなる．
$ x \in Dという命題は，$ xにどんな対象を代入しても，つねに偽な命題であります． したがって，
$ \forall x (x \in D \to F (x))
は真な命題で，
$ \exists x (x \in D \land F(x))
は偽な命題です．すなわち，どんな述語Fに対しても，$ \forall \xi F(\xi)はつねに真であり，$ \exists \xi F(\xi)は偽であります．ですから，当然
$ \forall \xi F(\xi) \to \exists \xi F(\xi)
という命題は成立しません．ところが，同じ形式をもつ
$ \forall x F(x) \to \exists x F(x)
は，$ xが対象領域を変域とする場合には，つぎのようにして証明することができるのです．
$ \frac{\forall \xi F(\xi)}{ \frac{F(a)}{ \frac {\exists x F(x)}{\forall x F(x) \to \exists x F(x)}} }
この形式scrapboxでうまく書けないな....
要するに，$ \exists x (x \in D)ということを仮定/公理としておいたとき，これは，Dが空集合でないことを意味する．
$ Dを変域とする自由変数$ aを用いるときには，$ a \in Dという命題はつねに仮定として使われていると考えていなければならぬのです．
任意の集合を対象領域として指定することはできるが，ただし，それは空集合であってはならない．
二つ以上の対象領域をもつ述語論理
ここまでの議論は変数の変域$ Dが一種類であることを想定していたが，
二種類以上の対象領域をもつ述語論理の論理式も，一種類の述語論理に還元可能である．
2つ以上の対象領域をもつ述語論理を考える場合には，それら個々別々の対象領域の和集合をただ1つの対象領域とする述語論理を考えればよいのです．そうすれば，もとの個々の対象領域はすべてその和集合たる対象領域の部分領域と考えられます
なるほどシンプル．
しかし，性質的に異なる，たとえばパンと酒をそれぞれ対象領域とする場合，和集合を生成するときに定性的に変化があるような気がするが．
述語論理の一般論として，たとえば$ \forall x F(x) \leftrightarrow \forall y F(y)は成立しないが，
$ \forall x \forall y F(x, y) \leftrightarrow \forall y \forall x F(x,y)は成立する．
なるほどこれでxとyが性質的に異なる場合でも議論できる...?