それ以来、時おり考えさせられてきたこと ─ 我々人類の推論と演繹は、いったいどういう構造を成し、実際どのように客観化（記号化）しているのだろうか
…とまあ、おおむねそんなことを考えていた矢先の、本書である。
『証明と論理に強くなる 小島寛之・著 技術評論社』
サブタイトルがとりわけ強力だ、なにしろ 「論理式の読み方から、ゲーデルの門前まで」 とあり、ゲーデルの名を見出した瞬間に、今度は数学論からチューリングマシン論までイメージがぱっと広がった。
そこで本書を読み進めてみれば、演繹フロー図や推論規則検証がズバ抜けて分かりやすい。
とりわけ数学やコンピュータプログラムに通じた読者であれば、直観的に理解が進むのでは、と察せられる。
一方では、文意が多元的ないし包括的に過ぎる箇所があり、このため却って論旨が掴みにくい点は惜しい (とくに助詞の 「の」 による繋ぎが判り難いのは、数理関係の類書について言えることである）。
本書コンテンツ第２部までの主旨を、あくまで僕なりにざっと要約してみると；
・或るなんらかの数学や命題や述語が、記号の構文（シンタックス）から成る論理式として、提示されているとする。
・その論理式から演繹されうる新たな論理式につき、真か偽か矛盾かを判定、その演繹（証明）の論理的な正しさを確かめる。
・ただし、いかなる演繹にしても、公理と推論規則がすでに完結的に準備されている（いわば演繹システム）。
・なお、同じ論理式と演繹システムでも、適用先の数理モデル＝可能世界によって、真偽は異なったものとなりうる。
・とはいえ、可能世界を問わず、あくまで公理と推論規則は正しい…この性質を（自己のメタ定義として）健全性定理と称す。
これらについて、本書で例示紹介される演繹システムは以下；
数学の基本論理を成す、 『等号』 における演繹システム
人間の命題論質の根本を成す、 『自然演繹』 における演繹システム
量化記号あわせ数学を検証する、 『述語論理』 における演繹システム
…さて、ここまで正しいとの僕なりの前提にて、本書の106ページ以降につき、自身の勉強録の意図もこめて以下に概略をメモってみた 。
【等号についての演繹システム】
等号 : = : の有する演繹機能につき、この数学上の特性を公理と推論規則を以て「等号の演繹システム」 として検証。
・等号の演繹システムにおける公理：
x, y, z を変数記号として
[公理T1]… 0+x : = : x
[公理T2]… x+y : = : y+z
[公理T3]… (x+y)+z : = : x+(y+z)
[公理T4]… ｘ*y : = : y*x
[公理T5]… (x*y)*z : = : x*(y*z)
[公理T6]… x*(y+z) : = : x*y+x*z
・等号の演繹システムにおける推論規則：
s, t, u, v などを任意の項の記号とし、ｘ を変数記号として
[対象律]… s : = : t から、t : = : s を導いてよい
[推移律]… s : = : t と t : = : u から、s : = : u を導いてよい
[代入律]… s と t に 変数 x が入っているとする。
ここで、s にある変数 x を任意の別項に置き換えて s1 が出来、また t にある変数 x を任意の別項に置き換えて s2 が出来るとする。
この場合、s : = : t ならば s1 : = : s2 を導いてよい。
[合成律]… s : = : t と u : = : v から、s+u : = : t+v を導いてよい。
また、s*u : = : t *v を導いてよい。
==============================
【等号の演繹システムにおける、健全性の定理】
演繹される式がいつも真である由：健全性定理を確かめる。
・まず、上に挙げた公理と推論規則の健全性をみる。
たとえば、以下の式をおく。
(x+y) * (z+w) : = : x*z + x*w + y*z + y*w …①
これに [公理Ｔ6]、[公理T4]、[合成律]、[公理T2]、[推移律] と充てて等号演繹を続けていくと、また①の式を得る事が出来る。
・次に、数学におけるモデルにおいて、この等号の演繹システムにおける健全性が「いつも」適用しうるかを確かめる。
たとえば、整数の代数のモデルにて、x=1, y=2, z =3, w=4 と数に置き換えて①を計算してみると、左辺も右辺も 21 となる。
したがい、ここでは等号の演繹システムの公理も推論も健全性が確かめられる。
また、空集合を含めた集合算のモデルにて、やはり x=1, y=2, z =3, w=4 と数に置き換えて①を計算してみると、左辺も右辺も 4 となり、やはり等号の演繹システムの健全性が確かめられる。
さらに、0 と 1 の（偶数と奇数の）２元体モデルでも、この健全性が確かめられる。
（※ なお、養老孟司氏の指摘によれば、等号を理解出来る生物は人間だけであるとのこと。また、欧米などでは等号そのものには完結的な意味をおかないケースも散見され、本書にても等号を演繹システムの例証として取り上げているのは実に面白い。）
====================================================
或る命題の構文上の表現つまり命題論理につき、本書では、人類共通の演繹方式として、ゲンツェンによる「自然演繹の形式化」のシステムを引用。
自然演繹システムの論理記号による推論規則；
[⇒（ならば）の除去］……論理式 t1 と、t1⇒t2 がともに演繹されていたら、⇒記号を除去し、論理式 t2 を新たにつなでいでよい。
[⇒（ならば）の導入]……論理式 t1 が「仮定」された場合に論理式 t2 が演繹されていたら、論理式 t1 ⇒ t2 をつなげ、「仮定」である論理式 t1 を解消してよい。
この推論規則 [⇒導入] があればこそ、或る「仮定」が公理であったとしてもそれを恒真式として反復させる必要が無い。
また、これら推論規則 [⇒除去］ と [⇒導入] の組み合わせによって、三段論法の演繹も出来る。
[∧(かつ）の導入]……論理式 t1 が演繹されており、また論理式 t2 も演繹されていたら、t1∧t2 も演繹出来る。
[∧(かつ)の除去]……論理式 t1∧t2 が演繹されていたら、そこから(当然に)論理式 t1 も演繹出来、論理記号 ∧ を除去出来る。
[∨(または)の導入]……論理式 t1 が演繹されていたら、t1∨t2 も演繹出来る。
［∨(または)の除去］……論理式 t1∨t2 が既に演繹されており、さらに、 t1 を仮定すれば新たな論理式 t3 が演繹され、一方では t2 を仮定しても t3 が演繹されている、ならば仮定としての t1, t2 をともに解消しつつ、t3 をつないでよい。
この推論規則 ［∨除去］ は数学などの場合分けによる証明にて起用されている。
［￢(でない)の除去］……論理式 t1 と ￢t1 がともに演繹されていたら、論理式 ⊥（矛盾） を演繹してよい。
[背理法]……仮定としての論理式 ￢t1 から論理式 ⊥（矛盾） を演繹出来るなら、仮定 ￢t1 を解消しつつ、論理式 t1 を演繹してよい。
この推論規則が、数学などにおける背理法の証明にて起用されているが、いわゆる直観主義を主張しつつ背理法を認めない数学者たちもいる。
[￢(でない)の導入]……仮定としての論理式 t1 から ⊥（矛盾） が導出されるなら、仮定 t1 を解消し、￢t1 を演繹してよい。
[⊥（矛盾) の推論規則]……すでに何らかの論理式から矛盾が演繹されている場合、それらとは全く別の新たな論理式 t1 を演繹出来る。
元来の数学にては、公理は矛盾しないものとされてきたが、理由は、もし或る数学公理が矛盾しているとしたら、それに則ったはずの新たな論理式に論拠が無いこととなるため。
とはいえ、この [⊥（矛盾) の推論規則] の導入により、数理論理学として、さまざまな演繹システムが数学として矛盾を孕むか否かまで検証するようになっている。
====================================
【自然演繹システムにおける、健全性の定理】
それぞれの推論規則が常に真を導き、だから演繹システムとしても常に真；健全性を成立させている。
よって、これによる証明（数学などにおける）は常に真を演繹していることになる。
・たとえば、上に記した推論規則のうち、 [∧(かつ）の導入] のみを用いる演繹の例。
まず、まだ演繹の行われていない論理式 s1 と s2 があり、いずれも真である、ならば、当然 s1 ∧ s2 も真である…ここまでで、まず [∧(かつ）の導入] の健全性が成り立つ。
この論理式 s1 ∧ s2 から演繹される論理式 s も真であり、また s ∧ s3 が演繹されるので、s3 も真である…ここまででも、やはり [∧(かつ）の導入] の健全性が成り立つ。
こうして演繹を続けていくと、任意の論理式 s と t において、どの演繹の段においても、直前の段の演繹により、s∧t は常に真となる。
だから、推論規則 [∧(かつ）の導入] はいつも真を導く。
これが数学的帰納法による演繹である。
・また、演繹のどこかに推論規則 [⇒（ならば）の導入] が含まれる例。
本旨の前提である、論理式すべて真の仮定集合 T に加えて、真偽の判然としない論理式 s をおき、あわせてT∪｛s｝ とする。
ここで、s が真ならばこの T∪｛s｝ 全体も真、推論規則 [⇒（ならば）の導入] によって演繹される t も真、だから s⇒t は真となり、T∪｛s｝ は解消される。
一方で、s が偽ならば、推論規則 [⇒（ならば）の導入] によって演繹される t が真であるか偽であるかは問わず、やっぱりs⇒t は真 となり、T∪｛s｝ は解消される。
どっちにしても、推論規則 [⇒（ならば）の導入] 自体は真を導く。
…このようにして、すべての推論規則は、演繹上のどこの段階で機能しようとも常に真を演繹する。
だから、自然演繹システム全体が常に健全性をたもつ。
・以上の健全性の定理にては、真であろう論理式がなんらかの仮定集合（平面幾何の公理、球面幾何の公理など）の内にある場合もあるが、そもそもどんな仮定集合にも属していない場合もあり、後者の場合ならば、適用先の可能世界モデルには制限が無いということになる。
ここまでふまえれば、この定理は 「拡張版としての健全性定理」と呼ぶことも出来る。
========================
・なお、等号の演繹システムにても、自然演繹システムにても、さらに完全性定理がある。
ざっと言えば、「全ての可能世界モデルで普遍的に真となる、あらゆる論理式は、そこでの公理と演繹規則によって必ず演繹出来る」というもの。
（※ ちょっとこの段は僕には捕捉しかねる難解なところ。）
=============================================
【述語論理式と量化記号】
ドイツ哲学者フレーゲが始めた述語論理をもとに、ホワイトヘッドとラッセルが 『数学大全』 によってあらゆる論理の記号操作方式としてまとめあげた。
・述語論理式の例として、Love(x,y) で、これを 「x は y を愛する」 と解釈するものとする。
これだけでは、真偽は判定しようがない。
真偽の判定のために、２つの量化記号； ∃（存在量化記号） と ∀（全称量化記号） を起用する。
すると、述語論理式はたとえば以下の２つに峻別出来、それぞれ厳密に真偽判定が出来る。
① ∀x∃yLove(x,y) … 『「x は y を愛する」、という関係の y が存在することが、すべてのxについていえる』
② ∃y∀xLove(x,y) … 『「x は y を愛する』、という関係がすべての x について成立する、そんな y が存在する』
・述語論理式と量化記号を、数学に適用してみる。
まず、述語論理式として、Even(x) を 「x は偶数である」 と解釈するものとする。
これだけでは、そもそも数学として真偽判定のしようがない。
ここに量化記号を起用すれば、適用される可能世界モデルが定まり、だから述語論理式の真偽を厳密に判定出来る。
たとえば、この述語論理式を「自然数すべての集合」という可能世界モデルに適用するならば、∀xEven(x) …「存在する x はすべて偶数である」、と表現することになる。
よって、この述語論理式は偽であると厳密に判定出来る。
また、適用先の可能世界モデルを 「（なんらかの）自然数」 とするならば、たとえば ∃x(Even(x)∧Prime(x)) …「偶数かつ素数である x が存在する」 と表現する。
この述語論理式は自然数「すべて」についてではないので、真であると判定出来る。
さらに。
∀x∃y(x+y=0) という述語論理式は、「整数の代数モデル」 に適用するならば x+y が必ず整数となり、だから真となる。
しかし、これをひっくり返して、∃y∀x(x+y=0) という述語論理式をつくり、やはり 「整数の代数モデル」 に適用すると、すべての x に対して同じ y をとるわけではないので、これは偽となる。
・量化記号を起用した述語論理式であれば、数列の一定数への極限などのような動的な概念も表現出来 （任意の正数それぞれへの番号付けと範囲設定など）、よって成立を証明出来る。
====================================================
…ざっと、ここまで概括。
本書はさらに第３部以降、述語論理における公理や推論規則を 「（メカ）自然数」 による演繹にて紹介、 ─ とはいえ、このあたりから先は推論規則と演繹がどんどん複合的になってゆき、もう僕のセンスでは理解に自信なし。
かくして、ゲーデルの不確実性定理の門前どころか遥か手前で、いったんギヴアップさせて頂く。
重ねて記すが、本書はコンピュータプログラムないし数理論に通じた読者であれば、それらに培われた直観力をもってかなりの速度で理解しえよう。
以上